2015 Fiscal Year Annual Research Report
| Project/Area Number |
25730039
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
LI Xin 東京大学, 情報理工学(系)研究科, 研究員 (60510641)
|
|---|
| Project Period (FY) |
2013-02-01 – 2016-03-31
|
| Keywords | Model Checking / Pushdown System / Web Security |
|---|
| Outline of Annual Research Achievements |
The general objective of this research is to develop formal verification techniques and tools, based on especially model checking techniques, to ensure the safety and security of web applications.
In 2015, our main efforts are devoted to the following tasks:
1) Elaborate a sliding-window incremental algorithm for weighted pushdown systems (WPDSs), so as to enhance the practical efficiency of program analysis algorithms encoded based on WPDSs. We have implemented and evaluated the new algorithm with Java points-to analysis. Our empirical study shows that the sliding-window algorithm always outperforms the whole program analysis. The work is under submission, and we plan to make our tool open source to the community after publishing the work.
2) Elaborate a new backward/forward saturation algorithm for reachability problem of subclasses of conditional pushdown systems (CPDSs) that obey certain patterns. It gives rise to alternative solutions to reachability analysis of the existing applications using CPDSs, such as reachability analysis of HTML5 parser specifications, stack inspection, etc. We found that the backward saturation algorithm could be further optimized for the sake of practical scalability. We are looking into the optimization and planning an empirical study based on it.
|
Research Products
(2 results)
