Transcript Code-Carrying Proofs (CCP)

Code-Carrying Proofs
Aytekin Vargun
Rensselaer Polytechnic Institute
Outline
 Introduction
 Proof-Carrying Code (PCC)
 Code-Carrying Proofs(CCP)
 Sample CCP session
 Future Work
Potential Problems to be Solved
 Memory Safety

illegal operations or illegal access to memory
 Security

unauthorized access to data or system
resources
 Functional Correctness

whether the code does correctly what it is
formally required to do
Two Solutions
 Proof-Carrying Code (PCC)
 Code-Carrying Proofs (CCP)
Proof-Carrying Code (PCC)
 Developed by Necula and Lee [1996] at
CMU.
 Basic Idea: Use machine-checkable proofs as
certificates.
 Proof construction is harder than proof
checking


Code producer provides the proof
Code consumer checks it
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
Source Code
Touchstone
Compiler
PCC
Tampered
VCGen
Native Code
With Annotations
Verification Condition
Theorem Prover
Safety Policy
Safety Proof
Code Producer
Hacker
Native Code
With Annotations
Code Consumer
Tampered
Safety Proof
Safety Policy
VCGen
Verification Condition
No
CPU
Proof Checker
Proof is either invalid
or
is not the proof of the VC
Source Code
Touchstone
Compiler
PCC
Tampered
VCGen
Native Code
With Annotations
Verification Condition
Theorem Prover
Safety Policy
Safety Proof
Code Producer
Hacker
Tampered
Native Code
With Annotations
Hacker
Code Consumer
Tampered
Safety Proof
Safety Policy
VCGen
Verification Condition
(may change)
Ok
CPU
Proof Checker
Safety is guaranteed
if the tampered proof is the
proof of the new VC
Foundational PCC
 Developed by Appel in [2000] at Princeton
 VCGen is a large program. Replace it!
 Basic Idea:
 Define the semantics of the machine
instructions and safety rules
 Use foundational mathematical logic instead of
programming-language-specific axioms or
safety rules
 No particular type system
Foundational PCC
 Prove w.r.t. the formal machine language
semantics
 Operates at a very low level of abstraction
 It does reduce dependency on a large
program (VCGen) but this is true for CCP
also
Code-Carrying Proofs (CCP)
 Start with axioms that define functions

The form of axioms is such that it is easy to
extract executable code from them.
 Prove that the defined functions obey certain
requirements
 The producer transmits



Axioms
The correctness theorems
And their proofs
Code-Carrying Proofs (CCP)
 No explicit code transmission
 The consumer checks proofs to see if the
correctness theorem is proved
 If proof checking succeeds, the consumer
applies the code extractor to the axioms and
obtain the executable code
Code-Carrying Proofs (CCP)
 CCP attempts to solve Functional
Correctness problem
 We are dealing with a higher-level language
Axioms & Theorems
CCP
Theorem Prover
Axioms & Proofs
Code Producer
Code Consumer
Requirements
Proof Checker
Axioms & Theorems
Code Extractor
Code
CPU
Axioms & Theorems
CCP
Tampered
Requirements
Theorem Prover
Axioms & Proofs
Code Producer
Hacker
Code Consumer
Tampered
Axioms & Proofs
Requirements
Proof Checker
(Failed Proofs)
Code Extractor
(No Code)
CPU
Issues
 Encoding axioms and proofs
 Proof Checking
 Tests to be applied by the consumer to new
function definitions (definitional principle)



Syntactic Property
Consistency
Termination
 Implementing Code Extractor
Athena
 Implemented by K.Arkoudas
 A language for both:


Ordinary Computation
Logical Deduction
Athena
Ordinary Computation Language
 Provides higher-order functions
 Has primitive functions for



Unification
Matching
Substitution
Athena
Logical Language
 Special Deductive Forms

dcheck, dbegin, assume, …
 Primitive Deduction Methods

mp, both, left-and, …
 Declarations

structure, declare, …
 Directives

load-file, clear-assumption-base, …
Athena
Advantages
 Better Proof Readability
 Machine checkable proofs
 Makes it possible to formulate and write
proofs as methods
 Generic Proofs

write the proof once and instantiate it to prove
specific cases
Code Extractor
 Quantified Equations and Conditional
Equations
 These are clauses of a recursive function
definition
 CE has to be able to combine these into a
recursive function
Code Extractor
 CE can extract pure functions

it is not capable of extracting destructive
functions
 Example Functions:

searching functions, sum
 It cannot handle functions like:

in-place reverse, sort
Code Extractor
 We have been working on simple functions.
But:


In analogy to STL, it is useful to have a library
of simple functions from which more complex
functions can be composed, especially if the
functions are generic
It is possible for code extractor to extract
complex functions composed of such simple
functions
Future Work
 New Definitions and Tests to be applied
 Defining Memory
 More Proof Examples
 Improving the Code Extractor
 Memory Safety
 Generic Proofs and Proof packaging