naistar (NAIST Academic Repository) >
学術リポジトリ naistar / NAIST Academic Repository naistar >
テクニカルレポート / Technical Report >
Please use this identifier to cite or link to this item:
|Title: ||Dicidability and complexity of the security verification problem for programs with stack inspection|
|Authors: ||Nitta, Naoya|
|Issue Date: ||Mar-2001|
|Publisher: ||Nara Institute of Science and Technology|
|Series/Report no.: ||Information Science Technical Report ~ TR2001003|
|Abstract: ||Java development kit 1.2 provides a runtime access control mechanism which inspects a control stack to examine whether the program has appropriate access permissions. For such a programming language, it is desirable to guarantee that each execution of a program satisfies required security properties. Jensen et al. introduced a verication problem of deciding for a given program P and a given security property written in a temporal logic formula, whether every reachable state of P satisfies . They showed that the problem is decidable for the class of programs which do not contain mutual recursion. In this paper, we show that the set of state sequences of a program is always an indexed language and consequently the verification problem is decidable. Our result is stronger than Jensen's in that a security property can be specified by a regular language, whose expressive power is stronger than temporal logic, and in that a program can contain mutual recursion. Furthermore, we discuss the computational complexity of the problem. For example, the problem is shown to be deterministic DEXP-POLY time complete if each check statement in P is specified by aNFA and a security property is specified by aDFA.|
|Text Version: ||author|
|Appears in Collections:||テクニカルレポート / Technical Report|
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.