| 研究概要 |
文字列解析に基づくウェブソフトウェアの検証に関して以下の研究を行った.
●スクリプト言語で記述されたプログラムでは,正則表現を用いたマッチングや文字列の置き換えが重要な役割を果たす.既存の文字列解析では,このような文字列操作をマッチングの戦略を無視した近似を用いることで解析を行っている.そのため,このような操作に対して高い精度の解析結果が得られていない.本研究では,戦略を考慮にいれた正則表現のマッチングの定式化をモナドの概念を用いて行い,その定式化に基づき出力付きオートマトンを構成する方法を与えた.
●HTMLの新しい規格として,HTML5の策定が進められている.HTML5では,HTML文書中の構文エラーの扱いを定めるなど,より詳細な仕様が決められている.一方,その仕様記述は非常に低いレベルの記述となっており,直感的な理解や理論的な扱いが困難になっている.そこで,本研究では,HTML5の構文規則の数学的定式化の研究を進めた.今年度には,字句解析の一部の定式化を行ったが,非常に仕様が複雑なため,適切な抽象度を再検討する必要がある.
●文字列解析によるコマンドインジェクション脆弱性の検査では,文字列操作によって生成される文字列のどの部分が,入力に影響を受けているかを解析する必要がある.先行研究では,出力付きオートマトンに対してこの解析を行っていたが,その解析が健全でないことが分かった.今年度には,この問題を解決するため,より抽象度の高い定式化を行い,この解析を行うことを目指した.
|
