Assurance Cases for Proofs as Evidence

Sagar Chaki, Arie Gurfinkel, Kurt Wallnau, Charles Weinstock, Proceedings of the Workshop on Proof-Carrying Code and Software Certification (PCC'09), pages 23-28, August 15, 2009

Abstract: Proof-carrying code (PCC) provides a gold standard for establishing formal and objective confidence in program behavior. However, in order to extend the benefits of PCC -- and other formal certification techniques -- to realistic systems, we must establish the correspondence of a mathematical proof of a program's semantics and its actual behavior. In this paper, we argue that assurance cases are an effective means of establishing such a correspondence. To this end, we present an assurance case pattern for arguing that a proof is free from various proof hazards. We also instantiate this pattern for a proof-based mechanism to provide evidence about a generic medical device software.

PDF