論文 - 新田 直也
-
Security Verification of Programs with Stack Inspection
Naoya Nitta
奈良先端科学技術大学院大学博士論文 2002年2月
単著
Recently, with rapidly growth of open network environment, a well-defined access control mechanism becomes necessary. 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. Jensen et al. introduced a verification problem of deciding for a given program P with stack inspection and a given security property psi written in a temporal logic formula, whether every reachable state of $P$ satisfies psi. They showed that the problem is decidable for the class of programs which do not contain mutual recursion. In this thesis, 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. We also investigated the computational complexity of the problem. Since the result implies the problem is computationally intractable in general, we introduce a practically important subclass of programs which exactly model programs containing stack inspection of Java development kit 1.2. We present an algorithm which can solve the problem for this subclass in linear time
in the size of a program. Furthermore, we implemented a verification system based on the proposed algorithm.
Experimental results suggest that the proposed lgorithm can be efficiently executed for real-world programs. -
An Efficient Security Verification Method for Programs with Stack Inspection
新田 直也, 高田 喜朗, 関 浩之
コンピュータ ソフトウェア 19 ( 3 ) 176 - 194 2002年
-
An Efficient Security Verification Method for Programs with Stack Inspection 査読あり
Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki
Proceedings of the 8th ACM Conference on Computer and Communication Security 68 - 77 2001年11月
共著
担当区分：筆頭著者
-
Security Verification of Programs with Stack Inspection 査読あり
Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki
Proceedings of 6th ACM Symp. on Access Control Models and Technologies 31 - 40 2001年5月
共著
担当区分：筆頭著者
-
Decidability and Complexity of the Security Verification Problem for Programs with Stack Inspection
Naoya Nitta, Satoshi Ikada, Yoshiaki Takata, Hiroyuki Seki
Technical Report NAIST-IS-TR2001003, Nara Institute of Science and Technology 2001年3月
共著
担当区分：筆頭著者
-
Security verification of programs with stack inspection.
Naoya Nitta, Hiroyuki Seki, Yoshiaki Takata
6th ACM Symposium on Access Control Models and Technologies, SACMAT 2001, Litton-TASC, Chantilly, Virginia, USA, May 3-4, 2001 31 - 40 2001年
共著
出版者・発行元：ACM
その他リンク： http://dblp.uni-trier.de/db/conf/sacmat/sacmat2001.html#conf/sacmat/NittaST01
-
An efficient security verification method for programs with stack inspection.
Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki
CCS 2001, Proceedings of the 8th ACM Conference on Computer and Communications Security, Philadelphia, Pennsylvania, USA, November 6-8, 2001. 68 - 77 2001年