Transcript slides, ppt - Susmit Sarkar

Small Proof
Witnesses for LF
Susmit Sarkar
Brigitte Pientka
Karl Crary
Motivation : Untrusted Code

Want : execute untrusted code
Internet
Code
Consume
r
Code
Solution : Certified Code

Solution : Certificate with Code
Internet
Code
Code
Certificate
Consume
r

Proof Carrying Code [Necula]
What is a Certificate?

Prove Code is Safe
Easily checkable by Code Consumer

First Answer : Proof in a Logic

Logical Framework (LF)

Uniformly represent logics (and proofs)
Well-studied properties
Used extensively [PCC, FPCC, TALT,…]

Problem : Proofs are BIG!


Use Proof Search?

Ask Code Consumer to search for proof



Caveat : Higher-order Logic Programming
Advantage : Zero proof size
Disadvantage : Large time required
Idea : Proof Search with Guidance




Do Proof Search
Look at proof to resolve Don’t Know
choices
All we really require are the choices
Encode as “oracle” [Necula and Rahul]
What is a Certificate? … contd.

New Answer : Sequence of choices made
(as a position number from available
choices)

Can be efficiently encoded
Time to check sufficiently low

Our Contributions


Oracles for higher-order logic programming
Handle the entire LF language (as
implemented in Twelf)



Previous efforts [Necula et al, Wu et al] restricted
to a subset
Generic oracle creation/verification for a
variety of logics
Efficient Term-Indexing strategies
Rest of Talk

Higher-order Logic Programming



Challenges
Instrumentation to generate / verify oracle
Experimental results
Higher-order Logic Programming

Goals may have nested implications and universal
quantifiers

Depth-First Search (like Prolog)
New Issues:




Dynamic Assumptions added (Scoping rules)
Term language is higher-order (Requires Higher Order
Unification)
Efficient Term Indexing strategies needed
Proof Search (producing proof)


Have set of dynamic assumptions 
Case : Goal is 8 x. G :

Solve G [a/x] in  (“a” is new parameter)
Get proof M [a/x] for subgoal

Proof for goal is  x. M

Proof Search … contd.

Case: Goal is G1 ¾ G2 :

Add clause u:G1 to 
Solve for G2 under this extended set of
assumptions
Get proof M for subgoal

Proof for goal is  u. M


Proof Search … contd.[2]

Case : Goal is Atomic

Choose clause C (from program or dynamic
assumptions) matching goal
Solve subgoals of clause
Get proof M for subgoals

Proof for goal is C . M



records C used, and M for rest
Higher-Order Term Indexing

Term Indexing strategy important



Reduction of choices is efficient for oracle size
Our strategy : Higher-order Substitution
Trees [Pientka]
Generalize Substitution Trees
Example: A Natural Deduction Logic
alli : prov (forall  x. P x)
<- ( x. prov (P x)).
alle : prov (P T)
<- prov (forall  x. P x).
impi : prov (imp P1 P2)
<- (prov P1 -> prov P2).
impe : prov P
<- prov (imp P1 P)
<- prov P1.
Example Query
` prov (forall  y. (imp (forall  x. p x) (p y)))
alli
alle
impe
(1/3 )
`  a. prov (imp (forall  x. p x) (p a))
` prov (imp (forall  x. p x) (p a))
alle
impe
impi
(2/3 )
` prov (forall  x. p x) ¾ prov (p a)
u:prov (forall  x. p x)` prov (p a)
u
alle
u:prov (forall  x. p x) ` prov (forall  x. p x)
impe
(1/3 )
Oracle Generation / Verification

Generating Oracle assumes Proof Term
available
Verifying Oracle assumes Oracle available

Follow complementary procedures


Similar to proof search procedure sketched out
Instrumented Proof Search

Case : Goal is 8 x. G :



Solve [a/x] G
No choice to be made
Case : Goal is G1 ¾ G2 :


Solve G2 in extended set of dynamic
assumptions
No choice to be made
Atomic Goal … Generation

Case : Goal is atomic


Choose clause C. Solve its subgoals
During Generation,



Look at proof term (records choice)
Count choices available
Oracle records number of choice made
Atomic Goal … Verification

Case : Goal is atomic


Choose clause C. Solve its subgoals
During Verification,



Look at oracle (records positional number of
choice)
Count choices available
Take indicated choice
Results : Time
Refinement
Multiplication
Square
FPCC
Closure
Increment
Proof Search
Time (sec)
Witness
Checking
Time (sec)
Speedup
5.81
1.10
5.3
12.55
1.85
6.8
12.26
0.47
26.1
11.55
0.70
18.3
Results : Proof Size
Proof Size
(bytes)
Refinement
Multiplication
Square
FPCC
Closure
Increment
Witness
Size (bytes)
Size
Reduction
15,654
169
92.6
25,303
242
104.6
201,910
638
316.5
441,965
703
628.7
Conclusions



Instrumented a proof search procedure to
produce / verify small witnesses
Handle all of LF (higher-order logic
programming required)
Experimental Study of technique