Correctness of Java Card Method Lookup via Logical Relations

  • Ewen Denney
  • Thomas Jensen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


We formalise the Java Card bytecode optimisation from class file to CAP file format as a set of constraints between the two formats, and define and prove its correctness. Java Card bytecode is formalised as an abstract operational semantics, which can then be instantiated into the two formats. The optimisation is given as a logical relation such that the instantiated semantics are observably equal. The proof has been automated using the Coq theorem prover.


Virtual Machine Smart Card Operational Semantic Logical Relation Class Reference 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    P. Bertelsen. Semantics of Java byte code. Technical report, Department of Information Technology, Technical University of Denmark, March 1997.Google Scholar
  2. 2.
    Ewen Denney. Correctness of Java Card Tokenisation. Technical Report 1286, Projet Lande, IRISA, 1999. Also appears as INRIA research report 3831.Google Scholar
  3. 3.
    Jean-Louis Lanet and Antoine Requet. Formal proof of smart card applets correctness. In Third Smart Card Research and Advanced Application Conference (CARDIS’98), 1998.Google Scholar
  4. 4.
    T. Lindholm and F. Yelling. The Java Virtual Machine Specification. Addison-Wesley, 1997.Google Scholar
  5. 5.
    J. Mitchell. Foundations for Programming Languages. Foundations of Computing Series. MIT Press, 1996.Google Scholar
  6. 6.
    Peter D. Mosses. Modularity in structural operational semantics. Extended abstract, November 1998.Google Scholar
  7. 7.
    Cornelia Pusch. Verification of Compiler Correctness for the WAM. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics (TPHOLs’96), pages 347–362. Springer-Verlag, 1996.Google Scholar
  8. 8.
    Cornelia Pusch. Formalizing the Java Virtual Machine in Isabelle/HOL. Technical Report TUM-I9816, Institut für Informatik, Technische Universität München, 1998.Google Scholar
  9. 9.
    Gaëlle Segouat. Preuve en Coq d’une mise en oeuvre de Java Card. Master’s thesis, Projet Lande, IRISA, 1999.Google Scholar
  10. 10.
    Sun Microsystems. Java Card 2.0 Language Subset and Virtual Machine Specification, October 1997. Final Revision.Google Scholar
  11. 11.
    Sun Microsystems. Java Card 2.1 Virtual Machine Specification, March 1999. Final Revision 1.0.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Ewen Denney
    • 1
  • Thomas Jensen
    • 1
  1. 1.Projet LandeIRISARennes CedexFrance

Personalised recommendations