Security properties of typed applets

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Security properties of typed applets

Full text

Pdf (1.99 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

San Diego, California, United States

Pages: 391 - 403

Year of Publication: 1998

ISBN:0-89791-979-3

Authors

Xavier Leroy	INRIA Rocquencourt, Projet Cristal, B.P. 105, 78153 Le Chesnay, France
François Rouaix	INRIA Rocquencourt, Projet Cristal, B.P. 105, 78153 Le Chesnay, France

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 19, Citation Count: 20

Additional Information:

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/268946.268979 What is a DOI?

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 , Andrew D. Gordon, Reasoning about Cryptographic Protocols in the Spi Calculus, Proceedings of the 8th International Conference on Concurrency Theory, p.59-73, July 01-04, 1997
	2	J.-P. Ban~tre and C. Bryce. A security proof system for net~vorks of communicating processes. Research report 2042, INRIA, Sept. 1993.
	3	J.-P. Billon. Security breaches in the JDK 1.1 beta2 security API. Dyacle~ hztp://~w, dyade.fr/fr/ actio~as/VIP/SecHole.html, Jan. 1997.
	4	Nathaniel Borenstein, Enabled Mail, Proceedings of the IFIP TC6/WG6.5 International Conference on Upper Layer Protocols, Architectures and Applications, p.411-412, June 01-03, 1994
	5	Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
	6	K. Brunnstein. Hostile ActiveX control demonstrated, RISKS Forum, 18(82), Feb. 1997.
	7	Luca Cardelli , Simone Martini , John C. Mitchell , Andre Scedrov, An extension of system F with subtyping, Information and Computation, v.109 n.1-2, p.4-56, Feb. 15/March 1994 [doi>10.1006/inco.1994.1013]
	8	D. Dean , Felten , Wallach, Java Security: From HotJava to Netscape and Beyond, Proceedings of the 1996 IEEE Symposium on Security and Privacy, p.190, May 06-08, 1996
	9	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]
	10	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]
	11	S. Drossopoulou and S. Eisenbach. 3ava is type safe - probably. In Pr0c. I I~h European Conference on Object Ories~ed Programming~ 3une 1997.
	12	M. Erdos, B. Hartman, and M. Mueller. Security reference model for the Java Developer% Kit 1.0.2. Java- Soft, http://java.sun, com/security/SRH.h~ml, Nov, 1998.
	13	J. Gosling and H. McGilton. The Java }anguag0 environment- a white paper. JavaSoft~ http:// java.sun, com/'docslwhi'~el}.angeav~ May 1996,
	14	N. Heinze and 3. G. BJecke. The SLam ca}cu}us: pro- ~amming with secrecy and integrity. Draftj ~va~}ablo elecSronically, Mar. 1998.
	15	D. Hopwood. Jaw security bug (applets can load nativQ methods). RISKS Forum, 17(83), Mar. 199G.
	16	T. 3ensen, D. Le M~tayer, and T. Thorn. A formaUsation of visibility and dynamic loading in Java. Technical Report t137, IR/SA, Oct. 1997.
	17	X. Leroy. Polymorphic typing of an algorithmic language. Research report 1778, INRIA, 1992.
	18	R. Milner, M. Tofte, R. Harper, and D. MacQueen. The d~finflion of Standard NIL (revised). The MIT Press, 1997.
	19	Greg Morrisett , Matthias Felleisen , Robert Harper, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.66-77, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224182]
	20	George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
	21	George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
	22	Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
	23	Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-378, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199533]
	24	Jens Palsberg , Peter Ørbæk, Trust in the lambda-Calculus, Proceedings of the Second International Symposium on Static Analysis, p.314-329, September 25-27, 1995
	25	G, D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aaxhus University, 1981.
	26	Z. Qian. A formal specification of a large subset of Java Virtual Machine instructions. Draft, available electronically, Sept. 1997.
	27	John C. Reynolds, User-defined types and procedural data structures as complementary approaches to data abstraction, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
	28	François Rouaix, A Web navigator with applets in Caml, Computer Networks and ISDN Systems, v.28 n.7-11, p.1365-1371, May 1996
	29	Jean-Pierre Talpin , Pierre Jouvelot, The type and effect discipline, Information and Computation, v.111 n.2, p.245-296, June 1994 [doi>10.1006/inco.1994.1046]
	30	Mads Tofte, Type inference for polymorphic references, Information and Computation, v.89 n.1, p.1-34, Nov. 1990 [doi>10.1016/0890-5401(90)90018-D]
	31	Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996
	32	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
	33	D. S. Wallach, D. Balfanz, D. Dean, and E. W. Felten. Extensible security architectures for Java. Technical rel~ort 546-97, Department of Computer Science, Princeton University, Apr. 1997.
	34	F. Yellin. Low level security in Java. In Proceedings of the Fourth International World Wide Web Conference. O'Reil}y, 1995.

CITED BY 20

	David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA
	Zhong Shao , Christopher League , Stefan Monnier, Implementing typed intermediate languages, ACM SIGPLAN Notices, v.34 n.1, p.313-323, Jan. 1999
	Peter Sewell , Jan Vitek, Secure composition of untrusted code: box π, wrappers, and causality types, Journal of Computer Security, v.11 n.2, p.135-187, May 2003
	Jan Vitek , Boris Bokowski, Confined types, ACM SIGPLAN Notices, v.34 n.10, p.82-96, Oct. 1999
	Christopher League , Zhong Shao , Valery Trifonov, Representing Java classes in a typed intermediate language, ACM SIGPLAN Notices, v.34 n.9, p.183-196, Sept. 1999
	Thomas Colcombet , Pascal Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 19-21, 2000, Boston, MA, USA
	Ciarán Bryce , Chrislain Razafimahefa, An approach to safe object sharing, ACM SIGPLAN Notices, v.35 n.10, p.367-381, Oct. 2000
	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
	Steve Zdancewic , Dan Grossman , Greg Morrisett, Principals in programming languages: a syntactic proof technique, ACM SIGPLAN Notices, v.34 n.9, p.197-207, Sept. 1999
	Christian Skalka , Scott Smith, Static enforcement of security with types, ACM SIGPLAN Notices, v.35 n.9, p.34-45, Sept. 2000
	David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, ACM SIGPLAN Notices, v.33 n.10, p.48-64, Oct. 1998
	Benjamin C. Pierce, Type systems, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
	Neal Glew , Greg Morrisett, Type-safe linking and modular assembly language, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-261, January 20-22, 1999, San Antonio, Texas, United States
	Dan Grossman , Greg Morrisett , Steve Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.6, p.1037-1080, Nov. 2000
	Gleb Naumovich, A conservative algorithm for computing the flow of permissions in Java programs, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	Zhichen Xu , Barton P. Miller , Thomas Reps, Safety checking of machine code, ACM SIGPLAN Notices, v.35 n.5, p.70-82, May 2000
	Lujo Bauer , Andrew W. Appel , Edward W. Felten, Mechanisms for secure modular programming in Java, Software—Practice & Experience, v.33 n.5, p.461-480, 25 April 2003
	Dave Clarke , Michael Richmond , James Noble, Saving the world from bad beans: deployment-time confinement checking, ACM SIGPLAN Notices, v.38 n.11, November 2003
	Tian Zhao , Jens Palsberg , Jan Vitek, Type-based confinement, Journal of Functional Programming, v.16 n.1, p.83-128, January 2006
	Seng Wai Loke , Andrew Davison, Secure Prolog-based mobile code, Theory and Practice of Logic Programming, v.1 n.3, p.321-357, May 2001