| 研究概要 |
本研究の主な目的は,様々なプログラム解析を統一的に扱える枠組みを,様相論理という論理体系を元にして開発し,実際のプログラミング言語の解析のための型システムとして応用することにある.本年度はプログラム解析のひとつである情報流解析のための様相論理体系を考案し,形式化した.
情報流解析とは,プログラムが実行中に機密情報を意図せずに漏洩することがないことを検査するための手法であるが,近年,型システムに基づく情報流解析手法が多数提案されいる.しかし,それらは対象言語毎に少しずつ異なる型システムを設計しているため,手法の細かな比較が困難になっている.そこで,情報流解析の型システムを様相論理の見地から見直し,それら多数の型システムの基礎付けとなるような型システムを考案した.具体的には,情報の秘匿性情報のつけられた型と様相論理における「必ず・・・である」という命題が対応することを観察し,直観主義様相論理の証明システムと対応する型システムを形式化し,主部簡約定理・合流性・強正規化可能性など種々の論理体系として好ましい性質や,不干渉性という情報流解析としての正当性を証明した.この過程において,不干渉の証明が,これまで提案された手法に対しての証明よりも,遥かに簡単に行なえることが明らかになった.
来年度は,ここで得られた情報流解析と様相論理の対応関係を一般化するとともに,どのようなクラスのプログラム解析の型システムが様相論理と対応しているかを考察していく.
|
