Iman Narasamdya, Michael Perin
Certification of Smart-Card Applications in Common Criteria (2008)
Certification of Smart-Card Applications in Common Criteria (2008)
TR-2008-14.pdf
Keywords: Software Certification, Common Criteria, Program Invariants, Inter-Program Properties
Abstract: This report describes a certification method of smart-card applications in the framework of Common Criteria. In this framework, a smart-card application is represented consecutively 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. We describe in this report the application of a theory of program properties 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 verification condition as a notion of certificate. The theory is applicable to the certification process because all representations of a smart-card application are essentially programs and the representation correspondences are properties relating two programs.
