Abstract
Security of modern software has become a major concern. One example of highly critical software is smart card software since smart cards often play a key role in user authentication and controlling access to sensitive services and data. To demonstrate the compliance of a smart card product to security requirements, its certification according to the Common Criteria is often recommended or even required. The highest, most rigorous levels of Common Criteria certification include formal verification. In this chapter, we show how an industrial smart card product—a JavaCard Virtual Machine—has been formally verified by Thales using Frama-C, a software verification platform for C code. We describe the main steps of this verification project, illustrate target security properties, present some lessons learned and discuss several directions for future work and necessary tool enhancements.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
EAL6 and EAL7 certificates are available, resp., at https://cyber.gouv.fr/sites/default/files/2021/11/certificat-anssi-cc-2021_42.pdf and https://cyber.gouv.fr/sites/default/files/document_type/Certificat-CC-2023_45fr_0.pdf.
- 2.
- 3.
The selection mechanism allows to deliver commands from the operating system to an applet [23].
- 4.
For convenience of the readers, the full example is available in the companion repository at https://git.frama-c.com/pub/frama-c-book-companion/-/tree/main/proof-of-security.
- 5.
This scope restriction implies that the selected application cannot be changed.
- 6.
Unless there is a critical exception and the JCVM execution is aborted.
- 7.
Except for a few specific cases such as critical errors that abort the VM execution, which are not detailed here.
- 8.
In the real-life code, this simplification is not made, therefore additional stack-related properties (such as the absence of overflows in method frames and system blocks) are verified to exclude the corresponding security vulnerabilities.
References
Common criteria for information technology security evaluation. Part 3: security assurance components (2017). Technical report, CCMB-2017-04-003. https://www.commoncriteriaportal.org/files/ccfiles/CCPART3V3.1R5.pdf
Andronick J, Chetali B, Paulin-Mohring C (2005) Formal verification of security properties of smart card embedded source code. In: International symposium of formal methods (FM 2005), LNCS, vol 3582, pp 302–317. Springer. https://doi.org/10.1007/11526841_21
Barthe G, Dufay G, Jakubiec L, Serpette BP, de Sousa SM (2001) A formal executable semantics of the JavaCard platform. In: 10th European symposium on programming on programming languages and systems, (ESOP 2001), held as part of the joint European conferences on theory and practice of software (ETAPS 2001), LNCS, vol 2028. Springer, pp 302–319. https://doi.org/10.1007/3-540-45309-1_20
Baudin P, Bobot F, Correnson L, Dargaye Z, Blanchard A (2020) WP plug-in manual. https://frama-c.com/download/frama-c-wp-manual.pdf
Baudin P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V, ACSL: ANSI/ISO C specification language. http://frama-c.com/acsl.html
Blanchard A, Kosmatov N, Loulergue F (2019) Logic against ghosts: comparison of two proof approaches for a list module. In: Proceedings of the 34th annual ACM/SIGAPP symposium on applied computing, software verification and testing track (SAC-SVT 2019). ACM, pp 2186–2195. ACM Best Software Development paper award. https://doi.org/10.1145/3297280.3297495
Brahmi A, Carolus MJ, Delmas D, Essoussi MH, Lacabanne P, Lamiel VM, Randimbivololona F, Souyris J (2020) Industrial use of a safe and efficient formal method based software engineering process in avionics. In: Embedded real time software and systems (ERTS 2020)
Carvalho N, da Silva Sousa C, Sousa Pinto J, Tomb A (2014) Formal verification of kLIBC with the WP frama-C plug-in. In: NASA formal methods (NFM 2014), LNCS, vol 8430. Springer, pp 343–358. https://doi.org/10.1007/978-3-319-06200-6_29
Djoudi A, Hána M, Kosmatov N (2021) Formal verification of a JavaCard virtual machine with Frama-C. In: Proceedings of the 24th international symposium on formal methods (FM 2021), LNCS, vol 13047. Springer, pp 427–444. https://doi.org/10.1007/978-3-030-90870-6_23. Long version available at https://nikolai-kosmatov.eu/publications/djoudi_hk_fm_2021.pdf
Djoudi A, Hána M, Kosmatov N, Kr̆íz̆enecký M, Ohayon F, Mouy P, Fontaine A, Féliot D (2022) A bottom-up formal verification approach for common criteria certification: application to JavaCard virtual machine. In: Proceedings of the 11th European congress on embedded real-time systems (ERTS 2022)
Dordowsky F (2015) 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. https://doi.org/10.4204/EPTCS.187.3
Ebalard A, Mouy P, Benadjila R (2016) Journey to a RTE-free X.509 parser. In: Symposium sur la sécurité des technologies de l’information et des communications (SSTIC 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
Éluard M, Jensen T, Denne E (2001) An operational semantics of the Java Card firewall. In: Smart card programming and security. Springer, pp 95–110. https://doi.org/10.1007/3-540-45418-7_9
Hähnle R, Huisman M (2019) Deductive software verification: from pen-and-paper proofs to industrial tools, LNCS, vol 10000. Springer, pp 345–373. https://doi.org/10.1007/978-3-319-91908-9_18
Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2015) Frama-C: a software analysis perspective. Formal Aspects Comput. https://doi.org/10.1007/s00165-014-0326-7
Mangano F, Duquennoy S, Kosmatov N (2016) Formal verification of a memory allocation module of Contiki with Frama-C: a case study. In: Proceedings of the 11th international conference on risks and security of internet and systems (CRiSIS 2016), LNCS, vol 10158. Springer, pp 114–120. https://doi.org/10.1007/978-3-319-54876-0_9
Marché C, Paulin-Mohring C, Urbain X (2004) The KRAKATOA tool for certification of Java/JavaCard programs annotated in JML. J Logic Algeb Program 58(1–2):89–106. https://doi.org/10.1016/j.jlap.2003.07.006
Mostowski W (2007) 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. http://ceur-ws.org/Vol-259/paper12.pdf
Nguyen QH, Chetali B (2006) Certifying native java API by formal refinement. In: 7th IFIP WG 8.8/11.2 international conference on smart card research and advanced applications (CARDIS 2006), LNCS, vol 3928. Springer, pp 313–328. https://doi.org/10.1007/11733447_23
Oortwijn W, Huisman M (2019) Formal verification of an industrial safety-critical traffic tunnel control system. In: 15th international conference on integrated formal methods (IFM 2019), LNCS, vol 11918. Springer, pp 418–436. https://doi.org/10.1007/978-3-030-34968-4_23
Oracle (2002) Java card 2.2 off-card verifier, whitepaper. Technical report, Oracle. https://www.oracle.com/technetwork/java/embedded/javacard/documentation/offcardverifierwp-150021.pdf
Oracle (2020) Java Card system—open configuration protection profile, version 3.1. Technical report, Oracle. https://www.bsi.bund.de/SharedDocs/Downloads/DE/BSI/Zertifizierung/Reporte/ReportePP/pp0099V2b_pdf.pdf;jsessionid=6C3F5A7FB5FA0D928A1C310C1C0EF1CE.internet462?__blob=publicationFile &v=1
Oracle (2021) Java Card platform: runtime environment specification, classic edition, version 3.1. Technical report, Oracle, Oracle. https://docs.oracle.com/javacard/3.1/related-docs/JCCRE/JCCRE.pdf
Oracle (2021) Java Card platform: virtual machine specification, classic edition, version 3.1. Technical report, Oracle, Oracle. https://docs.oracle.com/javacard/3.1/related-docs/JCVMS/JCVMS.pdf
Robles V, Kosmatov N, Prevosto V, Rilling L, Le Gall P (2019) Tame your annotations with MetAcsl: specifying, testing and proving high-level properties. In: International conferences on tests and proofs (TAP), LNCS, vol 11823. Springer, pp 167–185. https://doi.org/10.1007/978-3-030-31157-5_11
Robles V, Kosmatov N, Prevosto V, Rilling L, Le Gall P (2021) Methodology for specification and verification of high-level properties with MetAcsl. In: Proceedings of the 9th IEEE/ACM international conference on formal methods in software engineering (FormaliSE 2021), pp 54–67. IEEE. https://doi.org/10.1109/FormaliSE52586.2021.00012
Siveroni IA (2004) Operational semantics of the Java Card Virtual Machine. J Logic Algeb Program 58(1–2):3–25. https://doi.org/10.1016/j.jlap.2003.07.003
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Djoudi, A., Hána, M., Kosmatov, N. (2024). Proof of Security Properties: Application to JavaCard Virtual Machine. In: Kosmatov, N., Prevosto, V., Signoles, J. (eds) Guide to Software Verification with Frama-C. Computer Science Foundations and Applied Logic. Springer, Cham. https://doi.org/10.1007/978-3-031-55608-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-031-55608-1_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-55607-4
Online ISBN: 978-3-031-55608-1
eBook Packages: Computer ScienceComputer Science (R0)