文字列解析に基づくウェブソフトウェアの検証

2011 年度 研究成果報告書

• 研究課題/領域番号: 21500028
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 筑波大学
• 研究代表者: 南出 靖彦 筑波大学, システム情報系, 准教授 (50252531)
• 研究期間 (年度): 2009 – 2011
• キーワード: プログラム処理系 / ソフトウェア検証 / ウェブ

研究概要

ウェブソフトウェアの脆弱性検査に応用される文字列解析と呼ばれるプログラム解析を以下の点で改良した.検査結果として得られる反例を特殊な文脈自由文法として構成することで, 反例の可読性を高めた.スクリプト言語で重要な役割を果たす正規表現マッチングの意味論をモナドを用いて定式化し, その意味論からトランスューサを構成することで, 正規表現マッチングの正確な解析を可能とした.データベースと連携するサーバサイドプログラムの検査おいては, データベースに関する制約を求めることで解析の精密を大きく向上した.

研究成果

• [雑誌論文] Translating Regular Expression Matching into Transducers (2012)
  • 著者名/発表者名: Yuto Sakuma, Yasuhiko Minamide, Andrei Voronkov
  • 雑誌名: Journal of Applied Logic 巻: 10 ページ: 32-51
  • DOI: DOI:10.1016/j.jal.2011.11.003
  • 査読あり
• [雑誌論文] Rubyプログラムの制御フロー解析とその健全性の証明 (2010)
  • 著者名/発表者名: 松本宗太郎, 南出靖彦
  • 雑誌名: 情報処理学会論文誌:プログラミング 巻: 3 ページ: 9-25
  • URL: http://id.nii.ac.jp/1001/00068444/
  • 査読あり
• [学会発表] HTML5構文解析のプッシュダウンオートマトンを用いた検証 (2012)
  • 著者名/発表者名: 森俊介, 南出靖彦
  • 学会等名: プログラミングおよびプログラミング言語ワークショップ(ポスター)
  • 発表場所: 南紀白浜むさし(和歌山県)
  • 年月日: 2012-03-08
• [学会発表] 抽象DPLLのIsabelle/HOLによる形式化と検証 (2012)
  • 著者名/発表者名: 武井裕也, 南出靖彦
  • 学会等名: プログラミングおよびプログラミング言語ワークショップ(ポスター)
  • 発表場所: 南紀白浜むさし(和歌山県)
  • 年月日: 2012-03-08
• [学会発表] 文字列解析によるクロスサイトスクリプティング脆弱性検査の改良 (2012)
  • 著者名/発表者名: 木村将人, 南出靖彦
  • 学会等名: プログラミングおよびプログラミング言語ワークショップ(ポスター)
  • 発表場所: 南紀白浜むさし(和歌山県)
  • 年月日: 2012-03-08
• [学会発表] Semantics and Implementations of Regular Expression Matching (2011)
  • 著者名/発表者名: Yasuhiko Minamide
  • 学会等名: The Eighth Asian Workshop on Foundation of Software
  • 発表場所: 上海交通大学(中国)
  • 年月日: 2011-05-13
• [学会発表] Translating Regular Expression Matching into Transducers (2010)
  • 著者名/発表者名: Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov
  • 学会等名: 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara
  • 発表場所: Romania
  • 年月日: 20100923-26
• [学会発表] Formalizing Regular Expression Matching in Isabelle/HOL (2010)
  • 著者名/発表者名: Yasuhiko Minamide
  • 学会等名: TPP'10 : 6th Theorem Proving and Provers Meeting
  • 発表場所: 名古屋大学(愛知県 )
  • 年月日: 2010-11-26
• [学会発表] Formalizing Regular Expression Matching in Isabelle/HOL (2010)
  • 著者名/発表者名: Yasuhiko Minamide
  • 学会等名: TPP'10 : 6th Theorem Proving and Provers Meeting
  • 発表場所: 名古屋大学(愛知県)
  • 年月日: 2010-11-26
• [学会発表] The PHP String Analyzer (2010)
  • 著者名/発表者名: Yasuhiko Minamide
  • 学会等名: IFIP Working Group 2.8
  • 発表場所: Shirahama, Japan
  • 年月日: 2010-04-13
• [学会発表] 証明支援系Isabelle/HOLによるごみ集めアルゴリズムの形式化と安全性検証 (2009)
  • 著者名/発表者名: 藤原拓也, 南出靖彦
  • 学会等名: 日本ソフトウェア科学会第26回大会
  • 発表場所: 島根大学(島根県)
  • 年月日: 2009-09-16
• [学会発表] Rubyのコア言語の操作的意味論 (2009)
  • 著者名/発表者名: 松本宗太郎, 南出靖彦
  • 学会等名: 日本ソフトウェア科学会第26回大会
  • 発表場所: 島根大学(島根県)
  • 年月日: 2009-09-16
• [備考]
  • URL: http://www.score.cs.tsukuba.ac.jp/~minamide/phpsa
• [備考] 南出靖彦, 講義「Webプログラムの脆弱性と静的検査」, 2012年1月5日, お茶の水女子大学理学部情報科学科