Transcript Logic Engineering

Towards
Automatic Verification
of
Safety Architectures
Carsten Schürmann
Carnegie Mellon University
April 2000
Subtitle
Twelf
A Tool to Reason About Formal
Systems
2
Motivation
CERT-advisories





[www.cert.org]
Computer Emergency Response Team
January 1999 – February 2000
29 Advisories total
11 Advisories: Buffer overflow (e.g. ftpd)
Others: Viruses, Denial of Service …
> 38% of vulnerabilities due to bugs
3
Motivation
We need tools to



Increase confidence in software
Engineer trusted bases for computing
Catch programming language design flaws
There is such a tool:
Twelf
4
Contributions
Design of Twelf


Meta-logic
[Schürmann 00]
Algorithms for automated deduction
Implementation of Twelf


Core
Meta theorem prover
Application of Twelf

Experiments
5
[Pfenning, Schürmann 99]
[Schürmann 00]
Outline of This Talk
Problem

Safety Architectures
Twelf

Design
Implementation

Experiments
Conclusion

Research Agenda
6
Trusting the Source?
Source
Compiler
Binary
Trusted Computing Base
Example:


WU-ftpd 2.6.0:
GCC-core 2.95.2:
17865 lines of code
433128 lines of code
Related work:

Piton/Micro Gipsy
[Moore, Young, Bevier 89]
7
Trusting Binaries?
Source
Compiler
Binary
Verifier
Trusted Computing Base
Example:

WU-ftpd 2.5.0 binary: 150 KB
[RedHat 6.1]
Related work:

Software fault isolation
8
[Wahbe, … 93]
Trusting Safety Proofs?
Source
Binary
Compiler
Proof Checker
Safety Proof
Safety Proof Language
Small Trusted Computing Base
Feasibility study

Packet filter
[Necula, Lee 96]
9
Safety Architectures
Proof Carrying Code




Logic: 129 rules
Logic: several 100 rules
Proof checker: 206 lines
Uses a logical framework
Typed Assembly Language



[Appel, Felty 99]
[Schürmann 98]
Type Theory: 31 rules
[Morrisett, Crary … 98]
Proof Checker: approx 4000 lines
Java Bytecode

[Necula, Lee 97]
Type system: 20 pages prose
Bytecode verifier
10
Logical Frameworks
Uniform representation language



Storing
Shipping
Checking
Logical Framework
Binary
Safety Proof
Proof Checker
Safety Proof Language
Logic-independent safety proof checker
11
Safety Proof Languages
First-order/higher-order logics
[Gentzen 35]
Temporal logics (CTL, CTL*, LTL)
Modal and linear logics
Type theories
[Pnueli, Manna, … 84]
[Girard 86]
Language and system-specific knowledge
12
Good Safety Proof Languages
Is The Safety Proof Language Good?
Consistency

Falsehood should not be derivable
Expressiveness

Small safety proofs require expressive logics
Extensibility

Possibility to add new admissible rules
13
Meta-Logical Frameworks
Meta-Logical Framework
Is The Safety Proof Language Good?
Logical Framework
Safety Proof
Proof Checker
Safety Proof Language
14
Rest of this Talk
Twelf
A meta-logical framework that supports
the representation of logics and type systems
and automates reasoning about them
Used at CMU, Princeton, Stanford…
15
Overview
Reasoning
Meta-logical Framework
• Consistency arguments
• Theorems about logics
• Inductive proofs
• Automated proof search
Safety Proof Language
Logical Framework
• Logic
• Judgments
• Inference rules
• Uniform language
• Formulas
• Direct encoding as proofs
• Types
• Direct encoding as objects
16
Let’s Start
Safety Proof Language
• Logic
• Judgments
• Inference rules
17
A Simple Logic
Intuitionistic logic: | A1  A2 | 
Sequent calculus:


Judgment:
Rules:
, A  A
axiom
[Gentzen 35]
A , , An  A
1


, A  B
impr
 A B
  A , B  C
impl
, A  B  C
  A , A  C
cut
C
18
Next: Logical Framework LF
Safety Proof Language
Logical Framework
• Logic
• Judgments
• Inference rules
• Uniform language
• Types
• Direct encoding as objects
19
Representation
Logical framework LF


[Honsell, Harper, Plotkin 93]
Simply typed λ-calculus
Dependent types
Paradigm


Judgments as types
Derivations as objects
Logical Framework
D
A1 ,, An  A
u1 : hyp A1 ,, un : hyp An | D : conc A
20
Representation (cont’d)
Inference rules as constants
, A  A
axiom
axiom : (hyp A -> conc A).
, A  B
impr
 A B
impr : (hyp A -> conc B)
-> conc (A imp B).
  A , B  C
impl
, A  B  C
  A , A  C
cut
C
impl : conc A -> (hyp B -> conc C)
-> (hyp (A imp B) -> conc C).
cut : conc A -> (hyp A -> conc C)
-> conc C.
21
Representation (cont’d)
Reasoning about the real world
is as good as the encoding is
Logic
Logical Framework
1-to-1
Theorem prover for LF
22
[Schürmann 98]
Notes on the Representation
We can look at the current field of problem
solving by computers as a series of ideas about
how to present a problem. If a problem can be
cast into one of these representations in a
natural way, then it is possible to manipulate it
and stand some chance of solving it.
[Allen Newell]
Elegance


Higher-order representation techniques
Dependent types
Benefit

Variables and substitutions come for free!
23
Next: Reasoning
Reasoning
• Consistency arguments
• Theorems about logics
• Inductive proofs
Safety Proof Language
Logical Framework
• Logic
• Judgments
• Inference rules
• Uniform language
• Types
• Direct encoding as objects
24
A (Not So) Simple Argument
Theorem [Admissibility]:
E
, A  C
Proof: by induction on A,D,E.
E'
, A, B  C
Case: E=
impr
, A  B  C
If
D
 A
and
F'
, B  C
impr
BC
[Gentzen 35]
then
F
C
by induction hyp. on D,E’
by application of impr
25
History of This Result







Fundamental theorem in Logic
[Gentzen 35]
Consistency of first-order logic
Structural proof
[Pfenning 95]
Twelf can prove it automatically [Schürmann 99]
Neither a toy problem nor a trivial problem
182 = 324 cases for full-first order
intuitionistic logic
One of the most basic theorems of logic and
automated deduction
26
Significance of This Result
It is not reasoning in a logic


Derivation in a logic is only an object
Admissibility lemma is not expressible
But reasoning about a logic



Step outside the logic
Analyze properties of the logic
Admissibility lemma is expressible
27
Next: Meta-logical Framework
Reasoning
Meta-logical Framework
• Consistency arguments
• Theorems about logics
• Inductive proofs
• Automated proof search
Safety Proof Language
Logical Framework
• Logic
• Judgments
• Inference rules
• Uniform language
• Formulas
• Direct encoding as proofs
• Types
• Direct encoding as objects
28
Problem
Reasoning about derivations is inductive
In general: LF signatures are not inductive
axiom : (hyp A -> conc A).
impr : (hyp A -> conc B)
-> conc (A imp B).
Negative occurrence
impl : conc A -> (hyp B -> conc C)
-> (hyp (A imp B) -> conc C).
Standard induction techniques do not apply
29
Closed World Assumption
Standard induction techniques assume


Fixed set of constructors
Existence of induction principles
Example: Natural number induction
zero:nat
succ:nat -> nat
30
Open World Assumption
No induction principles


Type definitions are open-ended
New types, new inference rules may be added
Example: Admissibility Theorem

Not stable under extensions of the world
Forms of objects are not predictable
31
Solution
Regular world
assumption
Open world
assumption
Closed world
assumption
32
Regular World Assumption
Extensions to the world are predictable!


Sound induction principle exist
But it is not standard!
axiom : (hyp A -> conc A).
h1 :hyp A1.
impr : (hyp A -> conc B)
-> conc (A imp B).
h2 :hyp A2.
impl : conc A -> (hyp B -> conc C)
-> (hyp (A imp B) -> conc C).
33
...
hn :hyp An .
Meta Logic
+
M2
Regular extensions of the world: 
Here  ::  | , u : hyp A
Theorem [Admissibility]:
D
 ::   | E, h : hyp A
F
If   A and , A  C then   C
A : o.C : o.
D : conc A.E : hyp A  conc C.F : conc C. true
34
Meta Logic
+
M2
(cont’d)
Formulas: F :: x : A.F | x : A.F | F1  F2 | true
Semantics:
 | x : A.F iff
 | F [ M / x] for all M , s.t.  | M : A
 | x : A.F iff  | F [ M / x] for some M , s.t.  | M : A
 | F1  F2 iff
 | F1 and  | F2
 | true
35
Meta Logic
+
M2
(cont’d)
Proof calculus for M2+


[Schürmann 00]
Judgment:  | P  F
Rules: see thesis
Theorem [Soundness of
+
M2]
[Schürmann 00]
If  | P  F then  | F
Proof: via realizability interpretation.
36
Twelf Implementation
+
M2
Implements a theorem prover for
Success due to regular world assumption
Automated proof search
No tactics
Lemmas
Ind.-variables
Twelf
Bound
37
Proof in M2+
Not found
Twelf Implementation (cont’d)
Splitting
Recursion
Filling
Case analysis over LF objects
Regular world assumption
Induction hypotheses
Regular world assumption
Applies an underlying LF prover
Or theorem prover for underlying logic
38
Experiments
Problem
Total time Reason
Cut-Elimination IL Admissibility of Cut
6min 35sec
    true false Cut-elimination
ND - Sequent
ND - Hilbert
0.28sec
ND -> Sequent
0.11sec
Sequent -> ND
0.12sec
Deduction theorem
0.12sec
Translation theorem
0.37sec
Machine: Pentium II, 400Mhz, 192MB RAM, Linux 2.0
39
Experiments (cont’d)
Total time Reason
Problem
Mini-ML
Value-soundness
0.13sec
Type preservation
0.42sec
Reduction theorem
0.66sec
(app/lam) Uniqueness of typing
Compiler (CPM)
Soundness
not yet. Compl. ind.
Completeness
0.31sec
(both directions) Proof equivalence
CCC
0.25sec
Translation lambda
Distributivity
0.46sec
3.392sec
not yet. LF Prover
Machine: Pentium II, 400Mhz, 192MB RAM, Linux 2.0
40
Experiments (cont’d)
Problem
Total time Reason
Church-Rosser
Append lemma
0.08sec
Substitution lemma
0.18sec
Diamond lemma
Strip lemma
5.6sec
3min 58sec
Confluence lemma
Church-Rosser thm
28.52sec
2.05sec
Machine: Pentium II, 400Mhz, 192MB RAM, Linux 2.0
41
Experiments (cont’d)
Problem
Total time Reason
LP (Harrop)
Soundness (Uni)
Canonical forms
0.34sec
Completeness (Uni)
0.28sec
Soundness (Res)
1.05sec
Completeness (Res)
0.52sec
Kolmogorov CL->IL Soundness
Rippling
0.31sec
9.55.sec
Completeness
not yet LF Prover
Equivalence lemma
0.65sec
Skeleton preservation
0.94sec
Machine: Pentium II, 400Mhz, 192MB RAM, Linux 2.0
42
Contributions
Design of Twelf



Design of a theorem prover for LF
Regular world assumption
Design of the sound meta-logic M2+
Implementation of Twelf


Core (together with Frank Pfenning)
Meta theorem prover
Application of Twelf

Experiments
43
Research Vision
I believe, that the demand for
safe and secure software,
networks, programming languages
will continuously increase.
I foresee myself designing,
implementing, and applying
the necessary tools.
44
Research Agenda
Towards real-world applications




Network protocol design
Security protocol design
Programming language design
Software engineering
45
Research Agenda (cont’d)
Design and Implementation



Meta logic + Constraints
Lemma generalization
Natural language explanation
46
Conclusion
A meta-logical framework
(Twelf)
that supports
the representation of logics and type systems
and automates reasoning about them
http://www.twelf.org
47