| 研究概要 |
近年のコンピュータネットワークの普及により,信頼できない相手からソフトウェアがWWWや電子メールを介して受け取る機会が増えている.本研究の目的は,そのような状況において受け取ったソフトウェアが既存のシステムに危害を及ぼさないことを型システムを用いて静的に保証することである.本年度の研究成果は以下の通り.
1.計算資源に対するアクセス方法の正しさの検証のための型システムの改良と実装
計算機システムにおいては,プログラムは記憶領域(メモリ),ネットワーク,CPU,ファイルなどさまざまな資源を共有して動作しており,あるプログラムが不正に資源にアクセスを行うと,計算機システム全体の動作に悪影響を与える.そこで昨年度我々は,プログラムが正しいプロトコルで資源にアクセスすることを検証するための型システムをに開発した.本年度は,その型システムを改良するとともに,具体的な応用例としてJavaのバイトコードが正しくロックの獲得と解放を行っているかを検査するための検証器を作成した.
2.低レベル言語のための情報流解析の型システムの拡張と実装
昨年度研究を行ってきたJavaのバイトコードがパスワードなどの機密情報を漏らさないかを検査するための型システムを拡張し,実装を行った.
3.メールサーバの形式的検証
定理証明支援システムCoqを用い,メールサーバプログラムのモデル化および検証を行った.
|
