Transcript Safe Kernel Extensions Without Run

Safe Kernel Extensions Without
Run-Time Checking
George C. Necula & Peter Lee
Using Build Integrated Checking
to Preserve Correctness
Invariants
Hao Chen & Jonathan S. Shapiro
Laura Hauser cs297
6/7/2005
Overview
•
•
•
•
•
Proof-Carrying Code
Safety Policy
MOPS
EROS
Experiments using MOPS & EROS
Problem
How can an operating system kernel determine that it is
safe to execute code supplied by an untrusted source?
Solution
•Proof-Carrying Code (PCC)
–Code producer provides a formal proof proving the code
supplied adheres to the safety policy
–This proof is easy to validate for the code consumer
Safety Policy
• 3 part policy
– Floyd style VC generator
• Computes a safety predicate in first order logic
based on the code to be certified
– Axioms to validate safety predicate
– Precondition
• Predicate in first order logic that the code
consumer guarantees to be valid when the
PCC binary is invoked
Problem
How do we maintain correspondence between software
design and implementation in a cost effective manner?
Solution
Use static model checking tools normally used for error
detection for error prevention by integrating them into
the development lifecycle
How do they propose to do it?
• MOPS
– Open source, flow sensitive model checker
for temporal safety properties
• EROS
– Robust, mature, capability-based operating
system derived from KeyKOS
What Are They Hoping to
Achieve?
•
Bug prevention
• Automated checks
•
Simplicity
• Someone without experience with the model checking
tool should be able to use it fairly easily
• Necessary code changes should not result in
incomprehensible / unmaintainable code
•
Scalability
• Time issue: Want to integrate MOPS into the compile and
build process
MOPS
• Static (compile-time) analysis tool
• Checks that programs perform certain
operations in defined sequences
(temporal safety properties)
• Can express many application security
properties
• Properties are expressed in a finite
state automaton (FSA)
MOPS Restrictions
• The program is single-threaded
• The program is memory safe
• The program is written in standard compliant
C with selected GNU C extensions
• The program does not violate the soundness
assumptions required by the user-specified
temporal safety property
The MOPS Process
Safety
Property
FSA
C Program
Parser
CFG
Model
Checker
Program satisfies
safety property
Error Traces
FSA: finite state automaton
CFG: control flow graph
EROS
(Extremely Reliable Operating System)
• Capability-based OS
• Chosen for:
– Interrupt-Style Kernel
– Single-Level Store
– Caching Design
• All of these properties rely heavily on
temporal preciseness for some reason or
another, making it ideal for MOPS checking
Experiments
• Control Flow
– This is what MOPS is designed to check
for
– Yield, Commit
• Typestate Properties
– Is it worthwhile to extend MOPS?
– Prepare Before GetRegs
Yield, Commit
• Every system call control path should invoke
exactly one of Yield() or Commit()
• Following a call to Commit(), it is a bug to
subsequently call Yield()
Prepare Before GetRegs
• Any call to proc_GetRegs32 requires that the
typestate of process p is “cached”
• Proc_Prepare(p) changes the typestate of this
process from “unknown” to “cached”
• Even typestate can be reduced to temporal safety
properties most of the time
Did They Reach Their Goals?
• Bug Prevention
– Was able to successfully find bugs in 4 of
the 5 test cases
• Could not statically define one of the typestate
experiments
– While not every invariant can be reduced
easily to temporal safety properties many
can
Did They Reach Their Goals?
• Simplicity
– Found that required modifications to fix
problems often yielded more readable /
maintainable code
– The EROS expert on the project was easily
able to use the tool MOPS
Did They Reach Their Goals?
• Scalability
– Development time on the MOPS end was
minimal
– Found that MOPS is minimally disruptive to
the build process
– Building and linking 12.13s to 31.34s
– Model checking 100.13s: only do for major
builds
References
• George C. Necula, Peter Lee. Safe Kernel
Extensions Without Run-Time Checking.
OSDI'96,October 1996.
• H.Chen and J.S.Shapiro. Using buildintegrated static checking to preserve
correctness invariants. Proceedings of the
11th ACM conference on Computer and
communications security, Washington DC,
2004.
• www.cs.ucdavis.edu/~hchen/paper/ndss04.pp
t