JavaScriptを含んだHTML文書に対する データフロー解析を用いた構文検証手法の提案 鷲尾 和則†, 松下 誠‡, 井上 克郎‡ †大阪大学大学院基礎工学研究科 ‡大阪大学大学院情報科学研究科

背景 インターネットの普及によりHTML文書が多数作成されている タグ付け規則に従ってHTMLを記述することが必要 タグ付け規則はDTD(文書型定義)に定義されている HTML文書にJavaScriptを記述することが頻繁にある JavaScriptは任意のHTML文書の断片を出力することが可能である 既存のHTML構文検証ツールはJavaScriptの内容を無視する

目的 JavaScriptの内容を考慮してHTML文書の構文検証を行う タグ付け規則通りに正しく記述されているか

以前提案した手法 JavaScriptの内容を考慮したHTML文書の構文の検証方法を提案した

問題点 JavaScriptの実行結果(出力内容)は動的に変わり得る 実行するたびに検証結果が変わり得る すべての実行結果について検証する必要がある 現実的ではない

新しい手法の提案 JavaScriptの出力文字列を正規表現を用いてパターン化 パターンについて検証を行う 選択　　　→　｜ 繰り返し　→　＊ パターンについて検証を行う 何度も実行しなくとも，すべての実行結果について検証することができる

対象 HTMLは構文検証について曖昧な点がある 厳密に定義されたXMLで記述されたXHTML文書を検証の対象とする JavaScriptは特定のブラウザに固有のメソッドなどが含まれる ECMAによって標準化されているECMAScriptを対象とする

検証手法 入力：ECMAScriptを含むXHTML文書 出力：検証結果 次の３フェーズからなる フェーズ１：XHTML文書解析 フェーズ２：スクリプト解析 フェーズ３：パターンの構文検証 構文解析 抽出 XHTML文書 DOMツリー ECMAScript パターン化 A*(B|C) 検証 パターン DTD

検証手法 入力：ECMAScriptを含むXHTML文書 出力：検証結果 次の３フェーズからなる フェーズ１：XHTML文書解析 フェーズ２：スクリプト解析 フェーズ３：パターンの構文検証 構文解析 抽出 XHTML文書 DOMツリー ECMAScript パターン化 A*(B|C) 検証 パターン DTD

検証手法 入力：ECMAScriptを含むXHTML文書 出力：検証結果 次の３フェーズからなる フェーズ１：XHTML文書解析 フェーズ２：スクリプト解析 フェーズ３：パターンの構文検証 構文解析 抽出 XHTML文書 DOMツリー ECMAScript パターン化 A*(B|C) 検証 パターン DTD

検証手法 入力：ECMAScriptを含むXHTML文書 出力：検証結果 次の３フェーズからなる フェーズ１：XHTML文書解析 フェーズ２：スクリプト解析 フェーズ３：パターンの構文検証 構文解析 抽出 XHTML文書 DOMツリー ECMAScript パターン化 A*(B|C) 検証 パターン DTD

フェーズ１ XHTML文書についてXML構文解析を行う 構文解析結果はDOMツリー 要素の親子関係などが判定できる スクリプトはスクリプト要素として解析されるが，スクリプトの中身は単なるテキストデータとみなされる

フェーズ２ –概要– フェーズ１で得られたスクリプトに対して次の解析を行う Step1. 構文解析および意味解析を行う

フェーズ２ –Step1– Step1. 構文解析 / 意味解析 ECMAScriptの言語仕様(ECMA-262)に基づいて字句解析と構文解析を行う 解析結果は抽象構文木 １で得られた抽象構文木に対し，意味解析を行う

フェーズ２ –Step2– Step2. データフロー解析 抽象構文木をルートから順に辿りながら 変数の代入・参照関係がわかる 変数が定義された　→　変数表に追加 変数が参照された　→　変数表を参照．定義されている位置を判定し，変数とその位置を記したリストを作る． 変数の代入・参照関係がわかる

フェーズ２ –Step3(パターンとは)– Step3. 出力文字列のパターン化 パターンとは？ if文の条件分岐により、一方の実行経路では”A”という文字列が、他方の実行経路では”B”という文字列が出力される 双方をまとめて記述する A | B ・・・ A または B (正規表現を用いたパターン) while文などの繰り返し文 ex) C* (Cの繰り返し)

フェーズ２ –Step3(パターン化の方法)– １で得られた関係をもとに変数の値を求める 動的にその値が定まるものは不定値とする 変数の型を値として代用する クラスライブラリ(のメソッド)を用いた処理があった場合，不定値とする ２で求められた値について それぞれのブロックで出力される文字列を括弧でくくる 出力文がif文など選択文の制御下にあれば | を付加する 出力文がwhile文など繰り返し文の制御下にあれば * を付加する

フェーズ２ –パターン化例– “<B>”, int, “</B>” a = Math.floor(Math.random()*10); b = “hoge”; if (a>5) { document.write(“<B>”); document.write(a); document.write(“</B>”); } else { for (i=0;i<10;i++) { document.write(“<C>”); document.write(b); document.write(“</C>”); } “<B>”, int, “</B>” “<C>”, “hoge”, “</C>” (“<C>”, “hoge”, “</C>”)* (“<B>”, int, “</B>”) | (“<C>”, “hoge”, “</C>”)*

フェーズ３ –概要– パターンの構文検証 開始タグと終了タグの対応付け 要素パターンの検証 フェーズ２で得られた出力文字列のパターンについて、そこから開始タグと終了タグを対応付け、要素のパターンにする 要素パターンの検証 要素のパターンについて検証を行う

フェーズ３ –タグの対応付け– 開始タグと終了タグの対応付け 開始タグと終了タグに何も付加されていない そのまま対応付け 開始タグと終了タグに | が付加されている すべての組み合わせについて対応付け 開始タグと終了タグに * が付加されている 要素のネスト <A>...</A> 要素A (<A>|<B>)...(</B>|</C>) 要素B (<C>)*...(</C>)* 要素Cのネスト

フェーズ３ –要素パターンへの変換– 開始タグと終了タグの対応付け 対応付けの例 出力文字列パターンについて最も内側の括弧から先述の対応付けを行う 対応付けができた要素を判定する 対応付けができなくなったら、括弧に｜や＊が付いている場合、２で得られた要素に付加する 外側の括弧へ移行し対応付けを行う この時対応付けできた要素は、３の要素パターンの親要素 ※不定値についてはテキストデータとみなす 対応付けの例 “<A>”,((“<B>”,”</B>”)|(“<C>”,”</C>”)*),”</A>” “<A>”,(( B )|( C )*),”</A>” “<A>”,( B | C* ),”</A>” “<A>”, B | C* ,”</A>” A B |C*

フェーズ３ –要素パターンの検証– 要素パターンの構文検証 １によりすべての要素について、その子要素をパターンで表すことができる それぞれの要素の子要素パターンについて、DTDで定義されたパターン(正規表現)と検証する 正規表現の包含関係判定問題 要素パターンがDTDの定義パターンに含まれれば違反していない 違反するパターンがあれば，データフロー解析の結果から違反を起こす実行経路 (危険なパス) を提示する 不定値に由来するテキストが含まれる場合は，条件付きで検証を行う 違反しない　＝　不定値にタグが含まれない場合のみ

フェーズ３ –パターン検証(包含判定)– 正規表現の包含判定 簡単化のため要素パターンの側で以下の置き換えを行う 　　　a* = ε| a | aa DTDで用いられる繰り返しの正規表現 a? : 0 回 or 1 回 a* : 0 回以上 a+ : 1 回以上

検証例 –あいさつスクリプト– var a = “good morning” var b = “good afternoon” Date day = new Date(); document.write(“<UL>”) if(day.getHour() < 12){ document.write(“<LI>”); document.write(a); document.write(“</LI>”); }else{ document.write(b); } document.write(“</UL>”); “<UL>”, (( “<LI>” , ”good morning” , ”</LI>” ) | ”good afternoon” ) , ”</UL>”

検証例 –検証内容– 検証 UL要素の子要素はLI+(1回以上のLI要素) LI要素の子要素は#PCDATA(テキスト) テキストは違反する LI要素の子要素は#PCDATA(テキスト) テキストは違反しない UL要素の子要素としてテキストが来る場合、違反する else 節の変数 b が違反 UL要素の子要素は ( LI要素 | テキスト ) LI要素の子要素はテキスト

検証例 –検証結果(危険なパス)– var a = “good morning” var b = “good afternoon” Date day = new Date(); document.write(“<UL>”) if(day.getHour() < 12){ document.write(“<LI>”); document.write(a); document.write(“</LI>”); }else{ document.write(b); } document.write(“</UL>”); DTD違反となる実行経路

本手法の有効性 本手法が有効な場合 本手法が有効でない場合 出力文字列は静的に定まる 実行経路が複数ある (不定である) 出力文字列が動的に定まる (不定値が含まれる)

まとめ ECMAScriptを含むXHTML文書について，スクリプトの出力文に対してデータフロー解析を行い，出力文字列をパターン化し，そのパターンを検証することで，構文の検証を行う手法を提案した 本手法により，ECMAScriptのすべての実行結果について，構文を検証することができる XML処理プログラムが出力するXML文書に対しても，同様の方法で検証できる

今後の課題 本手法をシステムに実装し，検証精度などについて評価を行う必要がある