2003 Fiscal Year Final Research Report Summary
Security Verification of Software with Dynamic Access Control
| Project/Area Number |
14580376
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| 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) |
NITTA Naoya NARA INSTITUTE OF SCIENCE AND TECHNOLOGY, GRADUATE SCHOOL OF INFORMATION SCIENCE, ASSISTANT PROFESSOR, 情報科学研究科, 助手 (20346307)
TAKATA Yoshiaki NARA INSTITUTE OF SCIENCE AND TECHNOLOGY, GRADUATE SCHOOL OF INFORMATION SCIENCE, ASSISTANT PROFESSOR, 情報科学研究科, 助手 (60294279)
|
|---|
| Project Period (FY) |
2002 – 2003
|
| Keywords | ACESS CONTROL / SECURITY / SAFETY / VERIFICATION / MODEL CHECKING / POLICY |
|---|
| Research Abstract |
A policy for access control is a rule describing when and on which condition a specified subject can (or cannot or must) perform a specified action on a specified target. A program of which behavior is controlled by a policy is called a policy controlled system (PCS). In this research, we first define a simple policy specification language. The language has a structure sufficient for describing positive/negative authorization and obligation. We formally define the operational semantics of PCS based on the language.
Next, we define the (safety) verification problem for PCS as the problem to decide for a given PCS S and a goal (called safety property) φ, whether every reachable state of P satisfies φ. We have implemented a verification tool for PCS, which works as follows. First, a pushdown system (PDS) is abstracted from a PCS and a nondeterministic finite automaton (NFA) which accepts the set of all reachable states of the PDS is constructed. The computation time is about a few minutes for verifying a PCS of 1.7K lines with complex obligation policy, which shows that the proposed verification method is feasible for real world programs.
We extend the proposed method for verifying the property of term rewrite system (TRS). A subclass of TRS called generalized growing TRS (GG-TRS) is defined by extending PDS to tree structure. We show that for an arbitrary GG-TRS which preserves recognizability, an LTL (linear temporal logic) model checking is decidable. Also, as an application of the verification method, we have implemented a tool which verifies whether a given XML document satisfies a given accessibility guideline. We have verified about 3,000 web pages of forty major organizations in the U.S.A.and Japan using the tool.
|
