Advertisement

A Formal Executable Semantics of the JavaCard Platform

  • Gilles Barthe
  • Guillaume Dufay
  • Line Jakubiec
  • Bernard Serpette
  • Simão Melo de Sousa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)

Abstract

We present a formal executable specification of two crucial JavaCard platform components, namely the Java Card Virtual Machine (JCVM) and the ByteCode Verifier (BCV). Moreover, we relate both components by giving a proof of correctness of the ByteCode Verifier. Both formalisations and proofs have been machined-checked using the proof assistant Coq.

Keywords

Virtual Machine Smart Card Java Program Program Counter Proof Assistant 
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.

References

  1. 1.
    W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, and P. H. Schmitt. The Key approach: integrating design and formal verification of Java Card programs. In Proceedings of the Java Card Workshop, co-located with the Java Card Forum, Cannes, France, 2000.Google Scholar
  2. 2.
  3. 3.
  4. 4.
    B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, H. Laulhère, P. Loiseleur, C. Muñoz, C. Murthy, C. Parent-Vigouroux, C. Paulin-Mohring, A. Saïbi, and B. Werner. The Coq Proof Assistant User’s Guide. Version 6.3.1, December 1999.Google Scholar
  5. 5.
    Y. Bertot. Formalizing in Coq a type system for object initialization in the Java bytecode language. Manuscript, 2000.Google Scholar
  6. 6.
    P. Bieber, J. Cazin, V. Wiels, G. Zanon, P. Girard, and J.-L. Lanet. Electronic purse applet certification: extended abstract. In S. Schneider and P. Ryan, editors, Proceedings of the workshop on secure architectures and information flow, volume 32 of Electronic Notes in Theoretical Computer Science. Elsevier Publishing, 2000.Google Scholar
  7. 7.
    P. Brisset. A Case Study In Java Software Verification: SecurityManager.checkConnect(). In S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs. Technical Report 269, 5/2000, Fernuniversität Hagen, Fernuniversität Hagen, 2000.Google Scholar
  8. 8.
    CLDC and the K Virtual Machine (KVM). http://java.sun.com/products/cldc
  9. 9.
    A. Coglio, A. Goldberg, and Z. Qian. Towards a Provably-Correct Implementation of the JVM Bytecode Verifier. In Formal Underpinnings of Java Workshop at OOPSLA, 1998.Google Scholar
  10. 10.
    R. M. Cohen. Defensive Java Virtual Machine Specification Version 0.5. Manuscript, 1997.Google Scholar
  11. 11.
    M. Dam and P. Giambiagi. Confidentiality for mobile code: The case of a simple payment protocol. In Proceedings of CSFW’00. IEEE Press, 2000.Google Scholar
  12. 12.
    S. N. Freund. The Costs and Benefits of Java Bytecode Subroutines. In Formal Underpinnings of Java Workshop at OOPSLA, 1998.Google Scholar
  13. 13.
    S. N. Freund and J. C. Mitchell. A type system for object initialization in the Java bytecode language. In Proceedings of OOPSLA’ 98, volume 33(10) of ACM SIGPLAN Notices, pages 310–328. ACM Press, October 1998.CrossRefGoogle Scholar
  14. 14.
    R. Goré and L. Nguyen. CardKt: Automated Logical Deduction on Java Cards. In Proceedings of the Java Card Workshop, co-located with the Java Card Forum, Cannes, France, 2000.Google Scholar
  15. 15.
    K. Havelund. Java PathFinder―A Translator from Java to Promela. In D. Dams, R. Gerth, S. Leue, and M. Massink, editors, Proceedings of 5th and 6th International SPIN Workshops, volume 1680 of Lecture Notes in Computer Science, page 152. Springer-Verlag, 1999.Google Scholar
  16. 16.
  17. 17.
  18. 18.
    T. Jensen, D. Le Métayer, and T. Thorn. Verification of control flow based security policies. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 89–103. IEEE Computer Society Press, 1999.Google Scholar
  19. 19.
    G. Klein and T. Nipkow. Lightweight bytecode verification. In S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs. Technical Report 269, 5/2000, Fernuniversität Hagen, Fernuniversität Hagen, 2000.Google Scholar
  20. 20.
    J.-L. Lanet and A. Requet. Formal Proof of Smart Card Applets Correctness. In Proceedings of CARDIS’98, 1998.Google Scholar
  21. 21.
    K. R. M. Leino, J. B. Saxe, and R. Stata. Checking Java programs via guarded commands. In B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs. Technical Report 251, 1999, Fernuniversität Hagen, Fernuniversität Hagen, 1999.Google Scholar
  22. 22.
  23. 23.
    J. Meyer and A. Poetzsch-Heffter. An architecture for interactive program provers. In S. Graf and M. Schwartzbach, editors, Proceedings of TACAS’2000, volume 1785 of Lecture Notes in Computer Science, pages 63–77. Springer-Verlag, 2000.Google Scholar
  24. 24.
    T. Nipkow. Verified Bytecode Verifiers. In F. Honsell, editor, Proceedings of FOS-SACS’01, volume xxxx of Lecture Notes in Computer Science. Springer-Verlag, 2001. To appear.Google Scholar
  25. 25.
    T. Nipkow and D. von Oheimb. Javalight is type-safe―definitely. In Proceedings of POPL’98, pages 161–170. ACM Press, 1998.Google Scholar
  26. 26.
    A. Poetzsch-Heffter and P. Müller. A Programming Logic for Sequential Java. In D. Swiestra, editor, Proceedings of ESOP’99, volume 1576 of Lecture Notes in Computer Science, pages 162–176. Springer-Verlag, 1999.Google Scholar
  27. 27.
    C. Pusch. Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL. In W. R. Cleaveland, editor, Proceedings of TACAS’99, volume 1579 of Lecture Notes in Computer Science, pages 89–103. Springer-Verlag, 1999.Google Scholar
  28. 28.
    F. B. Schneider. Enforceable security policies. Technical Report TR99-1759, Cornell University, October 1999.Google Scholar
  29. 29.
    G. Ségouat. Preuve en Coq d’une mise en oeuvre de Java Card. Master’s thesis, University of Rennes 1, 1999.Google Scholar
  30. 30.
    R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proceedings of POPL’98, pages 149–160. ACM Press, 1998.Google Scholar
  31. 31.
    D. Syme. Proving Java type soundness. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 83–118. Springer-Verlag, 1999.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Gilles Barthe
    • 1
  • Guillaume Dufay
    • 1
  • Line Jakubiec
    • 1
    • 2
  • Bernard Serpette
    • 1
  • Simão Melo de Sousa
    • 1
    • 3
  1. 1.INRIASophia-AntipolisFrance
  2. 2.Université de ProvenceMarseilleFrance
  3. 3.Universidade da Beira InteriorCovilhãPortugal

Personalised recommendations