Prototyping Proof Carrying Code

13 years 10 months ago

Download www4.in.tum.de

Abstract We introduce a generic framework for proof carrying code, developed and mechanically veriﬁed in Isabelle/HOL. The framework deﬁnes and proves sound a veriﬁcation 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 overﬂow.

Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Seb

Real-time Traffic

Communications | Generic Framework | IFIPTCS 2004 | Proof Carrying Code | Safety Policy |

claim paper

» Research on ProofCarrying Code for UntrustedCode Security

» A Tutorial Example of the Semantic Approach to Foundational ProofCarrying Code

» A Syntactic Approach to Foundational ProofCarrying Code

» ProofCarrying Code

» A Gradual Approach to a More Trustworthy Yet Scalable ProofCarrying Code

» Tutorial Examples of the Semantic Approach to Foundational ProofCarrying Code

» ProofCarrying Code in a SessionTyped Process Calculus

» By Reason and Authority A System for Authorization of ProofCarrying Code

Post Info
More Details (n/a)

Added	02 Jul 2010
Updated	02 Jul 2010
Type	Conference
Year	2004
Where	IFIP
Authors	Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz

Comments (0)

Sciweavers

Prototyping Proof Carrying Code

Communications | Generic Framework | IFIPTCS 2004 | Proof Carrying Code | Safety Policy |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers