| Project/Area Number |
16500019
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | NARA INSTITUTE OF SCIENCE AND TECHNOLOGY |
|---|
Principal Investigator |
SEKI Hiroyuki NARA INSTITUTE OF SCIENCE AND TECHNOLOGY, GRADUATE SCHOOL OF INFORAMTION SCIENCE, PROFESSOR, 情報科学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAKATA Yoshiaki NARA INSTITUTE OF SCIENCE AND TECHNOLOGY, GRADUATE SCHOOL OF INFORAMTION SCIENCE, ASSISTANT PROFESSOR, 情報科学研究科, 助手 (60294279)
|
|---|
| Project Period (FY) |
2004 – 2005
|
| Project Status |
Completed (Fiscal Year 2005)
|
| Budget Amount *help |
¥3,400,000 (Direct Cost: ¥3,400,000)
Fiscal Year 2005: ¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 2004: ¥1,700,000 (Direct Cost: ¥1,700,000)
|
|---|
| Keywords | FORMAL VERIFICATION / MODEL CHECKING / ACITVE SOFTWARE / ACCESS CONTROL / STATIC ANALYSIS / EXECUTION HISTORY / FORMAL LANGUAGE / SECURITY POLICY |
|---|
| Research Abstract |
(1)A formal model of programs with access control based on execution history and its model checking : We defined a formal model called HBAC programs. The verification problem for HBAC programs was defined and shown to be EXPTIME-complete, while the problem is solvable in polynomial time under a reasonable assumption. The proposed method reduces the verification problem to the decision problem for a context-free grammar (cfg) that generates all the execution sequences of a given HBAC program. We also proposed a few optimization techniques that reduce the number of cfg rules useless for generating execution sequences. Experimental results showed that the verification tool we have implemented can verify practical HBAC programs within a reasonable time.
(2)A static analysis using tree automata for XML access control : We proposed a static analysis method based on tree automata for determining whether a query to an XML database does not access any elements nor attributes that are prohibited by a given policy. We showed that our query model is sufficiently general by showing that the expressive power of our model is strictly greater than Neven's query automata. We also investigated a consistency problem of policies in schema transformation of XML databases and showed that the problem is decidable.
(3)A formal model for stateful trust management systems : We proposed a trust management model that can represent a system with internal states. The verification problem was defined as the problem to decide whether the behavior of a system with a given policy satisfies a given verification property, and a verification method for the problem was also proposed. We implemented two verification tools, one is based on SPIN and Prolog and the other is implemented by Prolog only. Experimental results showed that the latter tool is more efficient than the former one.
|
