Modeling and verification of web software based on theories symbolic computation

• Project/Area Number: 20300001
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Fundamental theory of informatics
• Research Institution: University of Tsukuba
• Principal Investigator: IDA Tetsuo 筑波大学, システム情報系, 教授 (70100047)
• Co-Investigator(Kenkyū-buntansha): MINAMIDE Yasuhiko 筑波大学, システム情報系, 准教授 (50252531) ; MARIN Mircea 筑波大学, システム情報系, 講師 (60396603) ; SUSUKI Taro 会津大学, コンピュータ理工学部, 准教授 (90272179)
• Project Period (FY): 2008 – 2011
• Project Status: Completed (Fiscal Year 2011)
• Budget Amount: ¥19,110,000 (Direct Cost: ¥14,700,000、Indirect Cost: ¥4,410,000); Fiscal Year 2011: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000); Fiscal Year 2010: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2009: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000); Fiscal Year 2008: ¥7,150,000 (Direct Cost: ¥5,500,000、Indirect Cost: ¥1,650,000)
• Keywords: ソフトウェア検証 / 記号計算 / ウェブ / 情報基礎 / ソフトウェア / 検証 / ソフトウェア学

Research Abstract

As a case study of Web software verification, we have verified the core of WebEos. The effective verification was conducted by utilizing some results of the computation conducted on Mathematica. With respect to the verification based on string analysis, we developed the method to precisely analyze regular expression matching. By introducing the analysis of communication to database, we enabled the detection of stored XSS. We designed and implemented an algorithm of greedy regular expression matching based on position automata.

Research Products

• [Journal Article] Translating Regular Expression Matching into Transducers (2012)
  • Author(s): Yuto Sakuma, Yasuhiko Minamide, Andrei Voronkov
  • Journal Title: Journal of Applied Logic Volume: 10 Pages: 32-51
  • Peer Reviewed
• [Journal Article] Design and Implementation of New Generation Data Format for Lunar and Planetary Exploration (2012)
  • Author(s): Taro SUZUKI, Junya TERAZONO, Takafumi HAYASHI
  • Journal Title: JSASS on-line journal Aerospace Technology
  • NAID: 130003373361
  • Peer Reviewed
• [Journal Article] Design and Implementation of New Generation Data Format for Lunar and Planetary Exploration (2012)
  • Author(s): Taro SUZUKI, Junya TERAZONO, Takafumi HAYASHI
  • Journal Title: JSASS on-line journal "Aerospace Technology" Volume: (to appear)
  • NAID: 130003373361
  • Peer Reviewed
• [Journal Article] Morley's theorem revisited : Origami construction and automated proof (2011)
  • Author(s): Ida. T, Kasem. A, Ghourabi. F, Takahashi. H
  • Journal Title: Journal of Symbolic Computation Volume: vol. 46 Pages: 162-170
  • NAID: 120007130912
  • Peer Reviewed
• [Journal Article] Proof Assistant Decision Procedures for Formalizing Origami (2011)
  • Author(s): Kaliszyk. C, and Ida. T
  • Journal Title: Lecture Notes in Computer Science (proceedings of the Conference on Intelligent Computer Mathematics (CICM' 11)) Volume: 6824 Pages: 45-57
  • Peer Reviewed
• [Journal Article] Proof Documents for Automated Origami Theorem Proving (2011)
  • Author(s): Ghourabi. F, Ida. T, and Kasem. A
  • Journal Title: Lecture Notes in Computer Science (post-proceeding of the 8th International Workshop on Automated Deduction in Geometry (ADG 2010)) Volume: 6877 Pages: 78-97
  • Peer Reviewed
• [Journal Article] Origami Axioms and Circle Extension (2011)
  • Author(s): Kasem. A, Ghourabi. F, Ida. T
  • Journal Title: Proceedings of the 26th Symposium on Applied Computing (SAC 2011) Pages: 1106-1111
  • Peer Reviewed
• [Journal Article] Proof Assistant Decision Procedures for Formalizing Origami (2011)
  • Author(s): Kaliszyk. C, Ida. T
  • Journal Title: Lecture Notes in Computer Science (proceedings of the Conference on Intelligent Computer Mathematics (CICM'11)) Volume: 6824 Pages: 45-57
  • DOI: 10.1007/978-3-642-22673-1_4
  • ISBN: 9783642226724, 9783642226731
  • Peer Reviewed
• [Journal Article] Morley's theorem revisited : Origami construction and automated proof (2011)
  • Author(s): Ida.T, Kasem.A, Ghourabi.F, Takahashi.H
  • Journal Title: Journal of Symbolic Computation vol.46 Pages: 162-170
  • NAID: 120007130912
  • Peer Reviewed
• [Journal Article] Disambiguation in Regular Expression Matching via Position Automata with Augmented Transitions (2011)
  • Author(s): Satoshi Okui, Taro Suzuki
  • Journal Title: Lecture Notes in Computer Science Volume: 6482 Pages: 231-240
  • Peer Reviewed
• [Journal Article] Translating Regular Expression Matching into Transducers (2011)
  • 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
  • Peer Reviewed
• [Journal Article] Origami Fold as Algebraic Graph Rewriting (2010)
  • Author(s): Tetsuo Ida and Hidekazu Takahashi
  • Journal Title: Journal of Symbolic Computation Volume: 45(4) Pages: 393-413
  • NAID: 120007138181
  • Peer Reviewed
• [Journal Article] Rubyプログラムの制御フロー解析とその健全性の証明 (2010)
  • Author(s): 松本宗太郎, 南出靖彦
  • Volume: 3巻
  • Pages: 9-25
  • NAID: 110007970972
  • Peer Reviewed
• [Journal Article] Origami Fold as Algebraic Graph Rewriting. (2010)
  • Author(s): Tetsuo Ida, Hidekazu Takahashi
  • Journal Title: Journal of Symboli Computation 45(4) Pages: 393-413
  • NAID: 120007138181
• [Journal Article] (2010)
  • Author(s): 松本宗太郎, 南出靖彦
  • Journal Title: Rubyプログラムの制御フロー解析とその健全性の証明 3巻 Pages: 9-25
  • Peer Reviewed
• [Journal Article] Rubyプログラムの制御フロー解析とその健全性の証明 (2010)
  • Author(s): 松本宗太郎, 南出靖彦
  • Journal Title: 情報処理学会論文誌 プログラミング 3 Pages: 9-25
  • NAID: 110007970972
  • Peer Reviewed
• [Journal Article] Linear Systems for Regular Hedge Languages (2010)
  • Author(s): Mircea Marin, Temur Kutsia
  • Journal Title: Advances in Databases and Information Systems. Associated Workshops and Doctoral Consortium of ADBIS 2009. Proceedings. LNCS 5968 Pages: 104-112
  • Peer Reviewed
• [Journal Article] Copy-on-Write in the PHP Langauge (2009)
  • Author(s): Tozawa, M. Tatsubori, T. Onodera, Y. Minamide
  • Journal Title: Proc. of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Pages: 200-212
  • Peer Reviewed
• [Journal Article] Symbolic and Algebraic Methods in Computational Origami : Invited Talk (2009)
  • Author(s): Tetsuo Ida
  • Journal Title: In Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation (ISSAC 2009) Pages: 3-4
  • Peer Reviewed
• [Journal Article] Origami Fold as Algebraic Graph Rewriting (2009)
  • Author(s): Tetsuo Ida, Hidekaza Takahashi
  • Journal Title: Proc. of 24th annual ACM Symposium on Applied Computing Pages: 1132-1138
  • NAID: 120007138181
  • Peer Reviewed
• [Journal Article] Graph Rewriting in Computational Origami (2009)
  • Author(s): Ida, T
  • Journal Title: Proceedings of the 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing(SYNASC 2008) Pages: 20-27
  • Peer Reviewed
• [Journal Article] Theorem Proving Based on the Characteristic Set Method for Computational Origami Constructions (2009)
  • Author(s): Ghourabi, F, Ida, T, Wang, D
  • Journal Title: Proceedings of the Tunisia-Japan Workshop on Symbolic Computation in Software Science(SCSS 2009) Pages: 90-92
  • Peer Reviewed
• [Journal Article] Hedge Pattern Partial Derivative (2009)
  • Author(s): T.Suzuki, S.Okui
  • Journal Title: 14-th International Conference on Implementation and Application of Automata(CIAA 2009), Lecture Notes in Computer Science 5642 Pages: 125-134
  • Peer Reviewed
• [Journal Article] Origami Fold as Algebraic Graph Rewriting (2009)
  • Author(s): Tetsuo Ida, Hidekazu Takahas hi
  • Journal Title: 24th annual ACM, Symposium on Applied Computing (SAC 2009) Pages: 1132-1138
  • NAID: 120007138181
  • Peer Reviewed
• [Journal Article] Copy-on-write in the PHP Language (2009)
  • Author(s): A. Tozawa, M. Tatsubori, T. Onodera, Y. Minamide
  • Journal Title: Proc. POPL: The Symposium on Principles of Programming Languages Pages: 200-212
  • Peer Reviewed
• [Journal Article] A Translation from the HTML DTD into a Regular Hedge Grammar (2008)
  • Author(s): T. Nishiyama, Y. Minamide
  • Journal Title: Proc. of 13th International Conference on Implementation and Application of Automata Pages: 122-131
  • Peer Reviewed
• [Journal Article] Product Drivatives of Regular Expressions (2008)
  • Author(s): Taro Suzuki, Staoshi Okui
  • Journal Title: IPSJ Online Transactions Volume: 1巻 Pages: 53-65
  • Peer Reviewed
• [Journal Article] Product Drivatives of Regular Expressions (2008)
  • Author(s): Taro Suzuki, Staoshi Okui
  • Journal Title: IPSJ Online Transactions 1巻 Pages: 53-65
  • Peer Reviewed
• [Journal Article] WEBEOS: A System for Origami Construction and Proving on the Web (2008)
  • Author(s): Tetsuo Ida, Asem Kasem
  • Journal Title: The INTERNATIONAL INSTITUTE for ADVANCED STUDIES in SYSTEMS RESEARCH and CYBERNETICS 2 Pages: 53-59
  • Peer Reviewed
• [Journal Article] Computational Origami Construction as Colistraint Solving and Rewriting (2008)
  • Author(s): Tetsuo Ida, Mircea Marin, Hidekazu Takahashi, Fadoua Ghourabi
  • Journal Title: Electronic Notes in Theoretical Computer Science 216 Pages: 31-44
  • Peer Reviewed
• [Journal Article] A Translation from the HTML DTD into a Regular Hedge Grammar (2008)
  • Author(s): T. Nishiyama, Y. Minamide
  • Journal Title: Proc. of the 13th International Conference on-Implementation and Application of Automata LNCS 5184 Pages: 122-131
  • Peer Reviewed
• [Journal Article] Product Derivatives of Regular Expressions (2008)
  • Author(s): Taro Suzuki, Satoshi Okui
  • Journal Title: IPSJ Online Transactions 1 Pages: 53-65
  • NAID: 130000022133
  • Peer Reviewed
• [Presentation] 文字列解析によるクロスサイトスクリプティング脆弱性検査の改良 (2012)
  • Author(s): 木村将人, 南出靖彦
  • Organizer: プログラミングおよびプログラミング言語ワークショップ(ポスター)
  • Place of Presentation: 和歌山県南紀白浜
  • Year and Date: 2012-03-08
• [Presentation] Origami Axioms and Circle Extension (2011)
  • Author(s): Kasem.A, Ghourabi.F, Ida.T
  • Organizer: Proceedings of the 26th Symposium on Applied Computing (SAC 2011), pp.1106-1111
  • Place of Presentation: Tunghai University Taiwan
  • Year and Date: 2011-03-23
• [Presentation] Extended Web Services for Computational Origami. The 3rd International Workshop on Symbolic Computation in Software Science (SCSS2010) (2010)
  • Author(s): Kasem and T. Ida
  • Organizer: RISC-Linz Report Series
  • Place of Presentation: Hagenberg, Austria
  • Year and Date: 2010-07-30
• [Presentation] バックトラックのないマッチングオートマトンを用いたXML変換のためのアルゴリズム (2010)
  • Author(s): 柴田裕哉, 鈴木大郎
  • Organizer: 第78回情報処理学会プログラミング研究会
  • Place of Presentation: 電気通信大学
  • Year and Date: 2010-03-16
• [Presentation] Rubyのコア言語の操作的意味論 (2009)
  • Author(s): 松本宗太郎, 南出靖彦
  • Organizer: 日本ソフトウェア科学会第26回大会
  • Place of Presentation: 島根大学
  • Year and Date: 2009-09-16
• [Presentation] Copy-on-Write in the PHP Langauge (2009)
  • Author(s): Tozawa, M.Tatsubori, T.Onodera, Y.Minamide
  • Organizer: Proc.of the 13^<th> International Conference on Programming Languages, pp.200-212
  • Place of Presentation: Lyon, France
  • Year and Date: 2009-08-23
• [Presentation] Reasoning Tool for Mathematical Origami Construction (2009)
  • Author(s): F. Ghourabi, T. Ida, H. Takahashi, and A. Kasem
  • Organizer: The International Symposium on Symbolic and Algebraic Computation (ISSAC 2009)
  • Place of Presentation: Seoul, Korea
  • Year and Date: 2009-07-30
• [Presentation] Reasoning Tool for Mathematical Origami Construction (2009)
  • Author(s): Ghourabi, F, Ida, T, Takahashi, H, Kasem, A
  • Organizer: ISSAC09 Software Presentation. ACM
  • Place of Presentation: KIAS(Korea Institute for Advanced study)
  • Year and Date: 2009-07-30
• [Presentation] Origami Fold as Algebraic Graph Rewriting (2009)
  • Author(s): Tetsuo Ida, Hidekaza Takahashi
  • Organizer: Proc.of 24^<th> annual ACM Symposium on Applied Computing, pp.1132-1138
  • Place of Presentation: Hawaii, USA
  • Year and Date: 2009-03-12
• [Presentation] Symbolic and Algebraic Methods in Computational Origami : Invited Talk. (2009)
  • Author(s): Tetsuo Ida.
  • Organizer: In Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation (ISSAC 2009), pages 3-4. ACM
  • Place of Presentation: Hawaii, USA.
• [Presentation] Experiences with Web Environment Origamium (2008)
  • Author(s): Kasem and T. Ida
  • Organizer: 日本ソフトウェア科学会第25回大会
  • Place of Presentation: 筑波大学(東京キャンパス)
  • Year and Date: 2008-09-11
• [Presentation] ブラウザにおけるJavaScript実行のモデル化 (2008)
  • Author(s): 安田峰悠,松本宗太郎,南出靖彦
  • Organizer: 日本ソフトウェア科学会第25回大会
  • Place of Presentation: 筑波大学(東京キャンパス)
  • Year and Date: 2008-09-10
• [Presentation] 動的に生成されるHTML文書の妥当性検査 (2008)
  • Author(s): 西山拓哉,南出靖彦
  • Organizer: 日本ソフトウェア科学会第25回大会
  • Place of Presentation: 筑波大学(東京キャンパス)
  • Year and Date: 2008-09-10
• [Presentation] A Translation from the HTML DTD into a Regular Hedge Grammar (2008)
  • Author(s): T.Nishiyama, Y.Minamide
  • Organizer: Proc.of 13^<th> International Conference on Implementation and Application of Automata, pp.122-131
  • Place of Presentation: California, USA
  • Year and Date: 2008-07-21
• [Presentation] Experiences with Web Environment Origamium: Examples and Applications (2008)
  • Author(s): Asem Kasem, Tetsuo Ida
  • Organizer: Austrian-japanese Workshop on Symbolic Complutation in Software Science (SCSS 2008)
  • Place of Presentation: RISC, Hagenberg, Austria
  • Year and Date: 2008-07-13