Skip to main content
SpringerLink
Log in

A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2294))

Abstract

Many formal specifications of the JavaCard Virtual Machine are defensive, in that theyp erform type-checking at run-time. In this paper, we show how to construct from such a defensive virtual machine an offensive one that does not perform type-checking at run-time. Further, we establish that the two machines coincide for the class of JavaCard programs that pass bytecode verification. Both the construction of the offensive virtual machine and its correctness proof are achieved using (non-standard) abstract interpretation techniques and have been fully formalized in the Coq proof assistant.

Simão Melo de Sousa is partiallysu pported by the grant SFRH/BD/790/2000 from the Portuguese Fundação para a Ciência e a Technologia.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.

    Google Scholar 

  2. G. Barthe and P. Courtieu. Efficient Reasoning about Executable Specifications in Coq. Manuscript, 2002.

    Google Scholar 

  3. G. Barthe, G. Dufay, M. Huisman, and S. Melo de Sousa. Jakarta: a toolset to reason about the JavaCard platform. In I. Attali and T. Jensen, editors, Proceedings of e-SMART’01, volume 2140 of Lecture Notes in Computer Science, pages 2–18. Springer-Verlag, 2001.

    Google Scholar 

  4. G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, and S. Melo de Sousa. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP’01, volume 2028 of Lecture Notes in Computer Science, pages 302–319. Springer-Verlag, 2001.

    Google Scholar 

  5. C. Bernardeschi and N. De Francesco. Combining abstract interpretation and model checking for analysing security properties of java bytecode. In A. Cortesi, editor, Proceedings of VMCAI’02, volume 2xxx of Lecture Notes in Computer Science, 2002.

    Google Scholar 

  6. Y. Bertot. Formalizing in Coq a type system for object initialization in the Java bytecode language. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of CAV’01, volume 2102 of Lecture Notes in Computer Science, pages 14–24. Springer-Verlag, 2001.

    Google Scholar 

  7. 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 

  8. L. Casset and J.-L. Lanet. A Formal Specification of the Java Byte Code Semantics using the B Method. In B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Proceedings of Formal Techniques for Java Programs. Technical Report 251, 1999, Fernuniversität Hagen, Fernuniversität Hagen, 1999.

    Google Scholar 

  9. R. M. Cohen. Defensive Java Virtual Machine Specification Version 0.5. Manuscript, 1997.

    Google Scholar 

  10. P. Cousot. Abstract Interpretation Based Formal Methods and Future Challenges. In R. Wilhelm, editor, Informatics — 10 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 138–156. Springer-Verlag, 2001.

    Google Scholar 

  11. S. N. Freund and J. C. Mitchell. The type system for object initialization in the Java bytecode language. ACM Transactions on Programming Languages and Systems, 21(6):1196–1250, November 1999.

    Article  Google Scholar 

  12. A. Galland, D. Deville, G. Grimaud, and B. Folliot. Contrôle des ressources dans les cartes à microprocesseur. In Proceedings of LTRE’02, 2002.

    Google Scholar 

  13. P. Girard. Which securityp olicy for multiapplication smart cards? In Proceedings of Usenix workshop on Smart Card Technology (Smartcard’99), 1999.

    Google Scholar 

  14. P. Hartel and L. Moreau. Formalizing the Safety of Java, the Java Virtual Machine and Java Card. ACM Computing Surveys, 33:517–558, December 2001.

    Google Scholar 

  15. G. Klein and T. Nipkow. Verified bytecode verifiers. Theoretical Computer Science, 2002. Submitted.

    Google Scholar 

  16. Gemplus Research Labs. Java Card Common Criteria Certification Using Coq. Technical Report, 2001.

    Google Scholar 

  17. J.-L. Lanet and A. Requet. Formal Proof of Smart Card Applets Correctness. In J.-J. Quisquater and B. Schneier, editors, Proceedings of CARDIS’98, volume 1820 of Lecture Notes in Computer Science, pages 85–97. Springer-Verlag, 1998.

    Google Scholar 

  18. M. Montgomery and K. Krishna. Secure Object Sharing in Java Card. In Proceedings of Usenix workshop on Smart Card Technology, (Smartcard’99), 1999.

    Google Scholar 

  19. J. Strother Moore, R. Krug, H. Liu, and G. Porter. Formal Models of Java at the JVM Level A Surveyf rom the ACL2 Perspective. In S. Drossopoulou, editor, Proceedings of Formal Techniques for Java Programs, 2001.

    Google Scholar 

  20. T. Nipkow. Verified Bytecode Verifiers. In F. Honsell and M. Miculan, editors, Proceedings of FOSSACS’01, volume 2030 of Lecture Notes in Computer Science, pages 347–363. Springer-Verlag, 2001.

    Google Scholar 

  21. 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 

  22. Z. Qian. A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subroutines. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 271–312. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  23. A. Requet. A B Model for Ensuring Soundness of a Large Subset of the Java Card Virtual Machine. In S. Gnesi, I. Schieferdecker, and A. Rennoch, editors, Proceedings of FMICS’00, pages 29–46, 2000.

    Google Scholar 

  24. D.A. Schmidt. Binaryre lations for abstraction and refinement. Technical Report 2000-3, Department of Computing and Information Sciences, Kansas State University, 2000.

    Google Scholar 

  25. R. Stärk, J. Schmid, and E. Börger. Java and the Java Virtual Machine — Definition, Verification, Validation. Springer-Verlag, 2001.

    Google Scholar 

  26. The Coq Development Team. The Coq Proof Assistant User’s Guide. Version 7.2, January 2002.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia-Antipolis, France

    Gilles Barthe, Guillaume Dufay & Simão Melo de Sousa

  2. Université de la Méditerranée, Marseille, France

    Line Jakubiec

  3. Universidade da Beira Interior, Covilhã, Portugal

    Simão Melo de Sousa

Authors
  1. Gilles Barthe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Guillaume Dufay
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Line Jakubiec
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Simão Melo de Sousa
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Via Torino 155, 30170, Mestre-Venezia, Italy

    Agostino Cortesi

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barthe, G., Dufay, G., Jakubiec, L., de Sousa, S.M. (2002). A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-47813-2_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43631-7

  • Online ISBN: 978-3-540-47813-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation