2005 Fiscal Year Annual Research Report
型システムとモデル検査の融合によるソフトウェア検証
| Project/Area Number |
16650004
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| Keywords | 型システム / プログラム検証 / プログラム解析 / モデル検査 / 情報流解析 / 資源使用法解析 |
|---|
| Research Abstract |
本研究では、プログラム検証のための代表的な手法である型システムとモデル検査の技術を融合して新しい検証手法を確立することを目指している.本年度の主な研究成果は以下のとおり.
1.型システムとモデル検査技術の融合による新しい情報流解析手法の考案
プログラムが機密情報を漏洩しないかどうかを静的に(プログラム実行前に)検証する手法として,型システムを用いる手法,モデル検査器を用いる手法がそれぞれ提案されていた.しかしながら,型システムを用いる手法は解析が粗すぎて安全なプログラムを危険と判断してしまうという欠点,モデル検査を用いる手法は検証時間がかかりすぎるという欠点があった.本研究では,まずはじめにどのような経路で情報漏れが起きる可能性があるかを型システムを用いて発見し,その後モデル検査器を用いて,実際にその経路で情報漏れが起きるかどうかを判定するという新しい手法を考案した.新しい手法では型システムではできなかった情報漏れが実際に起きるケースを発見することができ,また,モデル検査だけを用いる手法よりも高速に発見することができる.
2.計算資源使用法解析の拡張
従来から研究をすすめてきたファイルやメモリ,ネットワークなどの計算資源の使用法を解析する手法の改良を行った.対象言語として,(1)例外処理機構を持つ関数型言語,(2)並行言語,の2つについてそれぞれ解析手法を研究した.いずれの手法も,まず型システムを用いて各計算資源の使われ方を表す抽象プログラムを取りだし,その抽象プログラムが資源の使われ方に関する仕様を満たしていることを一種のモデル検査によって検証を行う.
|
