An Operational Semantics of the Java Card Firewall

1. Java Card 2.1.1. http://java.sun.com/products/javacard/javacard21.html.

2. The bali project, Last visited 2001. http://www4.informatik.tu-muenchen.de/~isabelle/bali/.

3. The loop project, Last visited 2001. http://www.cs.kun.nl/~bart/LOOP/.

4. Jim Alves-Foss, editor. Formal syntax and semantics of Java, volume 1523 of Lecture Notes in Computer Science. Springer-Verlag, 1999. 404 pages.

   Google Scholar 

5. Peter Bertelsen. Semantics of Java Byte Code. Technical report, Dep. of Information Technology, Technical University of Denmark, March 1997. Home page http://www.dina.kvl.dk/~pmb/.

6. Peter Bertelsen. Dynamic semantics of Java bytecode. In Workshop on Principles on Abstract Machines, September 1998. Home page http://www.dina.kvl.dk/~pmb/.

7. Pierre Bieber, Jacques Cazin, Abdellah El Marouani, Pierre Girard, Jean-Louis Lanet, Virginie Wiels, and Guy Zanon. The PACAP prototype: a tool for detecting Java Card illegal flow. In Isabelle Attali and Thomas Jensen, editors, Java Card Workshop (JCW), volume 2041 of Lecture Notes in Computer Science, September 2000.

   Google Scholar 

8. Zhiqun Chen. Java Card Technology for Smart Cards: Architecture and Programmer’s Guide. Addison Wesley, 2000.

   Google Scholar 

9. Ewen Denney and Thomas Jensen. Correctness of Java Card method lookup via logical relations. In 9th European Symp. on Programming (ESOP), pages 104–118. Springer-Verlag, March 2000.

   Google Scholar 

10. Stephen N. Freund and John C. Mitchell. A formal framework for the Java bytecode language and verifier. Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 34(10):147–166, November 1999.

    Google Scholar 

11. James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language Specification, Second Edition. Addison Wesley, 2000. 896 pages, http://java.sun.com/docs/books/jls/index.html.

12. Sun Microsystems. Java Card 2.1.1 runtime environment (JCRE) specification, May 2000. Revision 1.0, 61 pages.

    Google Scholar 

13. Stéphanie Motré. Modélisation et implémentation formelle de la politique de sécurité dynamique de la Java Card. In Approches Formelles dans l’Assistance au Développement de Logiciel (AFADL), pages 158–172. LSR/IMAG, January 2000.

    Google Scholar 

14. Erik Poll, Joachim van den Berg, and Bart Jacobs. Specification of the JavaCard API in JML. In J. Domingo-Ferrer, D. Chan, and A. Watson, editors, 4th Smart Card Research and Advanced Application Conf. (CARDIS), pages 135–154. Kluwer Acad. Publ., 2000.

    Google Scholar 

15. Erik Poll, Joachim van den Berg, and Bart Jacobs. Formal specification of the JavaCard API in JML: the APDU class. Computer Networks Magazine, 2001.

    Google Scholar 

16. Cornelia Pusch. Formalizing the Java Virtual Machine in Isabelle/HOL. Technical Report TUM-I9816, Institut für informatik, Technische Universtät München, 1998.

    Google Scholar 

17. Soot: a Java optimization framework. http://www.sable.mcgill.ca/soot/.

18. David von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency: Practice and Experience, 2001.

    Google Scholar 

19. David von Oheimb and Tobias Nipkow. Machine-checking the Java specification: Proving type-safety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 119–156. Springer-Verlag, 1999.

    Chapter  Google Scholar 

Download references