• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Verification of Web Software Based on String Analysis

Research Project

Project/Area Number 21500028
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field Software
Research InstitutionUniversity of Tsukuba

Principal Investigator

MINAMIDE Yasuhiko  筑波大学, システム情報系, 准教授 (50252531)

Project Period (FY) 2009 – 2011
Project Status Completed (Fiscal Year 2011)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2011: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2010: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2009: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Keywordsプログラム処理系 / ソフトウェア検証 / ウェブ / ソフトウェア / 情報基礎 / プログラム解析 / ソフトウエア検証 / プログララム解析 / ソフトウェア工学
Research Abstract

We have improved a program analysis called string analysis that can be applied to the detection of Web software vulnerabilities in the following respects. The readability of counter examples generated by the analysis is improved by constructing them as context-free grammars in a specific form. We have formulated the semantics of regular expression matching in programming languages, and enabled their precise analysis through the precise translation to transducers. For the analysis of a server-side program utilizing a database, we have improved its analysis by analyzing the constraint on data imposed by the program storing the data.

Report

(4 results)
  • 2011 Annual Research Report   Final Research Report ( PDF )
  • 2010 Annual Research Report
  • 2009 Annual Research Report
  • Research Products

    (22 results)

All 2012 2011 2010 2009 Other

All Journal Article (4 results) (of which Peer Reviewed: 4 results) Presentation (16 results) Remarks (2 results)

  • [Journal Article] Translating Regular Expression Matching into Transducers2012

    • Author(s)
      Yuto Sakuma, Yasuhiko Minamide, Andrei Voronkov
    • Journal Title

      Journal of Applied Logic

      Volume: 10 Issue: 1 Pages: 32-51

    • DOI

      10.1016/j.jal.2011.11.003

    • Related Report
      2011 Annual Research Report 2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Translating Regular Expression Matching into Transducers2011

    • Author(s)
      Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov
    • Journal Title

      Proc.International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2010)

      Pages: 107-115

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Rubyプログラムの制御フロー解析とその健全性の証明2010

    • Author(s)
      松本宗太郎, 南出靖彦
    • Journal Title

      情報処理学会論文誌:プログラミング

      Volume: 3 Pages: 9-25

    • NAID

      110007970972

    • URL

      http://id.nii.ac.jp/1001/00068444/

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Rubyプログラムの制御フロー解析とその健全性の証明2010

    • Author(s)
      松本宗太郎, 南出靖彦
    • Journal Title

      情報処理学会論文誌 プログラミング 3

      Pages: 9-25

    • NAID

      110007970972

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Presentation] HTML5構文解析のプッシュダウンオートマトンを用いた検証2012

    • Author(s)
      森俊介, 南出靖彦
    • Organizer
      プログラミングおよびプログラミング言語ワークショップ(ポスター)
    • Place of Presentation
      南紀白浜むさし(和歌山県)
    • Year and Date
      2012-03-08
    • Related Report
      2011 Final Research Report
  • [Presentation] 抽象DPLLのIsabelle/HOLによる形式化と検証2012

    • Author(s)
      武井裕也, 南出靖彦
    • Organizer
      プログラミングおよびプログラミング言語ワークショップ(ポスター)
    • Place of Presentation
      南紀白浜むさし(和歌山県)
    • Year and Date
      2012-03-08
    • Related Report
      2011 Final Research Report
  • [Presentation] 文字列解析によるクロスサイトスクリプティング脆弱性検査の改良2012

    • Author(s)
      木村将人, 南出靖彦
    • Organizer
      プログラミングおよびプログラミング言語ワークショップ(ポスター)
    • Place of Presentation
      南紀白浜むさし(和歌山県)
    • Year and Date
      2012-03-08
    • Related Report
      2011 Final Research Report
  • [Presentation] HTML5構文解析のプッシュダウンオートマトンを用いた検証2012

    • Author(s)
      森俊介, 南出靖彦
    • Organizer
      第14回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      南紀白浜温泉むさし,和歌山県南紀白浜(ポスター)
    • Year and Date
      2012-03-08
    • Related Report
      2011 Annual Research Report
  • [Presentation] 抽象DPLLのIsabelle/HOLによる形式化と検証2012

    • Author(s)
      武井裕也, 南出靖彦
    • Organizer
      第14回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      南紀白浜温泉むさし,和歌山県南紀白浜(ポスター)
    • Year and Date
      2012-03-08
    • Related Report
      2011 Annual Research Report
  • [Presentation] 文字列解析によるクロスサイトスクリプティング脆弱性検査の改良2012

    • Author(s)
      木村将人, 南出靖彦
    • Organizer
      第14回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      南紀白浜温泉むさし,和歌山県南紀白浜(ポスター)
    • Year and Date
      2012-03-08
    • Related Report
      2011 Annual Research Report
  • [Presentation] Semantics and Implementations of Regular Expression Matching2011

    • Author(s)
      Yasuhiko Minamide
    • Organizer
      The Eighth Asian Workshop on Foundation of Software
    • Place of Presentation
      上海交通大学(中国)
    • Year and Date
      2011-05-13
    • Related Report
      2011 Final Research Report
  • [Presentation] Formalizing Regular Expression Matching in Isabelle/HOL2010

    • Author(s)
      Yasuhiko Minamide
    • Organizer
      TPP'10 : 6th Theorem Proving and Provers Meeting
    • Place of Presentation
      名古屋大学(愛知県 )
    • Year and Date
      2010-11-26
    • Related Report
      2011 Final Research Report
  • [Presentation] Formalizing Regular Expression Matching in Isabelle/HOL2010

    • Author(s)
      Yasuhiko Minamide
    • Organizer
      TPP'10 : 6th Theorem Proving and Provers Meeting
    • Place of Presentation
      名古屋大学(愛知県)
    • Year and Date
      2010-11-26
    • Related Report
      2011 Final Research Report
  • [Presentation] Formalizing Regular Expression Matching in Isabelle/HOL2010

    • Author(s)
      Yasuhika Minamide
    • Organizer
      TPP'10 : 6th Theorem Proving and Provers Meeting
    • Place of Presentation
      名古屋大学
    • Year and Date
      2010-11-26
    • Related Report
      2010 Annual Research Report
  • [Presentation] The PHP String Analyzer2010

    • Author(s)
      Yasuhiko Minamide
    • Organizer
      IFIP Working Group 2.8
    • Place of Presentation
      Shirahama, Japan
    • Year and Date
      2010-04-13
    • Related Report
      2011 Final Research Report
  • [Presentation] Translating Regular Expression Matching into Transducers2010

    • Author(s)
      Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov
    • Organizer
      12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara
    • Place of Presentation
      Romania
    • Related Report
      2011 Final Research Report
  • [Presentation] 証明支援系Isabelle/HOLによるごみ集めアルゴリズムの形式化と安全性検証2009

    • Author(s)
      藤原拓也, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      島根大学(島根県)
    • Year and Date
      2009-09-16
    • Related Report
      2011 Final Research Report
  • [Presentation] Rubyのコア言語の操作的意味論2009

    • Author(s)
      松本宗太郎, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      島根大学(島根県)
    • Year and Date
      2009-09-16
    • Related Report
      2011 Final Research Report
  • [Presentation] 証明支援系Isabelle/HOLによるごみ集めアルゴリズムの形式化と安全性検証2009

    • Author(s)
      藤原拓也, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      島根大学
    • Year and Date
      2009-09-16
    • Related Report
      2009 Annual Research Report
  • [Presentation] Rubyのコア言語の操作的意味論2009

    • Author(s)
      松本宗太郎, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      島根大学
    • Year and Date
      2009-09-16
    • Related Report
      2009 Annual Research Report
  • [Remarks]

    • URL

      http://www.score.cs.tsukuba.ac.jp/~minamide/phpsa

    • Related Report
      2011 Final Research Report
  • [Remarks] 南出靖彦, 講義「Webプログラムの脆弱性と静的検査」, 2012年1月5日, お茶の水女子大学理学部情報科学科

    • Related Report
      2011 Final Research Report

URL: 

Published: 2009-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi