Formal Verification of a JavaCard Virtual Machine with Frama-C

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.