Certification of smart-card applications in common criteria

ABSTRACT

This paper describes the certification of smart-card applications in the framework of Common Criteria. In this framework, a smart-card application is represented by a model of its specification, a functional specification describing an input-output relationship, a low-level design, and implementation code. The certification process consists of the following tasks: (1) prove that the model, the functional specification, the low-level design, and the code satisfy security properties in the smart-card application's specification, and (2) prove that there is a representation correspondence between each two consecutive representations. For each task, a certificate or a collection of certificates are needed to certify the accomplishment of the task. All representations of a smart-card application are essentially programs and the representation correspondences are properties relating two programs. We show that a theory of program properties can be applied to the certification process. The theory provides foundations for describing and proving properties of a single program and properties relating two programs. The theory provides a notion of certificate that is essential to the certification process.

REFERENCES

• 1: Common Criteria for Information Technology Security Evaluation, 2007. Version 3.1, CCMB-2007-09-003.
• 2: C.-B. Breunesse , N. Cataño , M. Huisman , B. Jacobs, Formal methods for smart cards: an experience report, Science of Computer Programming, v.55 n.1-3, p.53-80, March 2005 [doi>10.1016/j.scico.2004.05.011]
• 3: Robert W. Floyd. Assigning meaning to programs. In J. T. Schwartz, editor, Proceedings of Symposium in Applied Mathematics, pages 19--32, 1967.
• 4: Constance L. Heitmeyer , Myla Archer , Elizabeth I. Leonard , John McLean, Formal specification and verification of data separation in a separation kernel for an embedded system, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180405.1180448]
• 5: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 6: E.-M.G.M. Hubbers and E. Poll. Reasoning about card tears and transactions in Java Card. In M. Wermelinger and T. Margaria-Steffen, editors, Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, volume 2984 of LNCS, pages 114--128. Springer-Verlag, 2004.
• 7: E.-M.G.M. Hubbers and E. Poll. Transactions and non-atomic API methods in Java Card: specification ambiguity and strange implementation behaviors. Technical Report NIII R0438, University of Nijmegen, Toernooiveld, 6525 ED Nijmegen, The Netherlands, October 2004.
• 8: Iman Narasamdya and Michaël Périn. Certification of smart-card applications in common criteria. Technical Report TR-2008-14, Verimag, September 2008.
• 9: Sun Micro systems, Inc, Palo Alto, California. Java Card 3.0 Platform Specification, 2008. http://java.sun.com/javacard/3.0/.
• 10: Andrei Voronkov and Iman Narasamdya. Proving inter-program properties. Technical Report TR-2008-13, Verimag, September 2008.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Keywords:
assertion functions, assertions, common criteria certification, invariants, smart-card applications, specification techniques