Mind the Gap: Formal Verification and the Common Criteria

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert, Daniel Bruns und Sarah Grebing
In:6th International Verification Workshop (VERIFY 2010)
Verleger:EasyChair
Reihe:EPiC Series
Band:3
Jahr:2012
Seiten:4-12
URL:http://easychair.org/publications/?page=1489979161

Abstract

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.

BibTeX

@InProceedings{BeckertBrunsGrebing12,
  author	= {Bernhard Beckert and Daniel Bruns and Sarah Grebing},
  title		= {Mind the Gap: Formal Verification and the {Common} {Criteria}},
  year		= 2012,
  month         = jul,
  booktitle	= {6th International Verification Workshop ({VERIFY} 2010)},
  editor	= {Markus Aderhold and Serge Autexier and Heiko Mantel},
  language	= {english},
  abstract	= {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.},
  series	= {EPiC Series},
  volume	= 3,
  pages		= {4--12},
  publisher	= {EasyChair},
  issn		= {2040-557X},
  url		= {http://easychair.org/publications/?page=1489979161}
}