{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:39:45Z","timestamp":1725493185765},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008866"},{"type":"electronic","value":"9783540365754"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36575-3_1","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T21:52:15Z","timestamp":1193521935000},"page":"1-9","source":"Crossref","is-referenced-by-count":1,"title":["Computer Security from a Programming Language and Static Analysis Perspective"],"prefix":"10.1007","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"issue":"5","key":"1_CR1","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/324133.324266","volume":"46","author":"M. Abadi","year":"1999","unstructured":"Mart\u00edn Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749\u2013786, 1999.","journal-title":"Journal of the ACM"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi, Anindya Banerjee, Nevin Heintze, and Jon 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":"1_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/3-540-45315-6_2","volume-title":"Secrecy types for asymmetric communication","author":"M. Abadi","year":"2001","unstructured":"Mart\u00edn Abadi and Bruno Blanchet. Secrecy types for asymmetric communication. In Furio Honsell and Marino Miculan, editors, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, volume 2030 of Lecture Notes in Computer Science, pages 25\u201341. Springer-Verlag, 2001."},{"issue":"1","key":"1_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Mart\u00edn Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The Spi calculus. Information and Computation, 148(1):1\u201370, 1999.","journal-title":"Information and Computation"},{"key":"1_CR5","unstructured":"Ross Anderson. Security Engineering. John Wiley & Sons, 2001."},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/BFb0015258","volume-title":"Computer Science Today: Recent Trends and Developments","author":"R. Anderson","year":"1995","unstructured":"Ross Anderson and Roger Needham. Programming Satan\u2019s computer. In Computer Science Today: Recent Trends and Developments, number 1000 in Lecture Notes in Computer Science, pages 426\u2013441. Springer-Verlag, 1995."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Besson, Thomas de Grenier de Latour, and Thomas Jensen. Secure calling contexts for stack inspection. In Principles and Practice of Declarative Programming (PPDP 2002), pages 76\u201387. ACM Press, 2002.","DOI":"10.1145\/571157.571166"},{"key":"1_CR8","unstructured":"Luca Cardelli. Type systems. In Allen B. Tucker, editor, The Computer Science and Engineering Handbook. CRC Press, 1997."},{"key":"1_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Context inference for static analysis of java card object sharing","author":"D. Caromel","year":"2001","unstructured":"Denis Caromel, Ludovic Henrio, and Bernard Serpette. Context inference for static analysis of java card object sharing. In Proceedings e-Smart 2001, volume 2140 of Lecture Notes in Computer Science. Springer-Verlag, 2001."},{"key":"1_CR10","unstructured":"Zhiqun Chen. Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide. The Java Series. Addison-Wesley, 2000."},{"key":"1_CR11","unstructured":"Gennady Chugunov, Lars \u00e5Ake Fredlund, and Dilian Gurov. Model checking multiapplet Java Card applications. In Smart Card Research and Advanced Applications Conference (CARDIS\u201902), 2002."},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Thomas Colcombet and Pascal Fradet. Enforcing trace properties by program transformation. In 27th symposium Principles of Programming Languages, pages 54\u201366. ACM Press, 2000.","DOI":"10.1145\/325694.325703"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Karl Crary and JosephC. Vanderwaart. An expressive, scalable type theory for certified code. In International Conference on Functional Programming 2002. ACM Press, 2002.","DOI":"10.1145\/581478.581497"},{"key":"1_CR14","unstructured":"Damien Deville and Gilles Grimaud. Building an \u201cimpossible\u201d verifier on a Java Card. In USENIX Workshop on Industrial Experiences with Systems Software (WIESS\u201902), 2002."},{"key":"1_CR15","unstructured":"U. Erlingsson and Fred B. Schneider. IRM enforcement of Java stack inspection. In Symposium on Security and Privacy. IEEE Computer Society Press, 2000."},{"key":"1_CR16","unstructured":"Morrie Gasser. Building a secure computer system. Van Nostrand Reinhold Co., 1988."},{"key":"1_CR17","unstructured":"Li Gong. Inside Java 2 platform security: architecture, API design, and implementation. The Java Series. Addison-Wesley, 1999."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"James A. Gosling. Java intermediate bytecodes. In Proc. ACM SIGPLAN Workshop on Intermediate Representations, pages 111\u2013118. ACM, 1995.","DOI":"10.1145\/202529.202541"},{"issue":"4","key":"1_CR19","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/503112.503115","volume":"33","author":"P. H. Hartel","year":"2001","unstructured":"Pieter H. Hartel and Luc A. V. Moreau. Formalizing the safety of Java, the Java virtual machine and Java Card. ACM Computing Surveys, 33(4):517\u2013558, 2001.","journal-title":"ACM Computing Surveys"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Nevin Heintze and Jon 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":"1_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Aspect-oriented programming","author":"G. Kiczales","year":"1997","unstructured":"Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina Videira Lopes, Jean-Marc Loingtier, and John Irwin. Aspect-oriented programming. In European Conference on Object-Oriented Programming (ECOOP\u201997), number 1241 in Lecture Notes in Computer Science. Springer-Verlag, 1997."},{"key":"1_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/3-540-68697-5_9","volume-title":"Timing attacks on implementations of Diffe-Hellman, RSA, DSS, and other systems","author":"P. C. Kocher","year":"1996","unstructured":"Paul C. Kocher. Timing attacks on implementations of Diffe-Hellman, RSA, DSS, and other systems. In Proceedings Crypto\u2019 96, number 1109 in Lecture Notes in Computer Science, pages 104\u2013113. Springer-Verlag, 1996."},{"key":"1_CR23","unstructured":"Markus Kuhn. Tamper resistance-a cautionary note. In USENIX Workshop on Electronic Commerce proceedings, pages 1\u201311, 1996."},{"key":"1_CR24","unstructured":"Markus Kuhn. Design principles for tamper-resistant smartcard processors. In USENIX Workshop on Smartcard Technology proceedings, 1999."},{"key":"1_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-44585-4_26","volume-title":"Computer Aided Verification, CAV 2001","author":"X. Leroy","year":"2001","unstructured":"Xavier Leroy. Java bytecode verification: an overview. In G. Berry, H. Comon, and A. Finkel, editors, Computer Aided Verification, CAV 2001, volume 2102 of Lecture Notes in Computer Science, pages 265\u2013285. Springer-Verlag, 2001."},{"key":"1_CR26","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1002\/spe.438","volume":"32","author":"X. Leroy","year":"2002","unstructured":"Xavier Leroy. Bytecode verification for Java smart card. Software Practice & Experience, 32:319\u2013340, 2002.","journal-title":"Software Practice & Experience"},{"key":"1_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-48749-2_7","volume-title":"Secure Internet Programming-Security issues for Mobile and Distributed Objects","author":"X. Leroy","year":"1999","unstructured":"Xavier Leroy and Fran\u015fcois Rouaix. Security properties of typed applets. In J. Vitek and C. Jensen, editors, Secure Internet Programming-Security issues for Mobile and Distributed Objects, volume 1603 of Lecture Notes in Computer Science, pages 147\u2013182. Springer-Verlag, 1999."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. The Java Series. Addison-Wesley, 1999. Second edition.","DOI":"10.1007\/978-3-642-95851-9_5"},{"key":"1_CR29","unstructured":"Sergio Loureiro, Laurent Bussard, and Yves Roudier. Extending tamper-proof hardware security to untrusted execution environments. In USENIX Smart Card Research and Advanced Application Conference (CARDIS\u201902), 2002."},{"issue":"1","key":"1_CR30","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1017\/S0956796801004178","volume":"12","author":"G. Morrisett","year":"2002","unstructured":"Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. Journal of Functional Programming, 12(1):43\u201388, 2002.","journal-title":"Journal of Functional Programming"},{"issue":"3","key":"1_CR31","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528\u2013569, 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"George C. Necula. Proof-carrying code. In 24th symposium Principles of Programming Languages, pages 106\u2013119. ACM Press, 1997.","DOI":"10.1145\/263699.263712"},{"key":"1_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-68671-1_5","volume-title":"Mobile Agents and Security","author":"G. C. Necula","year":"1997","unstructured":"George C. Necula and Peter Lee. Safe, untrusted agents using proof-carrying code. In Giovanni Vigna, editor, Mobile Agents and Security, volume 1419 of Lecture Notes in Computer Science, pages 61\u201391. Springer-Verlag, 1997."},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Fran\u015fois Pottier and Sylvain Conchon. Information flow inference for free. In International Conference on Functional Programming 2000, pages 46\u201357. ACM Press, 2000.","DOI":"10.1145\/357766.351245"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Fran\u015fois Pottier and Vincent Simonet. Information flow inference for ML. In 29th symposium Principles of Programming Languages, pages 319\u2013330. ACM Press, 2002.","DOI":"10.1145\/565816.503302"},{"key":"1_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-45309-1_3","volume-title":"A systematic approach to static access control","author":"F. Pottier","year":"2001","unstructured":"Fran\u00e7ois Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. In David Sands, editor, Proceedings of the 10th European Symposium on Programming (ESOP\u201901), volume 2028 of Lecture Notes in Computer Science, pages 30\u201345. Springer-Verlag, 2001."},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 2(4), 2000.","DOI":"10.1145\/353323.353382"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Zhong Shao, Bratin Saha, Valery Trifonov, and Nikolaos Papaspyrou. A type system for certified binaries. In 29th symposium Principles of Programming Languages, pages 217\u2013232. ACM Press, 2002.","DOI":"10.1145\/503272.503293"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Sean W. Smith and Steve Weingart. Building a high-performance, programmable secure coprocessor. Technical Report RC 21102, IBM Research, 1998.","DOI":"10.1007\/BFb0055474"},{"key":"1_CR40","series-title":"Lect Notes Comput Sci","volume-title":"Enforcing security properties by type specialization","author":"P. Thiemann","year":"2001","unstructured":"Peter Thiemann. Enforcing security properties by type specialization. In European Symposium on Programming 2001, volume 2028 of Lecture Notes in Computer Science. Springer-Verlag, 2001."},{"key":"1_CR41","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"A type-based approach to program security","author":"D. Volpano","year":"1997","unstructured":"Dennis Volpano and Geoffrey 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":"1_CR42","first-page":"1","volume":"4","author":"D. Volpano","year":"1996","unstructured":"Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):1\u201321, 1996.","journal-title":"Journal of Computer Security"},{"issue":"5","key":"1_CR43","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/173668.168635","volume":"27","author":"R. Wahbe","year":"1993","unstructured":"Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. Efficient software-based fault isolation. ACM SIGOPS Operating Systems Review, 27(5):203\u2013216, 1993.","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"David Walker. A type system for expressive security policies. In 27th symposium Principles of Programming Languages, pages 254\u2013267. ACM Press, 2000.","DOI":"10.1145\/325694.325728"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Dan S. Wallach, Edward W. Felten, and Andrew W. Appel. The security architecture formerly known as stack inspection: A security mechanism for language-based systems. ACM Transactions on Software Engineering and Methodology, 9(4), 2000.","DOI":"10.1145\/363516.363520"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Hongwei Xi and Robert Harper. A dependently typed assembly language. In International Conference on Functional Programming\u2019 01, pages 169\u2013180. ACM Press, 2001.","DOI":"10.1145\/507635.507657"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Programming Language Design and Implementation 1998, pages249\u2013257. ACM Press, 1998.","DOI":"10.1145\/277650.277732"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36575-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T15:04:39Z","timestamp":1684076679000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36575-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008866","9783540365754"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/3-540-36575-3_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}