| 配分額 *注記 |
14,600千円 (直接経費: 14,600千円)
2003年度: 1,900千円 (直接経費: 1,900千円)
2002年度: 6,200千円 (直接経費: 6,200千円)
2001年度: 6,500千円 (直接経費: 6,500千円)
|
|---|
| 研究概要 |
本研究の目的は,ソフトウェアが安全に正しく動作することを型システムを用いて静的に検証することである.主要な研究成果は以下の通り.
1.並行プログラムの通信の整合性を検証するための型システムの構築
並行プログラムにおいては,通信部分の記述に誤りやセキュリティ上の欠陥が混入しやすい.本研究では,そのような通信部分の整合性がとれているかどうかを型システムに基づいてプログラム実行前に検証するための手法を確立した.
2.計算資源へのアクセス方法を検証するための型システムの構築
プログラム中で,ファイル・ネットワーク・メモリなどの計算資源を用いる際には,通常,システムコールやAPIといった形で資源毎に提供されている操作群を使う.これらの操作群に対しては通常,操作間の呼び出し順序なども決まっている。本研究では,そのような操作間の順序に関する正しさを型システムに基づいて実行前に検証する手法,資源使用解析,を確立した.
3.プログラムによる情報漏れを検証するための型システムの構築
欠陥のあるプログラムあるいはウィルスのような悪意のあるプログラムの実行によって,パスワードや銀行の口座番号など,コンピュータに管理されている情報が漏洩する可能性がある.本研究では実行形式のプログラムや並行プログラムを対象として,そのようなプログラムからの情報漏洩の可能性を型システムを用いて実行前に検証する手法を確立した.
4.定理証明器を用いた並行・分散プログラムの検証
本特定領域の複数の班で共同開発した安全メールサーバプログラムの核部分の正しさを定理証明器Coqを用いて検証するとともに,その知見をいかして,一般の並行プログラムを検証するためのライブラリ群を構築した.
|
