Embedding proof-carrying components into Isabelle
Bruno Hauser · Repository for Publications and Research Data (ETH Zurich) · 2009
The execution of mobile code can produce unexpected behaviour which may compromise security and correctness of a software system.Proof-Carrying Components are a way to overcome this problem.Proof-Carrying Components carry a mathematical proof showing that the component satisfies certain properties, known as the contract of the component.A code consumer can check the mathematical proof attached to the component before executing the mobile code.In this way, the consumer can make sure in advance that the mobile code will be executed in a safe way.Proof-Carrying Components can be automatically generated using Proof-Transforming Compilers.Proof-Transforming Compilers are compilers that take a source proof with contracts as input and produce a bytecode proof and its contract as output.An important property of Proof-Transforming Compilers is that they do not have to be trusted.If a Proof-Transforming Compiler produces a wrong specification or a wrong proof for a component, the proof checker of the code consumer will reject the component.In this Master thesis, we show how a bytecode proof produced as output of a Proof-Transforming Compiler can be embedded in a theorem prover.We have embedded the Proof-Carrying Components into Isabelle, using shallow embedding for the component contracts and a deep embedding for the bytecode instructions.To show that a component satisfies its contract, the generator produces a proof script.We have optimized this proof script and the measurements show that proofs are checked at least twice as fast compared to the non-optimized proof script.The embedding has been integrated into a Proof-Transforming Compiler in EiffelStudio.