ソフトウェアの安全性向上のための型理論
【研究分野】ソフトウエア
【研究キーワード】
プログラム検証 / プログラム解析 / 型理論 / 関数型プログラム / 並行プログラム / 情報流解析 / 型システム / デッドロック / 資源使用法解析 / プログラム等価性 / 線形最適化問題 / 割り込み / 双模倣 / プログラム変換 / XML
【研究成果の概要】
本研究の目的は,ソフトウェアの信頼性向上のため,型理論などの数理科学的手法に基づいたプログラムの検証手法を発展させることにあった.特に,これまでの申請者らによる検証手法を改良・発展させ,現実のプログラムの検証を可能にすることに主眼をおいた.
3年間の主要な成果は以下のとおり.以下のいずれの研究においても実際にプログラム検証器のプロトタイプを作成し有効性を確認している.
1.関数型プログラムの検証手法
以前から,ファイルやメモリなどの計算資源を正しいプロトコルでアクセスするかどうかを検証するための資源使用法解析について研究を行っていたが,例外処理機構を扱っていないなど,実際のプログラミング言語とは開きがあった.そこで,従来の我々の検証手法を拡張し,例外処理機構に対応できるようにした.また,従来の型を用いた自動検証手法では,一般に解析精度が粗かったため,依存型の自動推論手法を考案することにより,精度のよい解析を自動で行えるようにした.
2.並行プログラムの検証手法
以前からπ計算を対象として,デッドロックなどの自動解析手法を研究していたが,実用化する上での解析精度,実際の言語が提供するプリミティブとの開きなどがあった.そこで,前者の問題をモデル検査などとの融合によって改善した.また,後者の問題に対処するため,ポインタや割り込みなどが入った言語に対する解析手法も考案した.
3.情報流解析
プログラムが機密情報を漏らさないかどうかを検証する情報流解析について研究を行った.従来から型を用いた情報流解析手法は提案されていたが精度が問題だったため,本研究ではモデル検査手法と融合させることにより,高速かつ精度のよい解析を可能にした.
【研究代表者】