2019 Fiscal Year Research-status Report
Software Verification Based on the Theory of Transducers
| Project/Area Number |
19K11899
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | ソフトウェア検証 / トランスデューサ / オートマトン / 形式言語理論 / 文字列制約 |
|---|
| Outline of Annual Research Achievements |
本年度には，以下の研究を行なった．
＊文字列を操作するプログラムの検証の基盤となる直線形式文字列制約の充足可能性判定に関する研究を行なった．これまでの予備的な研究で，整数に関する制約を含まない純粋な文字列制約に関しては，ストリーミングトランスデューサが合成に関して閉じていることを利用すれば素朴な手続きで判定できることが分かっていた．この手法と，文字列制約をParikh写像を用いて整数制約に変換する手法と組み合わせ，以下の制約に関する充足可能性判定手続きを得た：正規言語への所属制約，ストリーミングトランスデューサによるトランスダクション，文字列長に関する整数制約．さらに，この手続きによるソルバをScalaにより実装し，既存のソルバと比較し，制約によってどのソルバが優れているかが分かれる結果を得た．
＊文字列の検索等に広く用いられる正規表現マッチングはその多くがバックトラックに基づくアルゴリズムで実装されており，対象文字列の長さに対して線形時間でマッチングを完了できない場合がある．これを事前に検知するために，マッチングに要する計算量を静的解析する手法が複数の先行研究によって提案されている．本研究では先行研究を拡張し，先読みや先頭/末尾のマッチなど，現実のソフトウェアで使用されている拡張された正規表現に対しても解析が行える手法を開発した．さらに，既存の解析アルゴリズムを高速化し，より実用的な速度で解析を行える手法を開発した．そして，これらの改良を施した計算量解析のツールをScalaで実装し，既存の実装よりも多くの正規表現が解析できることを実験により確認した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究で開発した文字列制約の充足可能性判定手続きは，既存の手続きより広いクラスの制約を扱うことができ有用性が高い．理論的にもストリーミングトランスデューサの枠組みで整理されており，今後の展開が期待できる．
正規表現マッチングの計算量解析については，先読み，後読み，後方参照をサポートをした初めての解析手法，ツールであり有用性，新規性が高い．
|
| Strategy for Future Research Activity |
文字列制約の充足可能性判定については，ストリーミングトランスデューサの等価性判定などの理論を用いて，扱える制約を拡張することを目指す．等価性判定の決定手続きを応用することで，等号否定を扱えるように拡張できる見込みである．
また，現実的な検証問題として，クロスサイトスクリプティング脆弱性への対抗技術である XSSAuditor のトランスデューサを用いた分析を進める．特に，交代性オートマトンの理論が応用できると考えている，
|
| Causes of Carryover |
コロナウイルスの感染拡大のため３月に予定していた研究発表のための国内出張が取りやめとなったため，次年度使用額が生じた．次年度には，在宅勤務で研究を進めるために必要な機器等の購入に使用する予定である．
|
