2010 Fiscal Year Annual Research Report
型理論と線形計画法によるマルチスレッドプログラムの安全性検証
| Project/Area Number |
20700019
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
寺内 多智弘 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| Keywords | ソフトウェア検証 / 型理論 / 型推論 / 線形計画法 / 権限計算 |
|---|
| Research Abstract |
本研究は、線形計画法と型理論を応用した、並行ソフトウェアの安全性(例えば、レースが起こらないなど)を検証する研究である。具体的には「分数権限計算」(Fractional Capabbity Calculus)という新しい概念を含んだ型システムを構築し、型推論問題を線形計画問題に帰着することにより高速に自動ソフトウェア検証を行う。
本年度は、以下の成果が得られた。
1.量的情報流の検証
20年度に我々が行った分数権限計算を用いたプログラム検証の応用のひとつに機密情報を扱うプログラムの情報漏えいを静的に検証するという「情報流」の検証がある。この研究の発展として、情報漏えいの有無だけでなく、その量を見積もる「量的情報流」の検証の研究を行った。具体的にはシャノンのエントロピー、minエントロピー、など既存研究で提案された量的情報流の定義に従い量的情報流を自動的に検証することの困難性(計算量理論的困難性など)を明らかにし、効果的な検証方法(量的でない情報流解析に用いられるself compositionの技法の応用)を提案した。
2.効率的な文脈依存解析
文脈依存なプログラム解析は、関数の出現の文脈を考慮するため、文脈非依存な解析より正確であるが、効率よく解析を行うのが難しいとされていた、我々は、「Thread-based code cloning」という古典的code cloningを発展させた並列プログラム解析に特化した文脈依存プログラム手法を開発し、上記の分数権限計算によるレース解析に応用した。
|
