Papers - NITTA Naoya
-
スタック検査機能を持つプログラムに対するセキュリティ検証問題の決定可能性 Reviewed
新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会論文誌(D-I) J85-D-I ( 4 ) 360 - 370 2002.4
Joint Work
Authorship：Lead author
-
Decidability of the Security Verification Problem for Programs with Stack Inspection
NITTA Naoya, TAKATA Yoshiaki, SEKI Hiroyuki
The Transactions of the Institute of Electronics,Information and Communication Engineers. 85 ( 4 ) 360 - 370 2002.4
Joint Work
Publisher：電子情報通信学会
Java development kit 1.2のように,プログラム実行時に制御スタックを検査することでアクセス制御を行うようなプログラム環境がある.Jensenらは,プログラム P 及び時相論理式を用いて記述された検証条件 ψ を与えたときに,P の到達可能な状態すべてが ψ を満たすかどうかを決定する問題として検証問題を定義し,相互再帰を含まないプログラムのクラスに対して検証問題が決定可能となることを示した. 本論文では,時相論理式よりも真に表現能力の大きい正規言語を用いて検証問題を定義する.そして,プログラムのトレース集合がインデックス言語となることを示し,その系としてプログラムが相互再帰を含む場合も含めて検証問題が一般に決定可能となることを示すことにより,Jensenらの結果を改善する.更に,自明なスタック検査のみを含むプログラムのクラスに対する検証問題が,プログラムサイズに対して多項式時間可解であることを示す.
-
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
-
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
-
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