 |
 |
 |
 |
 |
 |
 |
Home > 高い生産性を持つ高信頼ソフトウェア作成技術の開発 > 米澤 明憲
米澤 明憲
プロジェクトリーダー
片山 卓也 （北陸先端大学）
課題名
安全なシステム記述言語および高信頼OS
代表者・所属
米澤 明憲 (東京大学)
目的
型理論などのプログラム静的解析技術による，性能を劣化の少ない既存の基盤ソフトウェア(コンパイラ，OS，デバイスドライバ)の安全性の強化を通した，それらを使用する応用ソフトウェアの安全性の確立．
目標
- 高安全なC言語，およびC++言語コンパイラの開発
- 現在，システム記述に最も広く使われているCおよびC++言語での，コンピュータウィルス感染や情報漏洩の危険性のない，対攻撃耐性を持ったコードを生成する高安全 Cコンパイラを開発する．
- OS用型付きアセンブリ言語の設計・実装
- 従来高級言語に使われていた型理論を適用した型付きアセンブリ言語をさらに拡張し，OSカーネルのスレッド切替機構，割込処理機構，デバイスドライバ等のアセンブリ言語で書かれた構成要素を再記述することで，OSの安全性を大幅に向上させる．
- プロトコル実装の形式的検証
- サーバなどの基幹ソフトウェアが使用する通信プロトコルの実装が，その仕様に対して正しいかどうかを，定理証明器を用いて検証する技術を構築する．
期間
5年間