Industrial Use of Formal Methods for a High-Level Security Evaluation

This paper presents an effective use of formal methods for the development and for the security certification of smart card software. The approach is based on the Common Criteria's methodology that requires the use of formal methods to prove that a product implements the claimed security level. This work led to the world-first certification of a commercial Java Card TM product involving all formal assurances needed to reach the highest security level. For this certification, formal methods have been used for the design and the implementation of the security functions of the Java Card system embedded in the product. We describe the refinement scheme used to meet the Common Criteria's requirements on formal models and proofs. In particular, we show how to build the proof that the implementation ensures the security objectives claimed in the security specification. We also provide some lessons learned from this important application of formal methods to the smart cards industry.