様相論理に基づいたプログラム解析手法の研究

点击翻译按钮获取中文摘要

本研究の主な目的は,様々なプログラム解析を統一的に扱える枠組みを,様相論理という論理体系を元にして開発し,実際のプログラミング言語の解析のための型システムとして応用することにある.本年度は,昨年度まで研究を行ってきた様相論理体系に基づく情報流解析の枠組に関する考察と,論理関係を用いた非干渉性定理の一般化を行った.非干渉性とは,秘匿性の低い計算結果は,秘匿性の高い入力に依存しないこと,すなわち,秘匿性の高い入力の情報が1ビットたりとも漏洩していなことを示す性質であり,情報流解析の正当性として用いられている.従来の多くの研究では,入力と出力に関しては,整数などの基本的データ型に限って非干渉性が考察されてきた.我々の研究では,プログラムの等しさを論理関係というプログラム意味論の分野で使われている技法を用いて定式化することにより,基本的データだけではなく,関数値などの高階なデータ型に関しても適用可能な形に,非干渉性定理を一般化し,それを証明することに成功した.またこの結果から昨年まで行ってきたDCCという別の情報流解析の枠組との比較についても,両者は,比較不可能(どちらも相手よりも勝っている部分がある)という結論が出た.今後は両者の長所を統合したような,より一般的な情報流解析の枠組を目指すことが望まれる.