2017 Fiscal Year Annual Research Report
Verifying safety properties of embedded assembly program using innovative software model checking
| Project/Area Number |
15K00093
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
櫻井 孝平 金沢大学, 電子情報学系, 助教 (80597021)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 動的プログラム解析 / SMT / 抽象化精錬 |
|---|
| Outline of Annual Research Achievements |
本研究では，組込みアセンブリプログラムを対象として、革新的ソフトウェアモデル検査手法を開発して、その検証実験を行った．その研究実績の概要は以下である．
(1)割込み処理が埋め込まれた組込みアセンブリプログラムを動的なプログラム解析する．その動的プログラム解析の中で，アセンブリプログラムの枝刈りやビット列の抽象化精錬，実行時間見積もりなどを行って，アセンブリプログラムから，状態爆発を抑制したモデルの構築手法を開発した．その成果はジャーナルに投稿し採録されて、掲載中である．
(2)抽象化精錬とＳＭＴ有界モデル検査手法を融合した抽象化精錬型ＳＭＴモデル検査手法を開発した．具体的には、抽象化器（抽象化述語により，抽象モデル及びその精錬モデルを構築する）、ＳＭＴ有界モデル検査器（ビット列の背景理論を用いたＳＭＴ有界モデル検査器）、ＳＭＴ反例解析器、クレイグの補間定理による精錬器（偽反例を無くすために，クレイグの補間定理を用いて，ＳＭＴソルバで，精錬用述語を発見する）から構成される．そのプロトタイプを実装した．なお、その成果は、現在、国際会議に投稿中である．
(3) (1)と(2)からなる組込みアセンブリプログラムのソフトウェアモデル検査器により，小規模な組込みアセンブリプログラムのスタックオーバーフローや割込み多重化の安全性などのハードウェア依存の検証性質の検証実験を行った．なお、現在、実用レベルのプログラムの実験を行っている．
|
