Mind the Gap: Formal Verification and the Common Criteria. (Discussion paper)

It is a common belief that the rise of standardized software certification schemes like the Common Criteria (CC) would give a boost to formal verification, and that software certification may be a killer application for program verification. However, while formal models are indeed used throughout high-assurance certification, verification of the actual implementation is not required by the CC and largely neglected in certification practice -- despite the great advances in program verification over the last decade. In this paper we discuss the gap between program verification and CC software certification, and we point out possible uses of code-level program verification in the CC certification process.