Prototyping Proof Carrying Code

Abstract We introduce a generic framework for proof carrying code, developed and mechanically verified in Isabelle/HOL. The framework defines and proves sound a verification condition generator with minimal assumptions on the underlying programming language, safety policy, and safety logic. We demonstrate its usability for prototyping proof carrying code systems by instantiating it to a simple assembly language with procedures and a safety policy for arithmetic overflow.

• Type: Conference
• Year: 2004
• Where: IFIP
• Authors: Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz
• Keywords: Communications, Generic Framework, IFIPTCS 2004, Proof Carrying Code, Safety Policy