Advanced Search
Japanese | English

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
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.
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.


Copyright (c) 2007-2012 Nara Institute of Science and Technology All Rights Reserved.
DSpace Software Copyright © 2002-2010  Duraspace - Feedback