Formalizing the safety of Java, the Java virtual machine, and Java card

ABSTRACT

We review the existing literature on Java safety, emphasizing formal approaches, and the impact of Java safety on small footprint devices such as smartcards. The conclusion is that although a lot of good work has been done, a more concerted effort is needed to build a coherent set of machine-readable formal models of the whole of Java and its implementation. This is a formidable task but we believe it is essential to build trust in Java safety, and thence to achieve ITSEC level 6 or Common Criteria level 7 certification for Java programs.

REFERENCES

• 1: Martín Abadi, Protection in programming-language translations, Secure Internet programming: security issues for mobile and distributed objects, Springer-Verlag, London, 2001
• 2: 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]
• 3: Erika Ábrahám-Mumm , Frank S. de Boer, Proof-Outlines for Threads in Java, Proceedings of the 11th International Conference on Concurrency Theory, p.229-242, August 22-25, 2000
• 4: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 5: Ole Agesen , David Detlefs , J. Eliot Moss, Garbage collection and local variable type-precision and liveness in Java virtual machines, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.269-279, June 17-19, 1998, Montreal, Quebec, Canada
• 6: Ole Agesen , Stephen N. Freund , John C. Mitchell, Adding type parameterization to the Java language, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.49-65, October 05-09, 1997, Atlanta, Georgia, United States
• 7: Mustaque Ahamad , Rida A. Bazzi , Ranjit John , Prince Kohli , Gil Neiger, The power of processor consistency, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.251-260, June 30-July 02, 1993, Velen, Germany [doi>10.1145/165231.165264]
• 8: Jonathan Aldrich , Craig Chambers , Emin Gün Sirer , Susan J. Eggers, Static Analyses for Eliminating Unnecessary Synchronization from Java Programs, Proceedings of the 6th International Symposium on Static Analysis, p.19-38, September 22-24, 1999
• 9: Jim Alves-Foss , Fong Shing Lam, Dynamic Denotational Semantics of Java, Formal Syntax and Semantics of Java, p.201-240, January 1999
• 10: ANDERSON,T.AND WITTY, R. W. 1978. Safe programming. BIT 18, 1-8.
• 11: Gabriel Antoniu , Luc Bougé , Philip J. Hatcher , Mark MacBeth , Keith McGuigan , Raymond Namyst, Compiling Multithreaded Java Bytecode for Distributed Execution (Distinguished Paper), Proceedings from the 6th International Euro-Par Conference on Parallel Processing, p.1039-1052, August 29-September 01, 2000
• 12: Yariv Aridor , Michael Factor , Avi Teperman, cJVM: A Single System Image of a JVM on a Cluster, Proceedings of the 1999 International Conference on Parallel Processing, p.4, September 21-24, 1999
• 13: Y. Aridor , M. Factor , A. Teperman , T. Eilam , A. Schuster, A high performance cluster JVM presenting a pure single system image, Proceedings of the ACM 2000 conference on Java Grande, p.168-177, June 03-04, 2000, San Francisco, California, United States [doi>10.1145/337449.337543]
• 14: ATTALI, I., CAROMEL,D.,AND RUSSO, M. 1998. A formal executable semantics for Java. In OOPSLA'98 Workshop on Formal Underpinnings of Java (FUJ) (Vancouver, Canada, Nov.), pp. Paper 11. Dept. of Computing, Imperial College London.
• 15: Isabelle Attali , Denis Caromel , Carine Courbis , Ludovic Henrio , Henrik Nilsson, Smart tools for Java Cards, Proceedings of the fourth working conference on smart card research and advanced applications on Smart card research and advanced applications, p.155-177, February 2001, Bristol, United Kingdom
• 16: BALFANZ,D.AND FELTEN, E. W. 1997. A Java filter. Tech. Rep. 567-97 (Sept.), Dept. of Computer Science, Princeton Univ.
• 17: David A. Basin , Stefan Friedrich , Joachim Posegga , Harald Vogt, Java Bytecode Verification by Model Checking, Proceedings of the 11th International Conference on Computer Aided Verification, p.491-494, July 06-10, 1999
• 18: Peter Bertelsen, Dynamic semantics of java bytecode, Future Generation Computer Systems, v.16 n.7, p.841-850, May 2000 [doi>10.1016/S0167-739X(99)00094-1]
• 19: BERTELSEN, P. 1997. Semantics of Java byte code. Tech. Rep. (Mar.), Technical Univ. of Denmark.
• 20: BERTELSEN,P.AND ANDERSON, S. 1996. The semantics of a core language derived from Java. Tech. Rep. (Sept.), Technical Univ. of Denmark.
• 21: BIEBER, P., CAZIN, J., WIELS, V., ZANON, G., GIRARD,P., AND LANET, J.-L. 1999. Electronic purse applet certification. In S. Schneider and P. Ryan, Eds., Workshop on Secure Architectures and Information Flow (Royal Holloway, London, Dec.). Electronics Notes in Theoretical Computer Science, 32.
• 22: G. Bigliardi , C. Laneve, A Type System for JVM Threads, University of Bologna, 2000
• 23: Jeff Bogda , Urs Hölzle, Removing unnecessary synchronization in Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.35-46, November 01-05, 1999, Denver, Colorado, United States
• 24: Egon Börger , Wolfram Schulte, Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation, Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science, p.17-35, August 24-28, 1998
• 25: BORGER,E.AND SCHULTE, W. 1999a. Initialization problems for Java. Software Concepts and Tools 20, 4, 175-179.
• 26: Egon Börger , Wolfram Schulte, A Programmer Friendly Modular Definition of the Semantics of Java, Formal Syntax and Semantics of Java, p.353-404, January 1999
• 27: Egon Börger , Wolfram Schulte, Modular design for the Java virtual machine architecture, Architecture design and validation methods, Springer-Verlag New York, Inc., Secaucus, NJ, 2000
• 28: Egon Börger , Wolfram Schulte, A Practical Method for Specification and Analysis of Exception Handling-A Java/JVM Case Study, IEEE Transactions on Software Engineering, v.26 n.9, p.872-887, September 2000 [doi>10.1109/32.877847]
• 29: P. Borras , D. Clement , Th. Despeyroux , J. Incerpi , G. Kahn , B. Lang , V. Pascual, Centaur: the system, Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.14-24, November 28-30, 1988, Boston, Massachusetts, United States
• 30: BRACHA, G. 1999. A Critique of Security and Dynamic Loading in Java: A Formalization. Sun Java Software.
• 31: BRACHA, G., ODERSKY, M., STOUTAMIRE,D.,AND WADLER, P. 1998. GJ: Extending the Java programming language with type parameters. Tech. Rep. (Mar.), Bell Labs, Lucent Technologies.
• 32: Robert Cartwright , Guy L. Steele, Jr., Compatible genericity with run-time types for the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.201-215, October 18-22, 1998, Vancouver, British Columbia, Canada
• 33: CASSET,L.AND LANET, J.-L. 1999. A formal specification of the Java bytecode semantics using the B method. Technischer Bericht 251 (June), Fernuniversit~t Hagen, Lisbon, Portugal.
• 34: CENCIARELLI, P. 1999. Towards a modular denotational semantics of Java. Technischer Bericht 251 (June), Fernuniversit~t Hagen, Lisbon, Portugal.
• 35: Pietro Cenciarelli , Alexander Knapp , Bernhard Reus , Martin Wirsing, An Event-Based Structural Operational Semantics of Multi-Threaded Java, Formal Syntax and Semantics of Java, p.157-200, January 1999
• 36: CHEN,X.AND ALLAN, V. 1998. MultiJav: A distributed shared memory system based on multiple Java virtual machines. In Conference on Parallel and Distributed Processing Techniques and Applications (PDTA'98) (Las Vegas, Nevada, June).
• 37: Zhiqun Chen, Java Card Technology for Smart Cards: Architecture and Programmer's Guide, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 38: Jong-Deok Choi , Manish Gupta , Mauricio Serrano , Vugranam C. Sreedhar , Sam Midkiff, Escape analysis for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-19, November 01-05, 1999, Denver, Colorado, United States
• 39: COGLIO,A.AND GOLDBERG, A. 2000. Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions. Kestrel Institute, Palo Alto, Calif.
• 40: COGLIO, A., GOLDBERG, A., AND QIAN, Z. 1998. Toward a provably-correct implementation of the JVM bytecode verifier. In OOPSLA '98 Workshop on Formal Underpinnings of Java (FUJ) (Vancouver, Canada, Nov.), pp. Paper 6. Dept. of Computing, Imperial College London.
• 41: COHEN, R. M. 1997. The defensive Java virtual machine specification version 0.5. Tech. rep. (May), Computational Logic Inc, Austin, Texas.
• 42: Susan Eisenbach, Formal underpinnings of Java, Addendum to the 1998 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), January 1998, Vancouver, British Columbia, Canada [doi>10.1145/346852.346968]
• 43: Christopher Colby , Peter Lee , George C. Necula , Fred Blau , Mark Plesko , Kenneth Cline, A certifying compiler for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.95-107, June 18-21, 2000, Vancouver, British Columbia, Canada
• 44: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 45: COSCIA,E.AND REGGIO, G. 1998a. An operational semantics for Java. Tech. Rep. (Nov.), DISI, Univ. of Genova, Italy.
• 46: COSCIA,E.AND REGGIO, G. 1998b. A proposal for a semantics of a subset of multi-threaded 'good' Java programs. In OOPSLA '98 Work-shop on Formal Underpinnings of Java (FUJ) (Vancouver, Canada, Nov.), pp. Paper 10. Dept. of Computing, Imperial College London.
• 47: Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
• 48: Drew Dean, The security of static typing with dynamic linking, Proceedings of the 4th ACM conference on Computer and communications security, p.18-27, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266428]
• 49: 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
• 50: DEMARTINI, C., IOSIF, R., AND SISTO, R. 1998. Modeling and validation of Java multithreading applications using SPIN. In 4th Spin Workshop (Paris, France, Nov.).
• 51: Ewen Denney , Thomas P. Jensen, Correctness of Java Card Method Lookup via Logical Relations, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.104-118, April 02, 2000
• 52: DETLEFS, D. L., LEINO,K.R.M.,NELSON,G.,AND SAXE, J. B. 1998. Extended static checking. SRC Research Rep. 159 (Dec), Compaq Systems Research Center, Palo Alto, Calif.
• 53: Stephen Diehl, A formal introduction to the compilation of Java, Software—Practice & Experience, v.28 n.3, p.297-327, March 1998 [doi>10.1002/(SICI)1097-024X(199803)28:3<297::AID-SPE156>3.0.CO;2-M]
• 54: Sophia Drossopoulou, An Abstract Model of Java Dynamic Linking and Loading, Selected papers from the Third International Workshop on Types in Compilation, p.53-84, September 21, 2000
• 55: DROSSOPOULOU,S.AND EISENBACH, S. 1997. Java is type safe-Probably. In M. Aksit and S. Matsuoka, Eds., 11th European Conference on Object Oriented Programming, ECOOP, LNCS 1241 (Jyvaskyla, Finland, June), pp. 389-418. Springer-Verlag, Berlin.
• 56: Sophia Drossopoulou , Susan Eisenbach, Describing the Semantics of Java and Proving Type Soundness, Formal Syntax and Semantics of Java, p.41-82, January 1999
• 57: DROSSOPOULOU,S.AND VALKEVYCH, T. 2000. Java Exceptions Throw No Surprises. Department of Computing, Imperial College, London.
• 58: Sophia Drossopoulou , Susan Eisenbach , David Wragg, A Fragment Calculus Towards a Model of Separate Compilation, Linking and Binary Compatibility, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.147, July 02-05, 1999
• 59: Sophia Drossopoulou , Susan Eisenbach , Sarfraz Khurshid, Is the Java type system sound?, Theory and Practice of Object Systems, v.5 n.1, p.3-24, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<3::AID-TAPO2>3.0.CO;2-T]
• 60: Sophia Drossopoulou , David Wragg , Susan Eisenbach, What is Java binary compatibility?, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.341-361, October 18-22, 1998, Vancouver, British Columbia, Canada
• 61: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 62: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 63: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, A Programmer's Reduction Semantics for Classes and Mixins, Formal Syntax and Semantics of Java, p.241-269, January 1999
• 64: Wan Fokkink , Chris Verhoef, A conservative look at operational semantics with variable binding, Information and Computation, v.146 n.1, p.24-54, Oct. 10, 1998 [doi>10.1006/inco.1998.2729]
• 65: Philip W. L. Fong , Robert D. Cameron, Proof linking: an architecture for modular verification of dynamically-linked mobile code, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.222-230, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 66: FREUND, S. N. 1998. The costs and benefits of Java bytecode subroutines. In OOPSLA '98 Work-shop on Formal Underpinnings of Java (FUJ) (Vancouver, Canada, Nov.), pp. Paper 2. Dept. of Computing, Imperial College London.
• 67: Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.310-327, October 18-22, 1998, Vancouver, British Columbia, Canada
• 68: Stephen N. Freund , John C. Mitchell, A formal framework for the Java bytecode language and verifier, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.147-166, November 01-05, 1999, Denver, Colorado, United States
• 69: Stephen N. Freund , John C. Mitchell, The type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.6, p.1196-1250, Nov. 1999 [doi>10.1145/330643.330646]
• 70: FRITZINGER,J.S.AND MUELLER, M. 1996. Java Security. Sun Microsystems Inc, Mountain View, Calif.
• 71: GAGNON,E.AND HENDREN, L. 1999. Intraprocedural inference of static types. Tech. Rep. 1999-1 (Mar.), Sable Group, McGill University, Montreal, Canada.
• 72: S. Glesner , W. Zimmermann, Using many-sorted natural semantics to specify and generate semantic analysis, Proceedings of the IFIP TC2 WG2.4 working conference on Systems implementation 2000 : languages, methods and tools: languages, methods and tools, p.249-262, January 1998, Berlin, Germany
• 73: Allen Goldberg, A specification of Java loading and bytecode verification, Proceedings of the 5th ACM conference on Computer and communications security, p.49-58, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288104]
• 74: Li Gong, Secure Java Class Loading, IEEE Internet Computing, v.2 n.6, p.56-61, November 1998 [doi>10.1109/4236.735987]
• 75: Alex Gontmakher , Assaf Schuster, Java consistency: nonoperational characterizations for Java memory behavior, ACM Transactions on Computer Systems (TOCS), v.18 n.4, p.333-386, Nov. 2000 [doi>10.1145/362670.362673]
• 76: Rajeev Goré , Joachim Posegga , Andrew Slater , Harald Vogt, System Description: cardTAP: The First Theorem Prover on a Smart Card, Proceedings of the 15th International Conference on Automated Deduction: Automated Deduction, p.47-50, July 05-10, 1998
• 77: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 78: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java Language Specification, Second Edition: The Java Series, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 79: Yuri Gurevich, Evolving algebras 1993: Lipari guide, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
• 80: Masami Hagiya , Akihiko Tozawa, On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines, Proceedings of the 5th International Symposium on Static Analysis, p.17-32, September 14-16, 1998
• 81: Pieter H. Hartel, LETOS — a lightweight execution tool for operational semantics, Software—Practice & Experience, v.29 n.15, p.1379-1416, Dec. 25, 1999 [doi>10.1002/(SICI)1097-024X(19991225)29:15<1379::AID-SPE286>3.0.CO;2-V]
• 82: Pieter H. Hartel , Eduard de Jong, A Programming and a Modelling Perspective on the Evaluation of Java Card Implementations, Revised Papers from the First International Workshop on Java on Smart Cards: Programming and Security, p.52-72, September 14, 2000
• 83: Pieter H. Hartel , Michael J. Butler , Moshe Levy, The Operational Semantics of a Java Secure Processor, Formal Syntax and Semantics of Java, p.313-352, January 1999
• 84: HAVELUND,K.AND PRESSBURGER, T. 2000. Model checking Java programs using pathfinder. Software Tools for Technology Transfer 2, 4, 366-381.
• 85: Barry Hayes, Finalization in the Collector Interface, Proceedings of the International Workshop on Memory Management, p.277-298, September 17-19, 1992
• 86: HILDERINK, G., BROEKING, J., VERVOORT,W.,AND BAKKERS, A. 1997. Communicating Java threads. In 20th World Occam and Transputer User Group Technical Meeting (Enschede, The Netherlands, Apr.), pp. 48-76. IOS Press, Amsterdam.
• 87: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 88: HUISMAN, M. 2001. Reasoning about Java progams in higher order logic with PVS and Isabelle. PhD thesis, Univ. of Nijmegen, The Netherlands.
• 89: HUISMAN, M., JACOBS,B.,AND VAN DEN BERG,J. 2001. A case study in class library verification: Java's vector class. Software Tools for Technology Transfer, to appear.
• 90: HUMMEL, J., AZAVEDO, A., KOLSON,D.,AND NICOLAU,A. 1997. Annotating the Java bytecodes in support of optimization. Concurrency: Practice and Experience 9, 11 (Nov.), 1003-1016.
• 91: Atsushi Igarashi , Benjamin C. Pierce, On Inner Classes, Proceedings of the 14th European Conference on Object-Oriented Programming, p.129-153, June 12-16, 2000
• 92: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 93: ISO/IEC. 1995. 7816-4:1995 Information Technology- Identification Cards-Integrated Circuit(s) Cards with Contacts Part4: Inter-Industry Commands for Interchange. Int. Standards Organization.
• 94: ITSEC. 1993. Evaluation Criteria for IT Security Part 3: Assurance of IT Systems (version 1.2 ed.). INFOSEC Central Office, Brussels, Belgium.
• 95: Bart Jacobs, A Formalisation of Java's Exception Mechanism, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.284-301, April 02-06, 2001
• 96: Bart Jacobs , Erik Poll, A Monad for Basic Java Semantics, Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology, p.150-164, May 20-27, 2000
• 97: Bart Jacobs , Erik Poll, A Logic for the Java Modeling Language JML, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.284-299, April 02-06, 2001
• 98: Bart Jacobs , Joachim van den Berg , Marieke Huisman , Martijn van Berkum , U. Hensel , H. Tews, Reasoning about Java classes: preliminary report, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.329-340, October 18-22, 1998, Vancouver, British Columbia, Canada
• 99: T. Jensen , D. Le Métayer , T. Thorn, Security and Dynamic Class Loading in Java: A Formalization, Proceedings of the 1998 International Conference on Computer Languages, p.4, May 14-16, 1998
• 100: JENSEN, T., METAYER,D.L.,AND THORN, T. 1999. Verification of control flow based security properties. In Symp. on Security and Privacy (Oakland, California, May), pp. 89-103. IEEE Comput. Soc., Los Alamitos, Calif.
• 101: JONES, M. 1998. The functions of Java bytecode. In OOPSLA '98 Workshop on Formal Underpinnings of Java (FUJ) (Vancouver, Canada, Nov.), pp. Paper 3. Dept. of Computing, Imperial College London.
• 102: Lora Kassab , Steven J. Greenwald, Towards Formalizing the Java Security Architecture of JDK 1.2, Proceedings of the 5th European Symposium on Research in Computer Security, p.191-207, September 16-18, 1998
• 103: KAUFMANN,M.AND MOORE, J. S. 1996. ACL2: An industrial strength version of nqthm. In 11th Annual Conf. on Computer Assurance (COMPASS) (Gaithersburg, Md., June), pp.23-34.IEEE Computer Society Press, Los Alamitos, California.
• 104: KISTLER,T.AND FRANZ, M. 1996. A tree-based alternative to Java byte-codes. Tech. Rep. 96-58 (Dec.), Depart. of Information and Computer Science, Univ. of California, Irvine.
• 105: KLEIN,G.AND NIPKOW, T. 2000. Verified lightweight bytecode verification. In S. Drossopoulkou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Muller, and A. Poetzsch-Heffter, Eds., ECOOP'2000 Workshop on Formal Techniques for Java Programs (Sophia Antipolis, France, June), pp. 35- 42. Fernuniversitat Hagen.
• 106: Todd B. Knoblock , Jakob Rehof, Type elaboration and subtype completion for Java bytecode, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-242, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325725]
• 107: Dexter Kozen, Efficient Code Certification, Cornell University, Ithaca, NY, 1998
• 108: Jean Louis Lanet, Are Smart Cards the Ideal Domain for Applying Formal Methods?, Proceedings of the First International Conference of B and Z Users on Formal Specification and Development in Z and B, p.363-373, August 29-September 02, 2000
• 109: Jean Louis Lanet , Antoine Requet, Formal Proof of Smart Card Applets Correctness, Proceedings of the The International Conference on Smart Card Research and Applications, p.85-97, September 14-16, 1998
• 110: LEAVENS,G.T.,BAKER,A.L.,AND RUBY, C. 1999. JML: A notation for detailed design. In H. Kilov, B. Rumpe, and I. Simmonds, Eds., Behavioral Specifications of Business and Systems,pp. 175-188. Kluwer Academic, Boston/ Dordrecht/ London.
• 111: LEINO,K.R.M.,SAXE,J.B.,AND STATA, R. 1999. Checking Java programs via guarded commands. SRC Research Rep. 1999-002 (May), Compaq Systems Research Center, Palo Alto, Calif.
• 112: Sheng Liang , Gilad Bracha, Dynamic class loading in the Java virtual machine, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.36-44, October 18-22, 1998, Vancouver, British Columbia, Canada
• 113: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 114: Jan-Willem Maessen , Xiaowei Shen, Improving the Java memory model using CRF, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-12, October 2000, Minneapolis, Minnesota, United States
• 115: Dahlia Malkhi , Michael K. Reiter, Secure Execution of Java Applets Using a Remote Playground, IEEE Transactions on Software Engineering, v.26 n.12, p.1197-1209, December 2000 [doi>10.1109/32.888632]
• 116: MANSON,J.AND PUGH, W. 2001. Semantics of multithreaded Java. Tech. Rep. (Jan.), Dept. of Computer Science, University of Maryland.
• 117: Gary McGraw , Edward W. Felten, Securing Java: getting down to business with mobile code, John Wiley & Sons, Inc., New York, NY, 1999
• 118: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 119: MONTGOMERY,M.AND KRISHNA, K. 1999. Secure object sharing in Java card. In USENIX Workshop on Smartcard Technology (Smartcard '99) (Chicago), pp. 119-127. USENIX Assoc., Berkeley, Calif.
• 120: J. Strother Moore, Proving Theorems About Java-Like Byte Code, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), p.139-162, January 1999
• 121: José E. Moreira , Samuel P. Midkiff , Manish Gupta, From flop to megaflops: Java for technical computing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.265-295, March 2000 [doi>10.1145/349214.349222]
• 122: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 123: MORRISETT, G., FELLEISEN, M., AND HARPER, R. 1995. Abstract models of memory management. Tech. Rep. CMU-CS-95-110 (Jan.), School of Comp. Sci., Carnegie Mellon Univ.
• 124: MORRISETT, G., TARDITI, D., CHENG, P., STONE,C., HARPER, R., AND LEE, P. 1996. The TIL/ ML compiler: Performance and safety through types. In First Annual Workshop on Compiler Support for System Software (Tucson. Ariz., Feb.).
• 125: MOTRE, S. 2000. Formal model and implementaion of the Java card dynamic security policy. In Approches Formelles dans l'Assistance au Developpement de Logiciels-AFADL'2000 (Grenoble, France, Jan.).
• 126: Joseph A. Bank , Andrew C. Myers , Barbara Liskov, Parameterized types for Java, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.132-145, January 15-17, 1997, Paris, France [doi>10.1145/263699.263714]
• 127: NCSC. l985. Trusted Computer System Evaluation Criteria (Orange Book). U. S. Dept. of Defense, National Computer Security Center.
• 128: 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]
• 129: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 130: G. C. Necula , P. Lee, Efficient Representation and Validation of Proofs, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.93, June 21-24, 1998
• 131: George C. Necula , Peter Lee, Safe, Untrusted Agents Using Proof-Carrying Code, Mobile Agents and Security, p.61-91, January 1998
• 132: George C. Necula , S. P. Rahul, Oracle-based checking of untrusted software, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-154, January 2001, London, United Kingdom
• 133: Hanne Riis Nielson , Flemming Nielson, Semantics with applications: a formal introduction, John Wiley & Sons, Inc., New York, NY, 1992
• 134: NILSEN, K. 1998. picoPERC: a small-footprint dialect of Java. Dr. Dobb's Journal 23, 3 (Mar.), 50-54.
• 135: 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]
• 136: NIPKOW,T.,VON OHEIMB,D.,AND PUSCH, C. 2000. Java: Embedding a programming language in a theorem prover. In F. L. Bauer and R. Steinbruggen, Eds., Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf , pp. 117-144. IOS Press, Amsterdam.
• 137: NIST. 1999. Common Criteria for Information Technology Security Evaluation. U. S. Dept. of Commerce, National Bureau of Standards and Technology.
• 138: Robert O'Callahan, A simple, comprehensive type system for Java bytecode subroutines, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-78, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292549]
• 139: Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
• 140: Marcus Oestreicher, Transactions in Java Card, Proceedings of the 15th Annual Computer Security Applications Conference, p.291, December 06-10, 1999
• 141: OESTREICHER,M.AND KRISHNA, K. 1999. Object lifetimes in Java card. In USENIX Workshop on Smartcard Technology (Smartcard '99) (Chicago), pp. 129-37. USENIX Assoc, Berkeley, Calif.
• 142: Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995 [doi>10.1109/32.345827]
• 143: PAULSON, L. C. 1994. Isabelle: A Generic Theorem Prover, LNCS 828. Springer-Verlag, New York.
• 144: Arnd Poetzsch-Heffter , Peter Müller, A Programming Logic for Sequential Java, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.162-176, March 22-28, 1999
• 145: Erik Poll , Joachim van den Berg , Bart Jacobs, Specification of the Javacard API in JML, Proceedings of the fourth working conference on smart card research and advanced applications on Smart card research and advanced applications, p.135-154, February 2001, Bristol, United Kingdom
• 146: POLL, E., VAN DEN BERG,J.,AND JACOBS, B. 2001. Formal specification of the JavaCard API in JML: the APDU class. Computer Networks 36, 4(July), 407-421.
• 147: Joachim Posegga , Harald Vogt, Byte Code Verification for Java Smart Card Based on Model Checking, Proceedings of the 5th European Symposium on Research in Computer Security, p.175-190, September 16-18, 1998
• 148: PUGH, W. 2000. The Java memory model is fatally flawed. Concurrency: Practice and Experience 12, 1, 1-11.
• 149: PUSCH, C. 1998. Formalizing the Java virtual machine in Isabelle/HOL. Tech. Rep. TUM-I9816, Institut fur Informatik, Technische Univ. Munchen.
• 150: Cornelia Pusch, Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.89-103, March 22-28, 1999
• 151: Zhenyu Qian, A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subrountines, Formal Syntax and Semantics of Java, p.271-312, January 1999
• 152: QIAN, Z. 1999b. Standard Fixpoint Iteration for Java Bytecode Verification. Kestrel Institute, Palo Alto, Calif.
• 153: Zhenyu Qian , Allen Goldberg , Alessandro Coglio, A formal specification of Java class loading, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.325-336, October 2000, Minneapolis, Minnesota, United States
• 154: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• 155: REQUET, A. 2000. A B model for ensuring soundness of the Java card virtual machine. In S. Gnesi, I. Schieferdecker, and A. Rennoch, Eds., 5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS) (Berlin, Mar.), pp. 29-26. GMD.
• 156: ROSE, E. 1998. Towards secure bytecode verification on a Java card. Master's Thesis, DIKU, Univ. of Copenhagen.
• 157: ROSE,E.AND ROSE, K. H. 1998. Lightweight bytecode verification. In OOPSLA '98 Work-shop on Formal Underpinnings of Java (FUJ) (Vancouver, Canada, Nov. 1998), pp. Paper 7. Dept. of Computing, Imperial College London.
• 158: SARASWAT, V. 1997. Java is not type-safe. Tech. Rep. (Aug.), AT&T Research, Florham Park, New Jersey.
• 159: Manuel Serrano, Control flow analysis: a functional languages compilation paradigm, Proceedings of the 1995 ACM symposium on Applied computing, p.118-122, February 26-28, 1995, Nashville, Tennessee, United States [doi>10.1145/315891.315934]
• 160: SHIN,I.AND MITCHELL, J. C. 1998. Java bytecode modification and applet security. Tech. Rep., Comp. Sci. Dept., Stanford Univ.
• 161: Christian Skalka , Scott Smith, Static enforcement of security with types, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.34-45, September 2000
• 162: Vugranam C. Sreedhar , Michael Burke , Jong-Deok Choi, A framework for interprocedural optimization in the presence of dynamic class loading, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.196-207, June 18-21, 2000, Vancouver, British Columbia, Canada
• 163: Yellamraju V. Srinivas , Richard Jüllig, Specware: Formal Support for Composing Software, Mathematics of Program Construction, p.399-422, July 17-21, 1995
• 164: ST~RK, R. 1998. Foundations of Java-Lecture Notes for Computer Science Students. University of Fribourg, Switzerland.
• 165: Robert F. Stark , E. Borger , Joachim Schmid, Java and the Java Virtual Machine: Definition, Verification, Validation with Cdrom, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 166: Raymie Stata , Martín Abadi, A type system for Java bytecode subroutines, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-160, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268959]
• 167: Raymie Stata , Martin Abadi, A type system for Java bytecode subroutines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.90-137, Jan. 1999 [doi>10.1145/314602.314606]
• 168: K. Stephenson, Towards an Algebraic Specification of the Java Virtual Machine, Proceedings of the ESPRIT Working Group 8533 on Prospects for Hardware Foundations: NADA - New Hardware Design Methods, Survey Chapters, p.236-277, January 1998
• 169: STILES, G. S. 1998. Safe and verifiable design of multithreaded Java programs with CSP and FDR. In OOPSLA '98 Workshop on Formal Underpinnings of Java (FUJ) (Vancouver, Canada, Nov.), pp. Paper 12. Dept. of Computing, Imperial College London.
• 170: SUN. 1999. The K virtual machine (KVM)A white paper. Sun Microsystems Inc., Mountain View, Calif.
• 171: SUN. 2000. Connected Limited Devicde Specification Version 1.0, Java Platform 2 Micro Edition. Sun Microsystems Inc., Palo Alto, Calif.
• 172: Don Syme, Proving Java Type Soundness, Formal Syntax and Semantics of Java, p.83-118, January 1999
• 173: Bill Bush , Doug Simon , Antero Taivalsaari, The 1999/smli_tr-99-72.ps: Implementing a Java^TMSystem for the Palm Connected Organizer, Sun Microsystems, Inc., Mountain View, CA, 1999
• 174: TALPIN, J.-P. AND JOUVELOT, P. 1992. Polymorphic type, region and effect inference. J. Functional Programming 2, 3 (July), 245-271.
• 175: Tommy Thorn, Programming languages for mobile code, ACM Computing Surveys (CSUR), v.29 n.3, p.213-239, Sept. 1997 [doi>10.1145/262009.262010]
• 176: TOZAWA,A.AND HAGIYA, M. 1999a. Careful analysis of type spoofing. In C. H. Cap, Ed., JIT '99 Java- Informations- Tage, pp. 290-296. Informatik aktuell, Springer-Verlag.
• 177: TOZAWA,A.AND HAGIYA, M. 1999b. Formalization and Analysis of Class Loading in Java. Graduate School of Science, University of Tokyo.
• 178: Joachim van den Berg , Bart Jacobs, The LOOP Compiler for Java and JML, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.299-312, April 02-06, 2001
• 179: Joachim van den Berg , Marieke Huisman , Bart Jacobs , Erik Poll, A Type-Theoretic Memory Model for Verification of Sequential Java Programs, Selected papers from the 14th International Workshop on Recent Trends in Algebraic Development Techniques, p.1-21, September 15-18, 1999
• 180: Joachim van den Berg , Bart Jacobs , Erik Poll, Formal Specification and Verification of JavaCard's Application Identifier Class, Revised Papers from the First International Workshop on Java on Smart Cards: Programming and Security, p.137-150, September 14, 2000
• 181: Dennis M. Volpano , Geoffrey Smith, Language Issues in Mobile Program Security, Mobile Agents and Security, p.25-43, January 1998
• 182: VON OHEIMB, D. 2000. Axiomatic semantics for Java light . In S. Drossopoulkou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Muller, and A. Poetzsch-Heffter, Eds., ECOOP'2000 Work-shop on Formal Techniques for Java Programs (Sophia Antipolis, France, June), pp. 88-95. Fernuniversitat Hagen.
• 183: David von Oheimb , Tobias Nipkow, Machine-Checking the Java Specification: Proving Type-Safety, Formal Syntax and Semantics of Java, p.119-156, January 1999
• 184: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• 185: WALLACE, C. 1997. The semantics of the Java programming language: Preliminary version. Tech. Rep. CSE-TR-355-97, University of Michigan EECS Department.
• 186: Dan Seth Wallach , Edward Felten, A new approach to mobile code security, 1999
• 187: WALLACH,D.S.AND FELTEN, E. W. 1998. Understanding Java stack inspection. In Symp. on Security and Privacy (Oakland, Calif., May), pp. 52-63. IEEE Computer Society Press, Los Alamitos, Calif.
• 188: Mitchell Wand , Joshua D. Guttman, Vlisp: A Verified Implementation of Scheme, Kluwer Academic Publishers, Norwell, MA, 1995
• 189: WEBB, W. 1999. Embedded Java: An uncertain future. Electrical Design News 44, 10 (May), 89-96.
• 190: WELCH, P. H. 1997. Java threads in light of Occam/ CSP. In A. Bakkers, Ed., Parallel Programming and Java, WoTUG 20 (Twente, Netherlands, Apr.), pp. 282-309. Concurrent Systems Engineering Series, IOS Press, Amsterdam.
• 191: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States
• 192: Andrew Kevin Wright, Practical soft typing, Rice University, Houston, TX, 1996
• 193: Phillip M. Yelland, A compositional account of the Java virtual machine, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.57-69, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292548]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Smartcards

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

General Terms:
Verification

Keywords:
Common criteria, programming