Papers - NITTA Naoya
-
Security Verification of Programs with Stack Inspection
Naoya Nitta
奈良先端科学技術大学院大学博士論文 2002.2
Single Work
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
Nitta Naoya, Takata Yoshiaki, Seki Hiroyuki
Computer Software 19 ( 3 ) 176 - 194 2002
-
An Efficient Security Verification Method for Programs with Stack Inspection Reviewed
Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki
Proceedings of the 8th ACM Conference on Computer and Communication Security 68 - 77 2001.11
Joint Work
Authorship：Lead author
-
Security Verification of Programs with Stack Inspection Reviewed
Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki
Proceedings of 6th ACM Symp. on Access Control Models and Technologies 31 - 40 2001.5
Joint Work
Authorship：Lead author
-
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
Joint Work
Authorship：Lead author
-
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
Joint Work
Publisher：ACM
Other Link： 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
Joint Work
Publisher：ACM
Other Link： http://dblp.uni-trier.de/db/conf/ccs/ccs2001.html#conf/ccs/NittaTS01