2016 Fiscal Year Research-status Report
ソフトウェアの欠陥発見のための逆方向シミュレーション
| Project/Area Number |
15K11989
|
|---|
| Research Institution | Yamagata University |
|---|
Principal Investigator |
平中 幸雄 山形大学, 大学院理工学研究科, 教授 (40134465)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 逆方向シミュレーション / ソフトウェア安全性検証 / シンボリック逆実行 / 範囲分割逆モデル / Java機械語 / オーバフロー対応 / シミュレーション実行監視 |
|---|
| Outline of Annual Research Achievements |
ソフトウェアの安全性検証のため、網羅的にバグや想定外動作を検出する方法が望まれる。入力を変えながら探す方法では場合数が膨大になるが、出力結果からプログラムを逆算すると、より効率的に判断できる場合が多い。本研究は、そのための逆方向シミュレータを、Java機械語を対象に実現するのが目的である。初年度は、機械語要素の順方向及び逆方向処理の基本機能の実現、変数で状態を表すシンボリック処理方式の試行、シミュレーションを分散処理で高速化するためのMapReduce及びGPGPUによる方法に取り組んだ。
今年度は、シンボリック処理方式で大部分の機械語処理を実現し、Javaソースコードのコンパイルから自動実行できるプログラムを開発した。ただし、シンボリック実行では各機械語の演算が正確に行われることを前提にしていて、オーバフローなどの発生も含めて、より網羅性を持たせるため、数値的に行う方法も開発した。具体的に整数加算の逆算を範囲分割法と分岐処理で実現し、高速化のための方法として、範囲分割数を段階的に増やしていく、範囲を指数分割する、可能性の高いケースから探索するなどの工夫を行い、短いサンプルプログラムで実用的な処理時間も可能なことをを確認した。
分散処理による高速化では、MapReduce、GPGPUともに処理粒度と実行管理に課題があり、現在はマルチスレッドの利用を検討している。また、実行監視のため、Pure Dataのようなツールの利用を検討したが、作成したシミュレータに適合可能な方法としてデスクトップ上でのシミュレータ構築・実行方法を検討中である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の全体目標は、Javaバイトコードを対象に、逆方向シミュレーションに必要な要素機能を作成し、プログラムの逆実行を実現することである。その上で無限ループや入力値不使用の欠陥要因などが発見可能なシミュレータを実現することである。
これまでに、大部分のJava機械語に対して、シンボリックな順実行及び逆実行が可能なシミュレータを作成した。そのシミュレーションの結果では、出力結果に影響のない変数を明らかにすることができた。さらに、限られた機械語に対してだけであるが、オーバフローなどの対応も可能な数値範囲分割方式の逆方向シミュレータも実現でき、処理時間の短縮を可能とする効率的な方法も開発した。今後、無限ループの検出方法を明確化できれば、当初の目標はほぼ実現できると考えている。
|
| Strategy for Future Research Activity |
最終年度では、残る機械語命令の組み込みを行いながら、ループ逆算の把握と実行管理、マルチスレッドによる分散処理と同期方法の実現、グラフィカルインタフェースによるシミュレータ実現と実行管理を行っていきたい。その上で、本研究の逆方向シミュレーションの意義、将来性、課題の分析と評価を行い、ソフトウェアの網羅的安全検証方法としての実用性を確立していきたい。
|
