Princeton/Yale PCC Project Status
Download
Report
Transcript Princeton/Yale PCC Project Status
Scaling Proof-Carrying Code
to Production Compilers and
Security Policies
Edward W. Felten Princeton University
Andrew W. Appel Princeton University
Zhong Shao Yale University
February 2000
7/17/2015
1
The problem: Mobile Code Security
Code Producer
Source
Program
Compiler
Code
Code Consumer
Execute
load r3, 4(r2)
add r2,r4,r1
store 1, 0(r7)
store r1, 4(r7)
add r7,0,r3
add r7,8,r7
beq r3, .-20
?
Private files
Network access
Launch control
etc.
7/17/2015
2
Existing Practice: Trust or Enforcement
Enforcement
Trust
Social mechanisms
prevent misbehavior.
Technical mechanisms
prevent misbehavior.
Run only trusted code.
Run untrusted, safe code.
Technology
Technology
7/17/2015
public-key infrastructure
code signing
Subject to corruption
Works for any security
property
proof-carrying code
High assurance
Works for only some security
properties.
3
Technical Objectives
Secure integration of components can be achieved
through trust or protection. Our objectives:
Protection mechanisms for secure integration of
untrusted components.
Authentication mechanisms for flexible integration of
trust and protection.
7/17/2015
Our approach: typed intermediate languages, certifying
compilers, proof-carrying code.
Our approach: proof-carrying authentication.
4
Expected major achievements
Felten, Appel
Princeton U.
Appel, Felten
Princeton U.
Shao
Yale U.
Distributed
Authentication
Frameworks:
Mobile Code
Security:
Certifying
Compilers:
Proof-Carrying
Authentication
Secure
Key
Distribution
File servers
7/17/2015
Secure
Linking
Proof-Carrying
Code
FLINT/ML
FLINT/Java
PCC systems
for ML, Java
Language- &
machineindependent
mobile code
safe lang.
interop.
5
Part I: Proof-Carrying Code
Distributed
Authentication
Frameworks:
Proof-Carrying
Authentication
Secure
Linking
7/17/2015
Appel, Felten
Princeton U.
Mobile Code
Security:
Proof-Carrying
Code
Certifying
Compilers:
FLINT/ML
FLINT/Java
PCC systems
for ML, Java
6
Existing Practice: Hardware VM protection
Code Producer
Source
Program
Compiler
Machine
Code
load r3, 4(r2)
add r2,r4,r1
store 1, 0(r7)
store r1, 4(r7)
add r7,0,r3
add r7,8,r7
beq r3, .-20
Disadvantages:
Code Consumer
Execute
Operating System
virtual memory
Protected
resources
Large trusted code base of O.S.
Clumsy, slow interfaces between
trusted & untrusted code
7/17/2015
7
Existing Practice: Software Fault Isolation
Code Producer
Source
Program
Compiler
Machine
Code
load r3, 4(r2)
add r2,r4,r1
store 1, 0(r7)
store r1, 4(r7)
add r7,0,r3
add r7,8,r7
beq r3, .-20
Disadvantages:
Slowdown of untrusted code
Clumsy, slow interfaces between
trusted & untrusted code
Complex TCB
7/17/2015
Code Consumer
SFI: Insert
extra
instructions
before
load, store,
& jump
instructions
Safe
Machine
Code
Execute
8
Existing Practice: Bytecode Verification
Code Producer
Java
Program
Compiler
ByteCode
load r3, 4(r2)
add r2,r4,r1
store 1, 0(r7)
store r1, 4(r7)
add r7,0,r3
add r7,8,r7
beq r3, .-20
Trusted
Computing
Base
Advantage:
Clean, fast, O-O interface
between trusted & untrusted code
Disadvantage:
Huge trusted computing base: JIT
7/17/2015
Code Consumer
Bytecode
Verifier
OK
Just-in-time
Compiler
Native code
Execute
9
Proof-Carrying Code
Code Producer
Source
Program
Hints
Compiler
VCgen
+
Policy
Verification
Condition
load r3, 4(r2)
add r2,r4,r1
store 1, 0(r7)
store r1, 4(r7)
add r7,0,r3
add r7,8,r7
beq r3, .-20
(safety theorem)
Safety Proof
Prover
$-i(
-i(...
-r (
...)
)
)
$xy.y=r1 ...
7/17/2015
Native Code
(Necula & Lee 1997)
Code Consumer
Execute
VCgen
+
Policy
Trusted
Computing
Base
Verification
Condition
(safety theorem)
$xy.y=r1 ...
Checker
OK
10
Advantages of Proof-carrying code
Trusted Computing Base is
quite small
7/17/2015
(or prover!)
Can use types, dataflow,
induction, any other provable
property
Automated theorem-proving
is mature enough for
application
In contrast, optimizing JITs
are quite large
JIT is in TCB
Bug in JIT is security hole
Bytecodes too close to source
Verification conditions can be
general, flexible, expressive
Safety policy
Proof checker
No need to trust compiler
too easy to reverse-engineer
too hard to optimize at site
of origin
Many compiler optimizations
don’t fit in bytecode type
system.
Bytecodes are ad-hoc,
ill-specified
11
Shrinking the TCB
Code Producer
Source
Program
Compiler
VCgen
Policy
+
Hints
Policy
Verification
Condition
Verification
Condition
Native Code
load r3, 4(r2)
add r2,r4,r1
store 1, 0(r7)
store r1, 4(r7)
add r7,0,r3
add r7,8,r7
beq r3, .-20
(safety theorem)
Safety Proof
Prover
$-i(
-i(...
-r (
...)
)
)
$xy.y=r1 ...
Prover
7/17/2015
- make the prover work harder
Code Consumer
Execute
VCgen
Policy
+
Policy
Verification
Condition
Verification
Condition
(safety theorem)
$xy.y=r1 ...
Checker
OK
12
Safety policy
(trusted computing base)
Logical connectives (and,or,)
(AB) A B, C
C
P Q
A,B, Q
(AB), Q
P, Q
A
B
(AB)
P, P
A
A B
Machine Semantics
P ( [m[n+rj]/ri]Q readablem(n+rj) )
P {load ri,n(ri)} Q
P ( [ m[n+rj ri]/m]Q writablem(n+rj) )
P {store ri,n(ri)} Q
VCs1 {S1 S2 ... Sn}VCs true
safe(S1 S2 ... Sn)VCs
Read/write policies
read_write V
read_only V
readable V
readable V
read_write V
write_only V
writable V
writable V
V start
Typing rules
v :m intlist
v :m intlist
m[v]=1
readable(v)
readable(v+1) readable(v+2)
v :m intlist
v :m intlist
m[v]=1
m[v]=0 m[v]=1
m[v+2] :m intlist
read_write V
7/17/2015
13
How to shrink the safety policy
Machine Semantics
Logic: and, or, ...
Machine
Semantics
Shrink by
factoring
Read/write policies
Eliminate by
Typing rules
7/17/2015
using a semantic
model of types
14
Part II: Proof-Carrying Authentication
Felten, Appel
Princeton U.
Distributed
Authentication
Frameworks:
Proof-Carrying
Authentication
Secure
Key
Distribution
File servers
7/17/2015
Mobile Code
Security:
Proof-Carrying
Code
Certifying
Compilers:
FLINT/ML
FLINT/Java
Secure
Linking
15
Authentication: Existing Practice
Alice
“read foo”
signature + cert
Bob
decision
procedure
cert
policy
Charlie
7/17/2015
16
Authentication: Our Approach
Alice
“read foo”
proof
[CCS99]
Bob
proof
verifier
cert
policy
Charlie
7/17/2015
17
Encoding Authentication in Logic
x. (KC signed x) (Charlie says x)
KC is Charlie’s key
“Alice’s key is KA”
signed KC
KC signed (x. (KA signed x) (Alice says x))
K. P. x.
I trust Charlie
for key certification
(KC signed y.(K signed y) (P says y))
(K signed x) (P says x)
x. (KA signed x) (Alice says x)
7/17/2015
18
Other Abstractions
groups
local name spaces
roles
delegation
time, expiration, and revocation
done with definitions and lemmas; no additions to the logic
7/17/2015
19
Encoding Other Frameworks
can encode other frameworks
how to do it
7/17/2015
paper sketches how to encode SPKI
make a definition for each SPKI primitive
prove each SPKI processing rule as a lemma
can help other frameworks interoperate
can serve as “machine code” for frameworks
20
Implementation
implemented in Twelf, which is based on the Edinburgh
Logical Framework
definitions, lemmas, and proofs are all Twelf code
size of proof (for the example)
7/17/2015
main proof is 123 tokens
proofs of lemmas are 108 tokens total
further reductions possible; active research area
21
Goal: Integrating Trust and Protection
PCC offers higher assurance than trust does.
But PCC doesn’t work for all properties.
“This program will not display misleading dialog boxes.”
“This control software won’t let the vehicle tip over.”
Integration allows mixed use of trust and protection
for different properties within the same program.
“Verify when we can; trust when we must.”
7/17/2015
22
Part III: Certifying compilers
Shao
Yale U.
Distributed
Authentication
Frameworks:
Proof-Carrying
Authentication
Secure
Linking
7/17/2015
Mobile Code
Security:
Proof-Carrying
Code
Certifying
Compilers:
FLINT/ML
FLINT/Java
PCC systems
for ML, Java
Language- &
machineindependent
mobile code
safe lang.
interop.
23
The FLINT certifying compiler
ML
Java
Parse &
semantic
Parse &
semantic
High-level FLINT
Safe C
Parse &
semantic
type-check
Analysis &
Optimization
Medium-level FLINT
type-check
Code Gen.
Low-level FLINT
Add new front-ends to build
new certifying compilers !
Key: use typed
intermediate languages!
Motto: If Joe Hacker
can understand it, we
will type it.
type-check
Program for execution
Theorem
Prover
7/17/2015
Safety
Theorem
24
Why typed IL ?
Safe and secure low-level mobile code
(Why? applets, JINI, active network, extensible systems)
Types for stating and verifying invariants
7/17/2015
Java VM language is too complex and high-level
PCC and TAL are good but how to generate them?
IDL for common component libraries
Safe and principled language interoperation
Help optimizations and compiler debugging
25
What makes a good typed IL ?
As low-level as possible (close to real machine)
makes TCB smaller; helps generate PCC and TAL
Machine-independent
Simple
7/17/2015
types used in the IDL will be read by programmers
Expressive
(still an IL)
need to prove not just simple type safety
Efficient
26
Recent progress in FLINT
New results
Examples: GC, reflection, type dynamic, pickling
Express inlining as staged compuation
Typechecking link-time cross-module optimizations
Current implementation
7/17/2015
Extending FLINT to support Java
Typechecking runtime type dispatches
Can handle Standard ML and MiniJava
Types are now propagated through all optimization
phases
Currently working on typed closure conversion
27
Metrics to measure success
Size of trusted computing base
(smaller is better)
Number & complexity of rules in safety policy
Size of proof checker
Size of other runtime-system components
Time, space needed for creating proofs
Time, space needed for checking proofs
Time, space to execute untrusted code
(relative to previous practice such as JIT’s)
7/17/2015
28
Task Schedule
Proof-Carrying
Authentication
Proof-Carrying
Code
Security Logic
PCC Logic
Sample safety policy
Prototype prover
-release certifying
ML compiler,
subset Java
Year 1
Distributed
Authentication
Software
ML PCC prototype
-release certifying
ML compiler
FLINT/ML
FLINT/Java
Year 2
Secure
Linking
Java PCC prototype
-release certifying
subset Java compiler
Year 3
7/17/2015
29
Technology Transfer
Key components are open-source, widely used in
academia
These components have been used in commercial
applications
7/17/2015
Standard ML of New Jersey (FLINT) compiler
LF (Twelf) proof checker
SML/NJ: maintenance of telephone switch software (Lucent)
LF: Cedilla systems’ secure Java JIT compiler
ML, Java software built with our system will be
compatible with existing ML, Java software and
software-development processes
30
Scaling Proof-Carrying Code
to Production Compilers and
Security Policies
Edward W. Felten Princeton University
Andrew W. Appel Princeton University
Zhong Shao Yale University
February 2000
7/17/2015
31
Language-independent safety policy
Machine Semantics
Logic: and, or, ...
Machine Semantics
Read/write policies
(programming-language specific)
(compiler specific)
Typing rules
Without types in safety policy, code consumer does not impose
choice of language & compiler on code producer
7/17/2015
32
Challenges from Java
OO primitives are too high level
method invocation; field selection; checkcast
Access control
objects of “twin type” can access private fields
Name-based subtyping hierarchy
Reflection (class Class), linking & loading
Concurrency
On-the-fly code optimizations
7/17/2015
33