2003 Fiscal Year Annual Research Report
実行の安全性を保証するC言語コンパイラの実装手法に関する研究
Project/Area Number |
03J10889
|
Research Institution | The University of Tokyo |
Principal Investigator |
大岩 寛 東京大学, 大学院・情報理工学系研究科, 特別研究員(DC2)
|
Keywords | セキュリティー / C言語 / コンパイラ / 安全性 |
Research Abstract |
メモリ操作の安全性を保証するC言語の処理系である「Fail-Safe C」の実装方法について考察し、ANSI規格の定めるC言語の範囲のプログラムのうち共用体を含まないものを処理できる基本的な処理系を実装した。その処理系を小・中規模のプログラムに対して適用し動作を確認した。特に、構造体を含むプログラムを安全に動作させるためのメモリ上のデータ表現や、動作において必要とされる「アクセスメソッド」の具体的な実装法を確立し、実際の実装においてその正しさを確認した。具体的には実装した処理系を用い、実際に実用に供されているオープンソースのメールサーバソフトウェアから抽出したセキュリティーホールを含む部分のソースファイルをコンパイルし、危険な動作をきちんと検出し、安全にプログラムを停止させられることが確認できた。 実行時に安全性を検証する操作を軽減するためのプログラムの解析および最適化の方針については、研究を進める段階で処理系の構造やその安全性の理論的根拠が複雑になってきたため、動作の意味論についての新たな定式化の手法について検討することとし、理論的根拠を構造的に整理し実行安全性の統一的な議論を可能とする定式化手法をほぼ確立した。これにより、解析および最適化の導入がプログラム実行の安全性に及ぼす影響をきちんと議論することが可能になり、Fail-Safe Cの保証する安全性を保ったまま様々な解析・最適化手法を導入することの目処を立てることができた。 研究成果の公表については、実装上遭遇した困難の解決に予想以上の時間を要したため、報告書作成時点では論文誌等への投稿が間に合わなかうたが、ワークショップ等複数の場所において口頭によるデモンストレーションを行い、成果物の動作状況を公表した。また、現在論文を投稿準備中であり、公表を急いでいる。
|