安全なシステム記述言語および高信頼OS記述言語
| リーダー | 米澤 明憲 |
文部科学省、２００３〜２００７
高信頼基盤ソフトウェアの必要性
高度情報化に伴い，コンピュータウィルスや不正アクセス，情報漏 洩などの問題が，社会の安全性を脅かす深刻な事態となってきてい る．今後，さらなる情報化は不可避であり，コンピュータを利用し た社会基盤の安全性を保証することが早急に必要である．
すでに我々の周りには数多くの応用ソフトウェアが稼動しており， その多くに安全性の問題があると考えられている．それら個々の問 題を解決していくことは対症療法にすぎない．問題の根本は，これ らの応用ソフトウェアが，安全性の問題が社会的に顕在化する以前 に開発された基盤ソフトウェア(言語，OS) を利用している事にあ る．
本プロジェクトでは，型理論をはじめとするプログラムの静的解析 技術によって，既存の基盤ソフトウェアの信頼性を強化することを 通して，それらを使用する応用ソフトウェア全体の安全性を向上さ せることを目標とする．
プロジェクトの概要
本プロジェクトでは，今後の実施期間を含めて次の三つの方向性か ら上記の目標に取り組んでいる．
- 高安全なC言語コンパイラの開発
- 現在，システム記述に最も広く使われているC言語での，コンピュー タウィルス感染や情報漏洩の危険性のない，対攻撃耐性を持った コードを生成する高安全 Cコンパイラを開発する．
- OS用型付きアセンブリ言語の設計・実装
-
近年の静的プログラム解析，特に型理論の進歩により，「強く型 付けされた言語」(例:Javaバイトコード，O'Caml,等)が広く普及 している．これらの言語の長所の一つは，プログラムが実行時に エラーを生じないことを型検査によって保証できることである．
しかし，OS の作成には，未だ型理論の成果が応用されていな い．そこで本研究は，OSカーネルの記述に適した強く型付けさ れた言語「型付きアセンブリ言語 (TAL) 」を設計・実装し， OSカーネルをその TAL で記述することで，実行時にエラーを 生じない安全で高信頼なOS を実現することを目指す．
- 定理証明器によるOS安全性の形式的検証
- 通常のOS上では複数のプログラムが同時に動作しており，メモリやデバイスなどの共通 の資源を使用している．OSの仕事のひとつに，各プログラムが占有する資源の分離性の 保証，例えば，タスク分離性，あるプログラムの使用しているメモリが他のプログラム によって勝手に読み書きされない性質などがある．OSがそれらの仕事を正しく行うかど うかはコンピュータシステム全体の安全性にかかわる重要な問題であり，間違ったOSの 上では，たとえ個々のプログラムが正しく書かれていたとしてもそれらの安全性はまっ たく保証できない．にもかかわらず，現在までこのようなOSの安全性の検証はその複雑 性からあまり研究されてこなかった．この方面での形式的検証方法を確立するのが我々 の研究目的である．
関連公開ソフトウェア
- VITC: 脆弱性攻撃耐性コードを生成するC言語コンパイラ
- ビルド方法
- FailSafe-C に対するパッチ
(VITCは現在 FailSafe-Cに対する差分として開発されています。利用にあたってはFailSafe-Cのライセンスをご確認下さい。) - 以下のファイルは VITC のビルドに必要なライブラリ・パッチ群です。
- Fail-Safe C: メモリ安全なコードを生成するC言語コンパイラ
- applpi: 定理証明器Coq 用の並行プログラムを検証するライブラリ
- Kernel Mode Linux: ユーザプログラムをカーネルモードで安全に実行させるためのOS機構
- Seplog：定理証明器Coq 用のSeparation logic ライブラリ
- TALK: OS記述用型付アセンブリ言語の実装
- TOS: 型付アセンブリ言語で書かれたOSカーネル