|
naistar (NAIST Academic Repository) >
学術リポジトリ naistar / NAIST Academic Repository naistar >
テクニカルレポート / Technical Report >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/10061/3205
|
| Title: | Dicidability and complexity of the security verification problem for programs with stack inspection |
| Authors: | Nitta, Naoya
Ikada, Satoshi
Takata, Yoshiaki
Seki, Hiroyuki
ニッタ, ナオヤ
イカダ, サトシ
タカタ, ヨシアキ
セキ, ヒロユキ
新田, 直也
伊加田, 恵志
高田, 喜朗
関, 浩之 |
| 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. |
| URI: | http://hdl.handle.net/10061/3205 |
| URI: | http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=55465 |
| Fulltext: | http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=55465 |
| ISSN: | 0919-9527 |
| 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.
|
