Transcript PPT slides
The Design and Implementation of a Certifying Compiler [Necula, Lee] A Certifying Compiler for Java [Necula, Lee et al] David W. Hill CSCI 297 5.31.2005 How to deal with Untrusted Code? How can the host system ensure that the untrusted code will not damage it, for example, by corrupting internal data structures? How can the host ensure that the untrusted code will not use too many resources (such as CPU, memory, and so forth) or use them for too long a time period? How can the host make these assurances without undue effort and negative effect on overall system performance? Proof Carrying Code Proof-Carrying Code is a technique by which the host establishes a set of safety rules that guarantee safe behavior of programs. The code producer creates a formal safety proof that proves, for the untrusted code, adherence to the safety rules. Then, the host is able to use a simple and fast proof validator to check, with certainty, that the proof is valid and hence the foreign code is safe to execute. High Level Overview – Proof Carrying Code Code Producer Certifying Compiler Program Proof Checker Proof Security Policy Code Consumer A code producer sends a program and its safety proof to a code consumer – A certifying compiler constructs the program and proof – A proof checker checks them against a security policy PCC Process The source program is compiled to machine code annotated with loop invariants and with some other annotations. The annotated machine code is passed through the Verification Condition Generator (VCGen) that verifies the well-formedness of the code (such as that the branch targets are within the code segment) and emits a verification condition (VC). The verification condition is a predicate that is provable only if the code meets the safety policy. PCC Process The verification condition is passed to a theorem prover that finds and emits a proof of it according to the logic requested by the code consumer. The proof is verified to be valid (with respect to the given logic) and to prove the required verification condition. If the proof checking succeeds, the code meets the safety policy and can be safely installed for execution. The Cartoon Guide to PCC My program solves your problem. Code producer Great! But let me quickly look over the instructions first. Code consumer The Cartoon Guide to PCC Code producer Code consumer The Cartoon Guide to PCC This store instruction is dangerous! Code producer Code consumer The Cartoon Guide to PCC Can you prove that it is always safe? Code producer Code consumer The Cartoon Guide to PCC Yes! Here’s the proof I got from my certifying Java compiler! Code producer Can you prove that it is always safe? Code consumer The Cartoon Guide to PCC Code producer Your proof checks out. Code consumer The Cartoon Guide to PCC Code producer I believe you because I believe in logic! Code consumer Design & Implementation of an Certifying Compiler Translates programs written in a type-safe subset of C into highly optimized DEC Alpha assembly language programs. Certifier that automatically checks the type safety and memory safety of any assembly language program produced by the compiler. Certifier produced a formal proof that can be used by the code consumer to ensure safe code Overview of Certifying Compiler Code annotations assist certifier to verify type safety and memory safety Type specifications declare the type of argument and result register for every function in the code. Inside the Certifier VCGen creates a safety predicate for each function. Prover produces a formal proof of the predicate Proof checker validates the proof Certifier could be used for other properties, other than memory and type safety. Sample Code Source Code Touchstone Compiler PCC VCGen Native Code With Annotations Verification Condition Theorem Prover Safety Safety Proof Proof Code Producer Code Consumer Safety Policy VCGen Verification Condition Ok CPU Proof Checker Touchstone Compiler Source Code PCC Tampered VCGen Native Code With Annotations Verification Condition Theorem Prover Safety Policy Safety Proof Code Producer Hacker Tampered Native Code With Annotations Code Consumer Safety Proof Safety Policy VCGen Verification Condition (may change) Tampered Code is not delivered to the CPU Proof Checker No But safety is still guaranteed if the code is modified in such a way that the VC is unchanged CPU Sample Proof First rule states that it is safe to read an element of an array if its index is within the array boundaries Second rule states that the result of the read operation has the type of the array elements Proves that assembly language program is safe (memory) Benchmarks Certifying Compiler for Java 2nd paper Optimized compiler Special J that compiles java bytecodes into target code for x86 architecture Implement a certifier for a large subset of the Java language PCC binaries are of reasonable size and can be checked rapidly by a small proof checker PCC & Certifying compilers are scalable Architecture Java binary Certifying compiler Native code VCGen Annotations VCGen Axioms VC Axioms VC Proof generator Code producer Proof Proof checker Code Consumer VC Generation - Detailed Checks code that could violate safety policy and produces proof obligations movl 4(%eax), %ebx Assembly Inst. Saferd4 (add eax 4) proof obligation VC Generation - Loops When VCGen finds annotation below: ANN_LOOP (INV=P, MODREG=R) VC Generation PCC Architecture Details Host only needs VC Generator and Proof Checker – Small TCB VC GEN = 23K lines (C) Proof Checker = 1.4K lines (C) Benchmarks Online Demo George Necula’s Touchstone Demo http://raw.cs.berkeley.edu/Ginseng/Images/p ccdemo.html PCC Advantages Great for mobile code, consumer only has to run a small proof checking process. Burden shifted to producer. No cryptography of third party checks required Code is verified before execution, therefore don’t have to kill processes after acquisition of resources Issues for Discussion Writing good policies is the hard part – Better ways to define policies – Ways to reason about properties of policies – Ideas for the right policies for different scenarios – Ways to develop, reason about, and test distributed policies References -George Necula’s Web Page http://raw.cs.berkeley.edu/papers.html#annotated -Peter Lee’s Web Page http://www-2.cs.cmu.edu/~petel/ -Flexibility and Trustworthiness in Proof-Carrying Code, Andrew Bernard, CMU -Lecture 19. UVA, Proof Carrying Code, David Evans -Some open issues for certifying compilers, Greg Morrisett -Code Carrying Proofs, Aytekin Vargun, Rensselaer Polytechnic Institute Thank You! Discussion…..