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 Isabelle/HOL in form of a shallow embedding. 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: Isabelle/HOL shallow embedding
[empty] [empty]
[empty]
TermCodegen.thy [pdf] Extensions for Isabelle's ML program generator.
TupleOrd.thy [pdf] Lexical ordering of pairs.
SALSyntax.thy [pdf] Simple Assembly Language (SAL) instructions and datatypes.
SALSemantics.thy [pdf] A formal semantics for SAL programs.
SALSafetyLogic.thy [pdf] HOL predicates as annotations (shallow embedding), logical operators for the safety logic
SALOverflowPlatform.thy [pdf] Instantiates the VCG and a safety policy that prohibits arithmetic overflows and type errors.
SALOverflowFWInst.thy [pdf] Shows that this instantiation satisfies all requirements of the PCC Framework.


Examples

EX_DoubleAddition.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_SmartCardPurse_fa.thy [pdf] Same example as above, except that we use more annotations here.
EX_RecMult.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 12 19:48:22 MET 2004