Skip to main content
SpringerLink
Log in

Jakarta: A Toolset for Reasoning about JavaCard

  • Conference paper
  • First Online:
Book cover Smart Card Programming and Security (E-smart 2001)

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

Included in the following conference series:

Abstract

JavaCard [22] is a dialect of Java that enables Java technology to run on new generation smart cards and other devices with limited memory. As JavaCard is becomingincr easingly popular, there has been a strong interest, both from academics and industrials, to reason formally about the JavaCard platform.

partially supported by the Portuguese research grant sfrh/bd/790/2000.

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. S. Agerholm and J. Frost. Towards an integrated CASE and theorem proving tool for VDM-SL. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, Proceedings of FME’97, volume 1313 of Lecture Notes in Computer Science, pages 278–297. Springer-Verlag, 1997.

    Google Scholar 

  2. B. Barras, S. Boutin, C. Comes, 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 

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

  4. S. Bensalem, V. Ganesh, Y. Lakhnech, C. Muñoz, S. Owre, H. Rueß, J. Rushby, V. Rusu, H. Saïdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. In Proceedings of NASA’s Workshop on Formal Methods, 2000.

    Google Scholar 

  5. J. Bergstra and J. W. Klop. Conditional rewrite rules: confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  6. P. Bertelsen. Semantics of Java Byte Code. Master’s thesis, Department of Computer Science, Royal Veterinary and Agricultural University of Copenhagen, 1997.

    Google Scholar 

  7. 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 2xxx of Lecture Notes in Computer Science. Springer-Verlag, 2001.

    Google Scholar 

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

  9. E. Börger and W. Schulte. A Programmer Friendly Modular Definition of the Semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 353–404. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  10. P. Borras, D. Clément, Th. Despeyroux, J. Incerpi, G. Kahn, B. Lang, and V. Pascual. Centaur: the system. In Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 14–24. ACM Press, 1988.

    Google Scholar 

  11. J. P. Bowen and M. J. C. Gordon. A shallow embedding of Z in HOL. Information and Software Technology, 37(5–6):269–276, 1995.

    Article  Google Scholar 

  12. P. Cousot. Program analysis: The abstract interpretation perspective. ACM Computing Surveys, 28A(4es):165-es, December 1996.

    Google Scholar 

  13. P. Cousot. Types as abstract interpretations, invited paper. In Proceedings of POPL’97, pages 316–331. ACM Press, 1997.

    Google Scholar 

  14. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of POPL’77, pages 238–252. ACM Press, 1977.

    Google Scholar 

  15. A. van Deursen, J. Heering, and P. Klint, editors. Language Prototyping: an algebraic specification approach. AMAST Series in Computing. World Scientific, 1996.

    Google Scholar 

  16. S. Drossopoulou and S. Eisenbach. Describing the semantics of Java and Proving Type Soundness. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 41–82. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  17. M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, and H. Zheng. Tool-supported program abstraction for finite-state verification. In Proceedings of ICSE’01, 2001.

    Google Scholar 

  18. P. Hartel. LETOS-a lightweight execution tool for operational semantics. Software-practice and experience, 29:1379–1416, September 1999.

    Google Scholar 

  19. P. Hartel and L. Moreau. Formalizing the Safety of Java, the Java Virtual Machine and Java Card. ACM Computing Surveys, 2001. To appear.

    Google Scholar 

  20. P. H. Hartel, M. J. Butler, and M. Levy. The Operational Semantics of a Java Secure Processor. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 313–352. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  21. B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java classes. A CM SIGPLAN Notices, 33(10):329–340, October 1998.

    Google Scholar 

  22. JavaCard Technology. http://java.sun.com/products/javacard

  23. J. W. Klop. Term-rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, pages 1–116. Oxford Science Publications, 1992. Volume 2.

    Google Scholar 

  24. X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system, release 3.00, 2000.

    Google Scholar 

  25. P. Müller and A. Poetzsch-Heffter. A type system for checking applet isolation in Java Card. In S. Drossopoulou, editor, Formal Techniques for Java Programs, 2001. To appear.

    Google Scholar 

  26. C. Muñoz. PBS: Support for the B-method in PVS. Technical Report SRI-CSL-99-01, SRI International, February 1999.

    Google Scholar 

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

  28. T. Nipkow and D. von Oheimb. Java,/light is type-safe—definitely. In Proceedings of POPL’98, pages 161–170. ACM Press, 1998.

    Google Scholar 

  29. L. Paulson. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

    MATH  Google Scholar 

  30. M. Petersson. Compiling Natural Semantics. PhD thesis, Linköping University, 1995.

    Google Scholar 

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

  32. N. Shankar, S. Owre, and J. M. Rushby. The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International, February 1993. Supplemented with the PVS2 Quick Reference Manual, 1997. 3

    Google Scholar 

  33. R. Stata and M. Abadi. A type system for Java bytecode subroutines. ACM Transactions on Programming Languages and Systems, 21(1):90–137, January 1999.

    Google Scholar 

  34. D. Terrasse. Vers un environnement d’aide au developpement de preuves en Semantique Naturelle. PhD thesis, Ecole Nationale des Ponts et Chaussees, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia-Antipolis, France

    G. Barthe, G. Dufay & M. Huisman

  2. University of Beira Interior-Portugal, Portugal

    G. Barthe

Authors
  1. G. Barthe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. G. Dufay
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. M. Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. S. Melo de Sousa
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. INRIA Sophia Antipolis, BP 93, 06902, Sophia Antipolis Cedex, France

    Isabelle Attali

  2. Campus de Beaulieu, IRISA/CNRS, 35042, Rennes, France

    Thomas Jensen

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barthe, G., Dufay, G., Huisman, M., de Sousa, S.M. (2001). Jakarta: A Toolset for Reasoning about JavaCard. In: Attali, I., Jensen, T. (eds) Smart Card Programming and Security. E-smart 2001. Lecture Notes in Computer Science, vol 2140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45418-7_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-45418-7_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42610-3

  • Online ISBN: 978-3-540-45418-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation