Automated security analysis of web applications
| Project/Area Number |
25730039
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
LI Xin 東京大学, 情報理工学(系)研究科, 研究員 (60510641)
|
|---|
| Project Period (FY) |
2013-02-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000)
Fiscal Year 2014: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2013: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | Web Security / Access Control / Model Checking / Program Analysis / Pushdown System / Access Control Policy / Web Applications / Pushdown Model Checking / Access Rights Analysis |
|---|
| Outline of Final Research Achievements |
This research is to apply program analysis and formal verification techniques to automated web security analysis, with a focus on automated generation of access control policies for Java-centric web applications. During the project, we first designed a systematic approach to automated generation of access control policies for Java programs to pass the runtime authorization. Next, to put the technique into practice, we studied efficient algorithms of those analysis modules underpinning the algorithmic framework. Last but not least, we also developed algorithms for model checking recursively-typed higher-order grammars and their potential application to web security analysis will be studied as future work. In the future, we plan to further elaborate the proposed algorithms and techniques, and conduct empirical studies of them, whereby eventually build a practical system for web security analysis.
|
Report
(4 results)
Research Products
(7 results)
