2007 Fiscal Year Final Research Report Summary
STUDY ONAUTOMATIC VERIFICATION OF HIGHLY RELIABLE SOFTWARE BYINFINITE STATE MODEL CHECKING
| Project/Area Number |
18500023
|
|---|
| 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 INFORMATION SCIENCE, PROFESSOR (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAKATA Yoshiaki KOCHI UNIVERSITY OF TECHNOLOGY, FACULTY OF ENGINEEIG, ASSISTANT PROFESSOR (60294279)
|
|---|
| Project Period (FY) |
2006 – 2007
|
| Keywords | FORMAL VERIFICATION / MODEL CHECKING / STATIC ANALYSIS / FORMAL LANGUAGE / ACCESS CONTROL / SECURITY / EXECUTION HISTORY / XML |
|---|
| Research Abstract |
(1) Model Checking Methods for Recursive Programs: We defined a formal model for programs with access control based on execution history, called HBAC programs and showed that the verification problem for HBAC programs is solvable in polynomial time under a practical assumption. We also proposed a few optimization techniques based on the elimination of useless rules of context-free grammar (CFG). We conducted verifications of two examples, namely, Chinese wall policy and an online banking system, using our implemented verification tool. The verification time for the former problem was 64 seconds when the number of permissions was eighty, and the verification time for the latter problem was 0.01 second when the number of permissions was sixty.
(2) Information Flow Analysis: A new information flow analysis method for HBAC programs was proposed. Using the method, we can verify a property of information flow extended to execution paths. Also, we extended a self-composition method so that recursive programs can be analysed.
(3) Expressive Power of History-based Access Control: We clarified the relation among the expressive powers of various access control models based on execution history.
(4) A Formal Model of Aspect-Oriented Program: A formal model called A-LTS for a pointcut and advice was defined and it was shown that the languages accepted by A-LTSs, deterministic context-free languages (CFLs) and linear CFLs are pairwise incomparable.
(5) Other research results.
(a) A new class of tree automata called TAN was defined by incorporating a rewrite system modulo equational theory into a standard tree automaton, and discussed the decidability of the fundamental problems of TAN.
(b) Computational complexity of the disclosure tree strategy (DTS) in trust negotiation was clarified and an efficient algorithm was also proposed under practical conditions.
(c) We proposed a secondary structure prediction method for interacting RNA based on a parsing algorithm for multiple CFG.
|
Research Products
(26 results)
