Technische Universität München, Department of Computer Science, Chair IV: Software & Systems Engineering, Theorem Proving Group, VeryPCC Project

[empty]

PCC Instantiation - Overflow & Type safety for SAL


[empty] In these theories we instantiate our Proof Carrying Code Framework to a simple assembly language (SAL) with a safety policy that prohibits arithmetic overflows and type errors. As safety logic we use a variant of first order arithmetics in form of a deep embedding. Safety Proofs can be conducted in Isabelle using the Isabelle/HOL inference rules. From the framework we get a verified, executable VCG, which we use to certify the safety of various SAL programs. The safety proofs can be checked using Isabelle/HOL's proof checker. [empty]

[empty]
Machine Code: SAL
Safety Policy: No overflows, No type errors
Safety Logic: FOA (deep embedding)
[empty] [empty]
[empty]
SALSyntax.thy [pdf] Simple Assembly Language (SAL) instructions and datatypes.
FiniteMap.thy [pdf] Finite Maps are use for substitution functions.
DeepLogic.thy [pdf] Syntax (dataype form) and manipulation of formulae (substitution functions).
SALSemantics_deep.thy [pdf] The meaning of SAL programs in form of a small step semantics.
SALSafetyLogic_deep.thy [pdf] Instantiates the safety logic (connectives, judgements), the safety policy (safeF), and VCG parameter functions (succsF, wpF).
SALOverflowPlatform.thy [pdf] Instantiates the VCG and a wellformedness checker for SAL programs.
SALOverflowFWInst.thy [pdf] Shows that all instantiations satisfy the requirements of the PCC Framework. Establishes the VCG Soundness theorem for this platform.
VCOpt.thy [pdf] Defines and verifies an optimizer for verification conditions.


Examples

EX_DoubleAddition_deep.thy [pdf] Very primitive example: Computes 4 times X using two additions.
EX_SmartCardPurse.thy [pdf] A check procedure protects the balance of a smart card purse from overflows.
EX_RecMult_deep.thy [pdf] Multiplies two numbers with a recursive procedure; uses pointers to simulate a call stack in memory.
[empty]
Martin Wildmoser Last modified: Mon Jan 19 18:52:40 MET 2004