2017 Fiscal Year Annual Research Report
Backward simulation for software defect discovery
| Project/Area Number |
15K11989
|
|---|
| Research Institution | Yamagata University |
|---|
Principal Investigator |
平中 幸雄 山形大学, 大学院理工学研究科, 教授 (40134465)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | ソフトウェア安全性検証 / 逆方向シミュレーション / 逆実行モデル / 数値範囲分割 / シンボリック逆実行 / Java bytecode |
|---|
| Outline of Annual Research Achievements |
情報化社会はソフトウェアに依存しているが、そのソフトウェアの安全性検証は困難な技術テーマである。そこで、本研究ではこれまでと異なる逆方向シミュレーションを使ったソフトウェアの網羅的安全性検証を研究した。
通常のソフトウェアテストは個々のテストデータに対する出力を検証するため、網羅性に欠ける。データを数値範囲でまとめてテストする方法や、変数と演算記号を使ってシンボリックにトレースすることで網羅性の確保が期待できるが、プログラムによっては膨大なケース数を取り扱う必要が出てくる。しかし、異常値など特定の出力値に対する入力条件を求めることは、逆算を使えば効率良くできることもある。そこで、プログラムの最後から逆方向にたどっていく方法を研究した。
実際に、Java プログラムを対象に、機械語命令に相当するJavaバイトコードを逐次逆実行しながら、プログラム中のバグや誤動作要因を検知できる逆方向シミュレータを実現した。逆実行では個々の機械語命令の逆処理が必要になり、２入力１出力命令では原理的に不可能に見えるかもしれないが、演算結果を特定すればそれに対応する入力の組み合わせは有限になり、順次試していけば、最終的に可能な入力値組み合わせだけが残る。実際に数値範囲分割法として、数値を範囲で扱い、範囲を段階的に細分していくことで能率良く検証を行う方法を実現した。
数値範囲分割法ではオーバフローも検証対象にできる利点があるが、計算時間が長くなりやすい弱点がある。そこでデータに名前を付け、演算を記号的に処理するシンボリック法による逆方向シミュレーションも開発した。シミュレーション後に条件式の評価を行うことになるが、実際にプログラムに適用して有効な検証が行えた。今後の課題として、機械語命令に依存して数値範囲分割法とシンボリック法を選択、組み合わせる方法の開発がある。
|
