WEKO3
アイテム
Dicidability and complexity of the security verification problem for programs with stack inspection
http://hdl.handle.net/10061/3205
http://hdl.handle.net/10061/3205f73d30a2-c7b9-47a1-a987-6e408a085fc2
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
fulltext (428.8 kB)
|
|
| アイテムタイプ | テクニカルレポート / Technical Report(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2006-07-31 | |||||
| タイトル | ||||||
| タイトル | Dicidability and complexity of the security verification problem for programs with stack inspection | |||||
| 言語 | ||||||
| 言語 | eng | |||||
| 資源タイプ | ||||||
| 資源タイプ | technical report | |||||
| アクセス権 | ||||||
| アクセス権 | open access | |||||
| 著者 |
Nitta, Naoya
× Nitta, Naoya× Ikada, Satoshi× Takata, Yoshiaki× Seki, Hiroyuki |
|||||
| 抄録 | ||||||
| 内容記述タイプ | 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. | |||||
| 書誌情報 |
en : Information Science Technical Report 号 TR2001003, 発行日 2001-03 |
|||||
| 出版者 | ||||||
| 出版者 | Nara Institute of Science and Technology | |||||
| ISSN | ||||||
| 収録物識別子タイプ | ISSN | |||||
| 収録物識別子 | 0919-9527 | |||||
| 部分である | ||||||
| 関連タイプ | isPartOf | |||||
| 識別子タイプ | URI | |||||
| 関連識別子 | http://isw3.naist.jp/IS/TechReport/ | |||||
| 著者版フラグ | ||||||
| 出版タイプ | VoR | |||||
| 電子化ID | ||||||
| 値 | R001983 | |||||
