An efficient security verification method for programs with stack inspection

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An efficient security verification method for programs with stack inspection

Full text

Pdf (373 KB)

Source

Conference on Computer and Communications Security archive
Proceedings of the 8th ACM conference on Computer and Communications Security table of contents

Philadelphia, PA, USA

Session: Mobile Code and Distributed Systems table of contents

Pages: 68 - 77

Year of Publication: 2001

ISBN:1-58113-385-5

Authors

Naoya Nitta	Nara Institute of Science and Technology, Takayama, Ikoma, Nara, Japan
Yoshiaki Takata	Nara Institute of Science and Technology, Takayama, Ikoma, Nara, Japan
Hiroyuki Seki	Nara Institute of Science and Technology, Takayama, Ikoma, Nara, Japan

Sponsor

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 31, Citation Count: 2

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/501983.501994 What is a DOI?

ABSTRACT

Stack inspection is a key technology for runtime access control of programs in a network environment. In this paper, a verification problem to decide whether a given program with stack inspection satisfies a given security property is discussed. First, the computational complexity of the problem is investigated. Since the result implies the problem is computationally intractable in general, we introduce a practically important subclass of programs which exactly model programs containing check Permission of Java development kit 1.2. We show that the problem for this subclass is solvable in linear time in the size of a program.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martín Abadi , Michael Burrows , Butler Lampson , Gordon Plotkin, A calculus for access control in distributed systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.706-734, Sept. 1993 [doi>10.1145/155183.155225]
	2	M. Abadi, C. Fournet, and G. Gonthier. Secure communications processing for distributed languages. In IEEE Symp. on Security and Privacy, pages 74-88, 1999.
	3	Alfred V. Aho, Indexed Grammars—An Extension of Context-Free Grammars, Journal of the ACM (JACM), v.15 n.4, p.647-671, Oct. 1968 [doi>10.1145/321479.321488]
	4	Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
	5	Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
	6	Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
	7	E. A. Emerson. Temporal and Modal Logic, in Handbook of Theoretical Computer Science, 1023-1024. Elsevier, 1990.
	8	M. R. Garey and D. S. Johnson. Computers and Intractability. W. H. Freeman and Company, 1979.
	9	Li Gong, New security architectural directions for Java, Proceedings of the 42nd IEEE International Computer Conference, p.97, February 23-26, 1997
	10	Nevin Heintze , Jon G. Riecke, The SLam calculus: programming with secrecy and integrity, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.365-377, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268976]
	11	John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	12	T. Jensen, D. Le Mffetayer, and T. Thorn. Verification of control ow based security properties. In IEEE Symp. on Security and Privacy, pages 89-103, 1999.
	13	Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
	14	Naoya Nitta , Hiroyuki Seki , Yashiaki Takata, Security verification of programs with stack inspection, Proceedings of the sixth ACM symposium on Access control models and technologies, p.31-40, May 2001, Chantilly, Virginia, United States [doi>10.1145/373256.373260]
	15	Peter Ørbæk, Can you Trust your Data?, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.575-589, May 22-26, 1995
	16	Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997
	17	D. S. Wallach and E. W. Felten. Understanding Java stack inspection. In IEEE Symp. on Security and Privacy, pages 52-63, 1998.

CITED BY 2

	Byeong-Mo Chang, Static check analysis for Java stack inspection, ACM SIGPLAN Notices, v.41 n.3, March 2006
	Isao Yagi , Yoshiaki Takata , Hiroyuki Seki, A Labeled Transition Model A-LTS for History-Based Aspect Weaving and Its Expressive Power, IEICE - Transactions on Information and Systems, v.E90-D n.5, p.799-807, May 2007