| 研究概要 |
文字列解析に基づくウェブソフトウェアの検証に関して以下の研究を行った.
(1)文字列解析を応用したクロスサイトスクリプティング脆弱生検査を,いくつかの観点から改良した.データベースと連携するサーバサイドプログラムの検査では,データベースのスキーマ及びデータを格納するプログラムから,データベースに関する制約を求めることで,これまでに比べ格段に精密な解析が可能になった.また,クロスサイトスクリプティング脆弱生の検査と反例生成の仕組みを,トランスデューサを用いて再構成し柔軟な検査を可能とした.これらの改良をPHP文字列解析器上に実装し,評価を行った.
(2)前年度にまでに行ったプログラミング言語で用いられる正規表現マッチングの意味論の研究をモナドやモナドトランスフォーマを用いて定式化することで,より洗練された意味論を構築した.モナドトランスフォーマを用いて意味論を段階的に詳細化することで,出力付きオートマトンの構成法の見通しの良い正当性証明を与えることができた.
(3)HTML5構文仕様を形式化する研究を行った.HTML5構文仕様は,スタックを用いた複雑なアルゴリズムとして自然言語により記述されている.本研究では,遷移の条件としてスタックの内容を正則言語で検査できる条件付きプシュダウンオートマトンとして,このアルゴリズムの形式化を行った.この形式化は,文脈自由言語のHTML5構文に対する妥当性検査アルゴリズムの設計の基礎となる.
|
