| 研究課題/領域番号 |
25730039
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
LI Xin 東京大学, 情報理工学(系)研究科, 研究員 (60510641)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2015-03-31
|
| キーワード | Web Security / Access Rights Analysis / Pushdown Model Checking |
|---|
| 研究概要 |
Access control is the first step to securing safety-critical systems, but nowadays security policies for web applications are still manually generated by developers. This research aims to develop static analysis algorithms and techniques to automatically identify authorisation requirements, and to meanwhile detect vulnerabilities in web applications. In the past year, efforts are devoted to the following,
(1) designed an algorithm that automatically generates access control policies for Java programs that use stack-inspection based sandboxing for controlling access of components to system resources, and our latest algorithm in progress is recorded at http://arxiv.org/abs/1307.2964.
(2) proposed and implemented several new model checking algorithms for conditional weighted pushdown systems, and studied their practical efficiency by an initial application to models generated from HTML5 parsing specification. Applications to object-oriented programs will be investigated and tested next. One of the algorithms and the model checker will be published by IPSJ.
(3) proposed a static analysis algorithm that features both path-sensitivity and context-sensitivity. Its applications to the analysis of access control models and other security properties is under examination.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
(1) In the past year, the investigator took maternity leave for several months, and changed affiliation.
(2) The reachability analysis problem of stack-based access control is EXPTIME-complete. Therefore, it is challenging to automatically generating access rights efficiently for practical instances.
|
| 今後の研究の推進方策 |
To boost this research in the next year, the approach of abstraction refinement will be explored and combined into the analysis of access rights. Such a demand-driven technique is effective in program verification and will be promising for efficiency.
The disadvantage of language-based access control is known, yet it is still the backbone of Java security model. It would be investigated to combine access right analysis with techniques that detect malicious codes attempting to circumvent the stack-based sandboxing.
Scalable model checking algorithms have been developed for HORS (higher-order recursion schemes) that subsume pushdown systems, despite the hyper-exponentional worst-case complexity of the problem. HORS is extended to verify objected-oriented programs. Its potential application to Java-centric web security analysis will be studied.
|
| 次年度の研究費の使用計画 |
In the past year, the investigator took maternity leave for several months, and the research project was delayed for three months.
Besides, due to caring for the little baby and the change of affiliation, the investigator couldn’t travel abroad to visit collaborators as scheduled.
Several papers are under preparation and pending for publication. The budget will be mainly used to travel and present at conferences.
|
