Transcript Proof Carrying Code

Proof Carrying Code
Zhiwei Lin
Outline

Proof-Carrying Code
 The Design and Implementation of a
Certifying Compiler
 A Proof – Carrying Code Architecture for
Java
 A Certifying Compiler for Java
Proof-Carrying Code
George C.Necula
Carnegie Mellon University
January 1997
Proof-Carrying Code

Why do we need Proof-Carrying Code
– In distributed and web computing, particularly when
mobile code is allowed.
– Agent A on one part of the network write a component
of the software in ML, compile it to native machine
code, then transmit it to an agent B on another node for
execution
– How does agent A convince the agent B that the native
code have the type-safety properties shared by all ML
programs
Proof-Carrying Code

A code consumer must become convinced
that the code supplied by an untrusted code
producer has some set of properties

We need to establish “Trust”between the
consumer and the producer
Proof-Carrying Code

One Solution => Cryptography
– Ensure that the code was produced by a trusted
person or compiler
– While, it’s weak because of it’s dependency on
personal authority
– Even trusted persons, or compilers written by
them, can make errors occasionally
Proof-Carrying Code

Our Solution => PCC
– Code consumer specified Safety policy, that is under
what conditions it considers the execution of a foreign
program to be safe and make it public to code consumer
– Code producer creates a formal safety proof that
proves, for the untrusted code, adherence to the safety
rules
– Code consumer uses a simple and fast proof validator to
check that the proof is valid and hence the foreign code
is safe to execute
Proof-Carrying Code

3 Stages of PCC
– Stage 1: Certification
 The coder producer compiles the source code and
verifies the program with respect to the specification
described by the safety policy
 A proof of successful verification together with the
native code component forms the PCC binary
 Code producer can store the resulting PCC binary
for future use. Or can deliver it to code consumers
for execution
Proof-Carrying Code

3 Stages of PCC
– Stage 2: Validation
 Code consumer validates the proof part of PCC
binary and loads the native code component for
execution
 The existence of the proof allows for the verification
process to be performed off-line and only once for a
given program, independently of the number of
times it’s executed
Proof-Carrying Code

3 Stages of PCC
– Stage 3: Execution
 Code Consumer executes the machine-code program
many times without performing additional run-time
checks because the previous validation stage ensures
that the code obeys the safety policy
Proof-Carrying Code
Source Program
Compilation&
Certification
PCC
Binary Native Code Safety Proof
Code Producer
User Process
Code Consumer
Runtime System
Enable
CPU
Proof Validation
Safety Policy
Certifying Compiler
George C.Necula, Peter Lee
Carnegie Mellon University
June 1998
Certifying Compiler

Certifying Compiler vs. PCC
– PCC depends on semi-automatic theorem-
proving techniques to generate safety proofs
– Certifying Compiler produces safety proofs for
a PCC system for type safety completely
automatically
Certifying Compiler

What’s Certifying Compiler
– A combination of a compiler and a certifier
– A compiler that translates programs into
assembly language programs, and a certifier
that automatically checks the type safety and
memory safety of any assembly language
program produced by the compiler
Certifying Compiler
Type Specification
Compiler
Certifier
Annotated Code
Proof/Counter Example
Overview of the Certifying Compiler
Certifying Compiler

Overview of the Certifying Compiler
– The Compiler is a traditional compiler adapted
to produce type specifications and code
annotations in addition to the assembly
language target program
– The purpose of the code annotation is to make
it possible for a simple certifier to understand
enough of the code to verify its type safety and
memory safety
Certifying Compiler

The Certifier subsystem is itself a pipeline
composed of three subsystems
– The verification condition generator(VCGen)
– The prover
– The proof checker
Certifying Compiler
VCGen
Safety predicate
Prover
Proof
Proof Checker
The Structure of the Certifier
Certifying Compiler

Certifying Steps
– Step 1: Verification Condition
 VCGen scans the annotated assembly language
program and, using the type specifications and the
code annotations, produces a safety predicate for
each function in the code, such that the safety
predicate has a proof if and only if the assembly
language program is memory-safe and type safe
according to the typing specification
Certifying Compiler

Certifying Steps
– Step2: Prover

The safety predicate is submitted to a prover
for first-order predicate logic that produces a
formal proof of the predicate
Certifying Compiler

Certifying Steps
– Step3: Proof Checker

The safety predicate and its proof are given
to a very simple proof checker that verifies
that we actually have a valid proof of the
required safety predicate, and therefore the
compiler output is memory safe and type
safe
A Proof-Carrying Code
Architecture for Java
Christopher Colby, Peter Lee, and
George C.Necula
In 12th CAV00, Chicago,
15 July 2000.
A PCC Architecture for Java
Java Bytecode
Native Code
VC Generator
Certifying Compiler
Annotations
VC Generator
VC
Axioms
& Rules
VC
Proof Checker
Host
Proof
Proof Generator
Code Producer
Axioms
& Rules
A PCC Architecture for Java

A PCC architecture comprise two parts:
– Code Producer

A compiler generates native code from a
java .class file. This compiler is largely
conventional except that it attaches some
logical annotations to the resulting binary.
A PCC Architecture for Java

A PCC architecture comprise two parts:
– Code Producer
• The annotated binary is then analyzed by
verification-condition generator. The VC Generator
outputs a logical predicate that describes a
precondition that, if true, would imply that any
possible execution of the binary is safe by scanning
each native-code instruction and emitting safety
conditions as they arise. The result is called the
verification condition(VC)
A PCC Architecture for Java

A PCC architecture comprise two parts:
– Code Producer
 The VC is sent to an automated theorem prover,
which attempts to prove the VC and, if successful,
outputs the resulting logical proof in binary form.
The annotations and proof are added to the binary as
an .lf segment, thus producing a PCC binary. This
object file can be loaded and linked with existing
tools just like any other object file.
A PCC Architecture for Java

A PCC architecture comprise two parts:
– Host
 Host first separates the annotated binary from the
proof
 Host then runs a VC generator on the annotated
binary to produce a VC from a safety policy
specified by the same set of rules an axioms
 Lastly, it checks the proof to make sure that it’s
indeed a valid proof under the safety policy.
Advantages Over Related
Techniques

The trustworthiness of the proof-checker is an
important advantage over approaches that involve
the use of complex compilers or interpreters in the
code consumer. Here, almost the entire burden is
on the code producer. The code consumer has only
to perform a fast, simple, and easy-to-trust proofchecking process
 No Cryptography or trusted third parties are
required because PCC are ‘self-certifying’
Advantages Over Related
Techniques

As the untrusted code is verified statically
before executed, we not only save execution
time but we detect potentially hazardous
operations early, thus avoiding the
situations when the code consumer must kill
the untrusted process after it has acquired
resources or modified state
Conclusion

PCC Theory
 Certifying Compiler
 PCC Architecture for Java
 Advantages of PCC