Mind the Gap: Formal Verification and the Common Criteria

Bernhard Beckert, Daniel Bruns, Sarah Grebing


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.