2011 Fiscal Year Final Research Report
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
|
| 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.
|
