| 研究課題/領域番号 |
25730039
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
LI Xin 東京大学, 情報理工学(系)研究科, 研究員 (60510641)
|
|---|
| 研究期間 (年度) |
2013-02-01 – 2016-03-31
|
| キーワード | Access Control Policy / Web Applications / Pushdown Model Checking |
|---|
| 研究実績の概要 |
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.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
(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.
|
| 今後の研究の推進方策 |
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.
|
| 次年度使用額が生じた理由 |
(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.
|
| 次年度使用額の使用計画 |
The budget will be used to
(1) travel and present papers at conferences, and
(2) visit domestic and overseas collaborators if necessary.
|
