Transcript PPT slides
Proof-Carrying Code & Proof-Carrying Authentication Stuart Pickard CSCI 297 June 2, 2005 Papers Proof-Carrying Code George C. Necula. POPL97, January 1997. Proof-Carrying Authentication Andrew W. Appel and Edward W. Felten. 6th ACM Conference on Computer and Communications Security, November 1999. The “Proof-Carrying Code” paper is an extension on Tuesday’s presentation on Certifying Compilers. However, the “Proof-Carrying Authentication” is a new topic that uses similar logic to Proof-Carrying Code to prove the right of authentication. Proof-Carrying Code (quick review) Prof. Simha Stuart code proof Can Professor Simha trust me that my code is safe to run on his computer? Diagram from “Proof-Carrying Code” paper The Basic ideas of the paper: General Proof Carrying Technique With Specific Implementations: •Safety Policy •Safety Proofs •Validation of Safety Proofs The implementation in the paper uses First-Order Predicate Logic as a basis to formalize the safety policy. The safety rules are expressed as a Floyd-style verification condition generator When given a program and a set of preconditions and postconditions the system can produce a verification condition predicate (VC) in First–Order Logic. If the VC can be proven using the proof rules associated with the logic, then the program satisfies the safety invariants. If the VC cannot be proven, then the program does not satisfy the safety invariants and is unsafe to run. So what is First-Order Predicate Logic? First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as "there exists an x such that..." In our case: The statements that need to be quantified are the annotated lines of code where type verification is needed. The Typing Rules Theorem 3.1 Any program with a valid verification condition starting in a state that satisfies the preconditions will only reference valid memory locations Theorem: For any program Π, set of invariants Inv and postcondition Post such that Π0 = INV Pre, if ►VC (Π, Inv, Post) and the initial state satisfies the precondition Pre, then the program reads only from valid memory locations as they are defined by the typing rules, and if it terminates, it does so in a state satisfying the postcondition. Theorem 3.2 + Corollary These theorems can be used to help prove adequacy of the first-order logic to guarantee type safety as defined by the safety policy Recap of Paper Proof-Carrying code is a mechanism to allow code users to be guaranteed safe code in regards to their safety policy. The main contribution of the paper was the fact that they implemented a system of program verification using certification (creating the proof on the code producer side) and proof validation (on the code user side) Paper number 2: “Proof-Carrying Authentication” Main Idea: Say for example a client desired access to a server, but needed to be authenticated. The authors are purposing a strategy, analogous to Proof-Carrying Code, that makes the user construct a proof that shows they should have access. The server then verifies correctness of the proof and lets the user proceed Proof-Carrying Authentication proof Access? Grant Access Check Proof Example of Proof-Carrying Authentication Protocol Suppose Stuart wanted to access an email server named GWU. The server receives a request from Stuart to “read Stuart’s email.” GWU’s control list says that Stuart can read his email. But is the request really from Stuart? How do we solve this? Add a Certificate Authority The server GWU trusts the CA to guarantee key-to-name bindings, and the server also knows the CA’s public key. Stuart then obtains a certificate signed by CA’s private key that says “Ks is Stuart’s public key.” Stuart then signs the message ”read Stuart’s email” with his private key. With this information GWU can safely grant the request to “read Stuart’s email.” Constructing the Proof The server GWU starts with the following assumptions: A1 = trustedCA(CA) A2 = keybind(Kc, CA) A3 = Stuart controls read Stuart’s email With these assumptions published to Stuart, Stuart can prove to the server GWU that he should be able to read his email using high-order logic. Proof: How the Proof is checked: First check the two digital signatures to establish the fact that Ks signed “read Stuart’s email” and Kc signed the keybind(Ks, S) From assumption A1 we can prove C controls keybind(Ks, S) by the lemma trustedCA_e. From A2 and a digital; signature we prove C(keybind(Ks, S)) by the keybind_e lemma. Proof Check continued Now from the last two results (C controls keybind(Ks, S) and C(keybind(Ks, S))) we prove keybind(Ks, S) by the controls_e lemma. From this result and a signature we prove S(read Stuart’s email) by the keybind_e lemma. Finally, from assumption A3 and S(read Stuart’s email) we prove “read Stuart’s email” by controls_e. Thus, the server GWU authenticates the user Stuart and allows him access to his email Note: All parts of the proof need to be true/ checked in order for authentication to occur Advantages Just like Proof-Carrying Code, the burden is placed on one side. It is easy to check a proof, but hard to create a proof. The user takes the burden and leaves the server to perform the easy proof checking Implementation of previous example in Twelf Twelf is an implementation of the Edinburgh Logical Framework. A standard way of representing this protocol is needed and the code on the next slide is an example of the standard used in this paper. Twelf representation Overview Overall, this example has shown that higher-order logic can be used for authentication purposes The proofs can be small and not too difficult to create. Also, proof checking is easy in comparison to proof creation. Sources George C. Necula. Proof-Carrying Code POPL97, January 1997. Andrew W. Appel and Edward W. Felten. Proof-Carrying Authentication 6th ACM Conference on Computer and Communications Security, November 1999. Peter Lee http://www-2.cs.cmu.edu/Groups/fox/papers/neculaosdi96/node2.html Tue Sep 17 15:37:44 EDT 1996 Discussion