{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:07Z","timestamp":1749125167318,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540661306"},{"type":"electronic","value":"9783540487494"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48749-2_7","type":"book-chapter","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T12:22:57Z","timestamp":1192796577000},"page":"147-182","source":"Crossref","is-referenced-by-count":10,"title":["Security Properties of Typed Applets"],"prefix":"10.1007","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Rouaix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/BFb0014571","volume-title":"Theoretical Aspects of Computer Software\u2019 97","author":"M. Abadi","year":"1997","unstructured":"M. Abadi. Secrecy by typing in security protocols. In Theoretical Aspects of Computer Software\u2019 97, volume 1281 of Lecture Notes in Computer Science, pages 611\u2013638. Springer-Verlag, Sept. 1997."},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In 26th symposium Principles of Programming Languages, pages 147\u2013160. ACM Press, 1999.","DOI":"10.1145\/292540.292555"},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/3-540-63141-0_5","volume-title":"CONCUR\u201997: Concurrency Theory","author":"M. Abadi","year":"1997","unstructured":"M. Abadi and A. D. Gordon. Reasoning about cryptographic protocols in the Spi calculus. In CONCUR\u201997: Concurrency Theory, volume 1243 of Lecture Notes in Computer Science, pages 59\u201373. Springer-Verlag, July 1997."},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/65.690959","volume":"12","author":"D. S. Alexander","year":"1998","unstructured":"D. S. Alexander, W. A. Arbaugh, M. W. Hicks, P. Kakkar, A. D. Keromytis, J. T. Moore, C. A. Gunter, S. M. Nettles, and J. M. Smith. The SwitchWare active network architecture. IEEE Network, 12(3):29\u201336, 1998.","journal-title":"IEEE Network"},{"key":"7_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Secure Internet Programming","author":"D. S. Alexander","year":"1999","unstructured":"D. S. Alexander, W. A. Arbaugh, A. D. Keromytis, and J. M. Smith. Security in active networks. In J. Vitek and C. Jensen, editors, Secure Internet Programming, Lecture Notes in Computer Science. Springer-Verlag Inc., New York, NY, USA, 1999."},{"key":"7_CR6","unstructured":"J.-P. Ban\u00e2tre and C. Bryce. A security proof system for networks of communicating processes. Research report 2042, INRIA, Sept. 1993."},{"key":"7_CR7","unstructured":"J.-P. Billon. Security breaches in the JDK 1.1 beta2 security API. Dyade, http:\/\/www.dyade.fr\/fr\/actions\/VIP\/SecHole.html , Jan. 1997."},{"key":"7_CR8","unstructured":"N. S. Borenstein. Email with a mind of its own: the Safe-Tcl language for enabled mail. In IFIP International Working Conference on Upper Layer Protocols, Architectures and Applications, 1994."},{"issue":"1","key":"7_CR9","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/0890-5401(91)90055-7","volume":"93","author":"V. Breazu-Tannen","year":"1991","unstructured":"V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93(1):172\u2013221, 1991.","journal-title":"Information and Computation"},{"key":"7_CR10","unstructured":"K. Brunnstein. Hostile ActiveX control demonstrated. RISKS Forum, 18(82), Feb. 1997."},{"issue":"1\u20132","key":"7_CR11","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1006\/inco.1994.1013","volume":"109","author":"L. Cardelli","year":"1994","unstructured":"L. Cardelli, S. Martini, J. C. Mitchell, and A. Scedrov. An extension of system F with subtyping. Information and Computation, 109(1\u20132):4\u201356, 1994.","journal-title":"Information and Computation"},{"key":"7_CR12","unstructured":"D. Dean, E. W. Felten, D. S. Wallach, and D. Balfanz. Java security: Web browsers and beyond. In D. E. Denning and P. J. Denning, editors, Internet Besieged: Countering Cyberspace Scofflaws, pages 241\u2013269. ACM Press, 1997."},{"issue":"5","key":"7_CR13","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D. E. Denning","year":"1976","unstructured":"D. E. Denning. A lattice model of secure information flow. Commun. ACM, 19(5):236\u2013242, 1976.","journal-title":"Commun. ACM"},{"issue":"7","key":"7_CR14","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D. E. Denning","year":"1977","unstructured":"D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Commun. ACM, 20(7):504\u2013513, 1977.","journal-title":"Commun. ACM"},{"key":"7_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BFb0053388","volume-title":"Proc. 11th European Conference on Object Oriented Programming","author":"S. Drossopoulou","year":"1997","unstructured":"S. Drossopoulou and S. Eisenbach. Java is type safe \u2014 probably. In Proc. 11th European Conference on Object Oriented Programming, volume 1241 of Lecture Notes in Computer Science, pages 389\u2013418. Springer-Verlag, June 1997."},{"key":"7_CR16","unstructured":"M. Erdos, B. Hartman, and M. Mueller. Security reference model for the Java Developer\u2019s Kit 1.0.2. JavaSoft, http:\/\/java.sun.com\/security\/SRM.html , Nov. 1996."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"S. N. Freund and J. C. Mitchell. A type system for object initialization in the Java bytecode language. In Object-Oriented Programming Systems, Languages and Applications 1998, pages 310\u2013327. ACM Press, 1998.","DOI":"10.1145\/286942.286972"},{"key":"7_CR18","unstructured":"L. Gong. Java security architecture (JDK1.2). JavaSoft, http:\/\/java.sun.com\/products\/jdk\/1.2\/docs\/guide\/security\/spec\/security-spec.doc.html , Oct. 1998."},{"key":"7_CR19","unstructured":"J. Gosling and H. McGilton. The Java language environment \u2014 a white paper. JavaSoft, http:\/\/java.sun.com\/docs\/white\/langenv , May 1996."},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In 25th symposium Principles of Programming Languages, pages 365\u2013377. ACM Press, 1998.","DOI":"10.1145\/268946.268976"},{"key":"7_CR21","unstructured":"D. Hopwood. Java security bug (applets can load native methods). RISKS Forum, 17(83), Mar. 1996."},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"T. Jensen, D. Le M\u00e9tayer, and T. Thorn. Security and dynamic class loading in Java: A formalisation. In International Conference on Computer Languages 1998, pages 4\u201315. IEEE Computer Society Press, 1998.","DOI":"10.1109\/ICCL.1998.674152"},{"key":"7_CR23","unstructured":"X. Leroy. Polymorphic typing of an algorithmic language. Research report 1778, INRIA, 1992."},{"key":"7_CR24","unstructured":"X. Leroy, J. Vouillon, D. Doligez, et al. The Objective Caml system. Software and documentation available on the Web, http:\/\/caml.inria.fr\/ocaml\/ , 1996."},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper, and D. MacQueen. The definition of Standard ML (revised). The MIT Press, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In Functional Programming Languages and Computer Architecture 1995, pages 66\u201377. ACM Press, 1995.","DOI":"10.1145\/224164.224182"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"G. C. Necula. Proof-carrying code. In 24th symposium Principles of Programming Languages, pages 106\u2013119. ACM Press, 1997.","DOI":"10.1145\/263699.263712"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"G. C. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proc. Symp. Operating Systems Design and Implementation, pages 229\u2013243. Usenix association, 1996.","DOI":"10.1145\/248155.238781"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"T. Nipkow and D. von Oheimb. JavaLight is type-safe \u2014 definitely. In 25th symposium Principles of Programming Languages, pages 161\u2013170. ACM Press, 1998.","DOI":"10.1145\/268946.268960"},{"issue":"4","key":"7_CR30","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/210184.210187","volume":"17","author":"J. Palsberg","year":"1995","unstructured":"J. Palsberg and P. O\u2019Keefe. A type system equivalent to flow analysis. ACM Trans. Prog. Lang. Syst., 17(4):576\u2013599, 1995.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"issue":"6","key":"7_CR31","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1017\/S0956796897002906","volume":"7","author":"J. Palsberg","year":"1997","unstructured":"J. Palsberg and P. \u00d8rbaek. Trust in the \u03bb-calculus. Journal of Functional Programming, 7(6):557\u2013591, 1997.","journal-title":"Journal of Functional Programming"},{"key":"7_CR32","unstructured":"G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981."},{"key":"7_CR33","series-title":"Lect Notes Comput Sci","volume-title":"Formal Syntax and Semantics of Java","author":"Z. Qian","year":"1998","unstructured":"Z. Qian. A formal specification of a large subset of Java Virtual Machine instructions. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, Lecture Notes in Computer Science. Springer-Verlag, 1998. To appear."},{"key":"7_CR34","unstructured":"J. C. Reynolds. User-defined types and procedural data structures as comple mentary approaches to data abstraction. In C. Gunter and J. Mitchell, editors, Theoretical aspects of object-oriented programming, pages 13\u201323. MIT Press, 1994."},{"key":"7_CR35","first-page":"1365","volume":"28","author":"F. Rouaix","year":"1996","unstructured":"F. Rouaix. A Web navigator with applets in Caml. In Proceedings of the 5th International World Wide Web Conference, Computer Networks and Telecommunications Networking, volume 28, pages 1365\u20131371. Elsevier, May 1996.","journal-title":"Proceedings of the 5th International World Wide Web Conference, Computer Networks and Telecommunications Networking"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"R. Stata and M. Abadi. A type system for Java bytecode subroutines. In 25th symposium Principles of Programming Languages, pages 149\u2013160. ACM Press, 1998.","DOI":"10.1145\/268946.268959"},{"key":"7_CR37","unstructured":"D. Syme. Proving JavaS type soundness. Technical Report 427, University of Cambridge Computer Laboratory, June 1997."},{"issue":"2","key":"7_CR38","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"J.-P. Talpin","year":"1994","unstructured":"J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111(2):245\u2013296, 1994.","journal-title":"Information and Computation"},{"issue":"1","key":"7_CR39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"Mads Tofte","year":"1990","unstructured":"M. Tofte. Type inference for polymorphic references. Information and Computation, 89(1), 1990.","journal-title":"Information and Computation"},{"key":"7_CR40","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"Proceedings of TAPSOFT\u201997, Colloquium on Formal Approaches in Software Engineering","author":"D. Volpano","year":"1997","unstructured":"D. Volpano and G. Smith. A type-based approach to program security. In Proceedings of TAPSOFT\u201997, Colloquium on Formal Approaches in Software Engineering, volume 1214 of Lecture Notes in Computer Science, pages 607\u2013621. Springer-Verlag, 1997."},{"issue":"3","key":"7_CR41","first-page":"1","volume":"4","author":"D. Volpano","year":"1996","unstructured":"D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):1\u201321, 1996.","journal-title":"Journal of Computer Security"},{"key":"7_CR42","doi-asserted-by":"crossref","unstructured":"D. S. Wallach, D. Balfanz, D. Dean, and E. W. Felten. Extensible security architectures for Java. Technical report 546-97, Department of Computer Science, Princeton University, Apr. 1997.","DOI":"10.1145\/268998.266668"},{"key":"7_CR43","unstructured":"D. S. Wallach and E. W. Felten. Understanding Java stack inspection. In Proceedings of the 1998 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 1998."},{"key":"7_CR44","doi-asserted-by":"crossref","unstructured":"F. Yellin. Low level security in Java. In Proceedings of the Fourth International World Wide Web Conference, pages 369\u2013379. O\u2019Reilly, 1995.","DOI":"10.1145\/3592626.3592656"}],"container-title":["Lecture Notes in Computer Science","Secure Internet Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48749-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T19:23:31Z","timestamp":1737487411000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48749-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540661306","9783540487494"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/3-540-48749-2_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}