2014 Fiscal Year Research-status 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 | Access Control Policy / Web Applications / Pushdown Model Checking |
|---|
| Outline of Annual Research Achievements |
The primary aim of this research is to develop static analysis algorithms and techniques to automatically generate access control policies for Java-centric web applications, and hereby to help securely deploy applications and find vulnerabilities in web applications.
In 2014, research efforts were devoted to the following tasks:
(1) Design of tractable algorithms for subclasses of conditional pushdown systems (CPDS). The reachability problem of CPDS is EXPTIME-complete. We identify the subclasses of CPDS which have polynomial algorithms for reachability analysis, and show that certain context-sensitive points-to analysis for Java, and the reachability of programs with stack inspection can be modelled to the subclasses.
(2) Design of new algorithms for conditional weighted pushdown systems (CWPDS) by satisfiability checking. Inspired by the theoretical and practical advances in satisfiability checking (known as SAT and SMT techniques), we proposed a new algorithm for CWPDS using satisfiability checking, more specifically, satisfiability of formulas containing uninterpreted functions with equality.
(3) We had proposed a static analysis algorithm that features both path-sensitivity and context-sensitivity. We are looking into the possibility of extending the model to further support quantitative aspects.
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
(1) It is challenging to scale program analysis techniques to production-level web applications.
(2) The investigator had a baby in 2013 and took maternity leave for a couple months, so the project was delayed in the first place. She also changed affiliation afterwards, and currently no students could help her to fulfil some implementation tasks.
|
| Strategy for Future Research Activity |
It is challenging to scale program analysis techniques to production-level web applications. To boost this research in the next year,
(1) We have to tune our algorithms to be compositional and demand-driven for practical efficiency and scalability. These techniques are known to be effective in scaling program analysis algorithms and formal verification techniques.
(2) We may also need to apply heuristics in the analysis, and find a good tradeoff between precision and efficiency. We plan to first make a prototype for the preliminary algorithm proposed for automatically generating access control policies, and apply it to realistic web applications.
Besides, the investigator would solicit collaborators to help fulfil some implementation tasks.
|
| Causes of Carryover |
(1) Several papers are under preparation and pending for publication.
(2) According to the progress of the project, the investigator may visit potential collaborators, e.g., researchers of IBM Thomas J. Watson Research Center where they have been working on Java security and the security of web applications.
|
| Expenditure Plan for Carryover Budget |
The budget will be used to
(1) travel and present papers at conferences, and
(2) visit domestic and overseas collaborators if necessary.
|
