| 研究概要 |
近年のコンピュータネットワークの普及により,信頼できない相手からソフトウェアがWWWや電子メールを介して受け取る機会が増えている.本研究の目的は,そのような状況において受け取ったソフトウェアが既存のシステムに危害を及ぼさないことを型システムを用いて静的に保証することである.本年度の研究成果は以下の通り.
1.情報流解析の拡張・改良とそれに基づく検証器の実装
並行プログラムが機密情報を漏らさないかどうかを解析するための一般的な型システムを構築し,その正しさを証明した.ロックや通信などの並行プリミティブを扱ったプログラムについて,情報漏洩の可能性を既存の並行プログラムの情報流解析と比べてより正確に判定することができる.
2.並行プログラムの検証のためのCoqライブラリの構築:
Coqなどの定理証明器を用いてプログラムの検証を行うことができるが,メールサーバのような並行プログラムの検証を定理証明器を用いて一から行うためには多大な労力が必要となり,現実的ではない.そこで,Coqを用いた並行プログラムの検証を容易にするためのライブラリを構築した.
3.様相論理に基づく情報流解析の理論
近年,型システムに基づく情報流解析手法が多数提案されているが,それらは対象言語毎に少しずつ異なる型システムを設計しているため,手法の細かな比較が困難になっている.そこで我々は,情報流解析の型システムを様相論理の見地から見直し,それら多数の型システムの基礎付けとなるような型システムを考案した.その結果,情報流解析の正当性の証明が,これまで提案された手法に対しての証明よりも,遥かに簡単に行なえることが明らかになった.
|
