研究課題
本研究は、線形計画法と型理論を応用した並行ソフトウェアの安全性を検証する研究である。具体的には「分数権限計算」(Fractional Capaility Calculs)という新しい概念を含んだ型システムを構築し、型推論問題を線形計画問題に帰着することにより高速に自動ソフトウェア検証を行う。本年度は、以下の成果が得られた。1. バッファ使用量の検証MPIプログラムなど、プロセス同士がメッセージパッシングで通信・同期をとる並行プログラムでメッセージがバッファされる場合、バッファが限度サイズ以上使用されると、バッファオーバーフローが起きたり例外が発生するなどの問題がある。このようなソフトウェアに対し、型推論と線形計画法を用いてバッファの使用量上限を求めるという多項式時間のアルゴリズムを開発した。2. レースコンディンションの防止マルチスレッドプログラムにおいて、異なるスレッドが共有変数を同時にアクセスし、少なくとも一方がその変数に書き込んでいる状態をレースコンディンションと呼ぶ。我々は、型推論と線形計画法を用い、プログラム実行時にレースが起こらないか検証する多項式時間のレース検証アルゴリズムを開発した。従来のレース検証アルゴリズムに比べ、セマフォやシグナルなどロック以外の同期プリミティブにも対応するなど、性能の向上に成功した。3. Observation Determinismの検証機密情報を含んだ並行ソフトウェアにおいて、スレッドのスケジューリングから外部に機密情報が漏洩してしまう場合がある。機密情報が漏洩しないことを保障する十分条件の一つに、Observational Determinismという概念がある。Observation Detarminismは、外部から見える実行結果が機密情報にもスレッドのスケジューリングにも依存しないという性質である。我々は、型推論と線形計画法を応用することによってメッセージパッシングなどを含んだ幅広い並行ソフトウェアのObservational Determinismを効率的に(多項式時間で)検証することに成功した。
すべて 2008
すべて 雑誌論文 (3件) (うち査読あり 3件)
Proceedings of the 17th European Symposium on Programming(ESOP 2008) 4960
ページ: 284-298
Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation(PLDI 2008)
ページ: 1-10
Proceedings of the 21st IEEE Computer Security Foundations Symposium(CSF 2008)
ページ: 287-300
