[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Formal Verification of a JavaCard Virtual Machine with Frama-C

  • Conference paper
  • First Online:
Formal Methods (FM 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 13047))

Included in the following conference series:

Abstract

Formal verification of real-life industrial software remains a challenging task. It provides strong guarantees of correctness, which are particularly important for security-critical products, such as smart cards. Security of a smart card strongly relies on the requirement that the underlying JavaCard virtual machine ensures necessary isolation properties. This case study paper presents a recent formal verification of a JavaCard Virtual Machine implementation performed by Thales using the Frama-C verification toolset. This is the first verification project for such a large-scale industrial smart card product where deductive verification is applied on the real-life C code. The target properties include common security properties such as integrity and confidentiality. The implementation contains over 7,000 lines of C code. After a formal specification in the ACSL specification language, over 52,000 verification conditions were generated and successfully proved. We present several issues identified during the project, illustrate them by representative examples and present solutions we used to solve them. Finally, we describe proof results, some lessons learned and desired tool improvements.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.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

Similar content being viewed by others

Notes

  1. 1.

    It was recently added in the 23.0beta and 23.0 releases of Frama-C; it should be removed if an earlier release is used.

References

  1. Andronick, J., Chetali, B., Paulin-Mohring, C.: Formal verification of security properties of smart card embedded source code. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 302–317. Springer, Heidelberg (2005). https://doi.org/10.1007/11526841_21

    Chapter  MATH  Google Scholar 

  2. Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., de Sousa, S.M.: A formal executable semantics of the JavaCard platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 302–319. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45309-1_20

    Chapter  Google Scholar 

  3. Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blanchard, A.: WP Plug-in Manual (2020). https://frama-c.com/download/frama-c-wp-manual.pdf

  4. Baudin, P., et al.: ACSL: ANSI/ISO C Specification Language, v1.16 (2020). http://frama-c.cea.fr/acsl.html

  5. Brahmi, A., et al.: Industrial use of a safe and efficient formal method based software engineering process in avionics. In: Embedded Real Time Software and Systems (ERTS 2020) (2020)

    Google Scholar 

  6. Carvalho, N., da Silva Sousa, C., Pinto, J.S., Tomb, A.: Formal verification of kLIBC with the WP Frama-C plug-in. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 343–358. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_29

    Chapter  Google Scholar 

  7. Conchon, S., et al.: The Alt-Ergo automated theorem prover. http://alt-ergo.lri.fr

  8. Correnson, L.: Qed. Computing what remains to be proved. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 215–229. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_17

    Chapter  Google Scholar 

  9. Dordowsky, F.: An experimental study using ACSL and Frama-C to formulate and verify low-level requirements from a DO-178C compliant avionics project. Electron. Proc. Theor. Comput. Sci. 187, 28–41 (2015). https://doi.org/10.4204/EPTCS.187.3

    Article  Google Scholar 

  10. Ebalard, A., Mouy, P., Benadjila, R.: Journey to a RTE-free X.509 parser. In: Symposium sur la sécurité des technologies de l’information et des communications (SSTIC 2019) (2019). https://www.sstic.org/media/SSTIC2019/SSTIC-actes/journey-to-a-rte-free-x509-parser/SSTIC2019-Article-journey-to-a-rte-free-x509-parser-ebalard_mouy_benadjila_3cUxSCv.pdf

  11. Éluard, M., Jensen, T., Denne, E.: An operational semantics of the Java Card Firewall. In: Attali, I., Jensen, T. (eds.) E-smart 2001. LNCS, vol. 2140, pp. 95–110. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45418-7_9

    Chapter  MATH  Google Scholar 

  12. Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8

    Chapter  Google Scholar 

  13. Hähnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345–373. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-91908-9_18

    Chapter  Google Scholar 

  14. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015). https://doi.org/10.1007/s00165-014-0326-7

    Article  MathSciNet  Google Scholar 

  15. Marché, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of Java/JavaCard programs annotated in JML. J. Logic Algebraic Program. 58(1–2), 89–106 (2004). https://doi.org/10.1016/j.jlap.2003.07.006

    Article  MATH  Google Scholar 

  16. Mostowski, W.: Fully verified Java Card API reference implementation. In: 4th International Verification Workshop in connection with CADE-21. CEUR Workshop Proceedings, vol. 259. CEUR-WS.org (2007). http://ceur-ws.org/Vol-259/paper12.pdf

  17. Nguyen, Q.-H., Chetali, B.: Certifying native Java Card API by formal refinement. In: Domingo-Ferrer, J., Posegga, J., Schreckling, D. (eds.) CARDIS 2006. LNCS, vol. 3928, pp. 313–328. Springer, Heidelberg (2006). https://doi.org/10.1007/11733447_23

    Chapter  Google Scholar 

  18. Oortwijn, W., Huisman, M.: Formal verification of an industrial safety-critical traffic tunnel control system. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) IFM 2019. LNCS, vol. 11918, pp. 418–436. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-34968-4_23

    Chapter  Google Scholar 

  19. Oracle: Java Card 2.2 Off-Card Verifier, Whitepaper. Technical report, Oracle (2002)

    Google Scholar 

  20. Oracle: Java Card System - Open Configuration Protection Profile, Version 3.1. Technical report, Oracle (2020). https://www.bsi.bund.de/SharedDocs/Downloads/DE/BSI/Zertifizierung/Reporte/ReportePP/pp0099V2b_pdf.pdf;jsessionid=6C3F5A7FB5FA0D928A1C310C1C0EF1CE.internet462?__blob=publicationFile&v=1

  21. Oracle: Java Card Platform: Runtime Environment Specification, Classic Edition, Version 3.1. Technical report, Oracle, February 2021. https://docs.oracle.com/javacard/3.1/related-docs/JCCRE/JCCRE.pdf

  22. Oracle: Java Card Platform: Virtual Machine Specification, Classic Edition, Version 3.1. Technical report, Oracle, February 2021. https://docs.oracle.com/javacard/3.1/related-docs/JCVMS/JCVMS.pdf

  23. Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le Gall, P.: MetAcsl: specification and verification of high-level properties. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 358–364. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_22

    Chapter  Google Scholar 

  24. Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le Gall, P.: Tame your annotations with MetAcsl: specifying, testing and proving high-level properties. In: Beyer, D., Keller, C. (eds.) TAP 2019. LNCS, vol. 11823, pp. 167–185. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31157-5_11

    Chapter  Google Scholar 

  25. Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le Gall, P.: Methodology for specification and verification of high-level properties with MetAcsl. In: 9th IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE 2021), pp. 54–67. IEEE (2021). https://doi.org/10.1109/FormaliSE52586.2021

  26. Siveroni, I.A.: Operational semantics of the Java Card Virtual Machine. J. Logic Algebraic Program. 58(1–2), 3–25 (2004). https://doi.org/10.1016/j.jlap.2003.07.003

Download references

Acknowledgement

The authors thank the Frama-C team members for their reliable and efficient support. Many thanks to the anonymous reviewers for their helpful comments.

Author information

Authors and Affiliations

  1. Thales Digital Identity and Security, Meudon, France

    Adel Djoudi

  2. Thales Digital Identity and Security, Prague, Czech Republic

    Martin Hána

  3. Thales Research and Technology, Palaiseau, France

    Nikolai Kosmatov

Authors
  1. Adel Djoudi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Hána
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nikolai Kosmatov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nikolai Kosmatov .

Editor information

Editors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Marieke Huisman

  2. NASA Ames Research Center, Moffett Field, CA, USA

    Corina Păsăreanu

  3. Institute of Software, Chinese Academy of Sciences, Beijing, China

    Naijun Zhan

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Djoudi, A., Hána, M., Kosmatov, N. (2021). Formal Verification of a JavaCard Virtual Machine with Frama-C. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science(), vol 13047. Springer, Cham. https://doi.org/10.1007/978-3-030-90870-6_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-90870-6_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-90869-0

  • Online ISBN: 978-3-030-90870-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation