Proof of Security Properties: Application to JavaCard Virtual Machine

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.