2015 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 | 逆方向シミュレーション / ソフトウェア安全性検証 / 数値範囲分割 / ケース分岐シミュレーション / GPU並列処理 / MapReduce分散処理 |
|---|
| Outline of Annual Research Achievements |
ソフトウェアの安全性検証のため、バグや想定外動作を網羅的に検出する方法が望まれる。通常の入力条件に対するテストでは、検出できない可能性が残り、網羅的検出には条件数を無限大に増やす必要がある。そこで本研究では、異常等を意味する結果から、ソフトウェアを逆に辿って、それが発生する条件を探る方法を逆方向シミュレーションと呼び、その基本方式の確立と実現をはかることを目的としている。具体的に、静的に制御フローが確定しているJava言語のプログラムを検証対象としている。
初年度は、逆方向シミュレーションに必要な機能要素の実現と、処理時間を短縮するための並列分散処理の活用を中心的内容とした。まず、(1)Javaバイトコードごとの機能作成、(2)シミュレーション実行管理機能の実現、(3)順方向シミュレーションによる各機能の動作確認を行い、最後に(4)逆方向での分岐処理を含めたシミュレーション動作の実現を行った。
また、次年度に実施予定であったシミュレーションの高速化を実現する方法の検討も、先行して開始した。具体的には、GPUの並列処理ハードウェアを使用する方法と、多数のPCでMapReduce方式による分散処理を利用することを、それぞれプログラムを作成しながら検討した。いずれも、比較的簡単な逆方向シミュレーションで実現可能なFIRデコンボリューションで試みたが、扱う数値範囲の分割数と処理時間の関係に関する知見と効率化のアイデアが得られた。
|
| 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バイトコードを対象に、逆方向シミュレーションに必要な要素機能を作成し、プログラムの逆実行を実現すること、その上で無限ループや入力値不使用などの欠陥要因が発見可能なシミュレータを実現することである。
最初のシミュレーション要素機能については、整数処理に必要な機械語要素と最低限の制御要素について実現し、簡単なプログラムに対する逆方向シミュレーションを実現できた。無限ループ等の検出は今後の課題であるが、シミュレーション実行上の最大課題は、精度を高くして有効な結果を得るための変数数値範囲の細分化や、ループ逆流処理のために大量の分岐処理を行う必要があることである。その解決のための並列分散処理や効率化の工夫についても、進歩があった。
|
| Strategy for Future Research Activity |
検証可能なプログラムの範囲を拡大していきながら、機能上の課題を解決し、逆方向シミュレーションに必要となる機能、管理機能を整備していく。また、GPUによる並列処理、PC群による分散処理を組み合わせて、実際的な処理時間内に実行できることを目指す。また、外部の研究者の評価、協力を得ながら、実用的な方法として確立していきたい。
|
Research Products
(1 results)
