Type safety from the ground up.
Chris Hawblitzel
(joint work with Jean Yang, Juan
Chen, and Gregory Malecha)
1/28
Modern computer systems are great!
(but they have bugs)
2/28
Answer #1: Type Safety!
(but compilers have bugs)
source code
(e.g. C#)
Type checker
Compiler
• Catches many common bugs (at
compile time or run time):
• buffer overflows
• double frees
• ...
assembly
language
Web scripting: Java, Javascript, .NET, ...
Operating systems: SPIN, Singularity, ...
3/28
Example compiler bug (in Bartok)
counterexample:
i = -231
j = 231 - 1
j>i
vulnerability:
address = &(arr[0]) + 4*j
= &(arr[0]) + 4*(231 - 1)
= &(arr[0]) - 4
void F(int[] arr, int i) {
if (i <= arr.Length) {
// i ≤ arr.Length
int j = i - 1;
// j < i ≤ arr.Length
if (j >= 0) {
// 0 ≤ j < i ≤ arr.Length
// no bounds check required!
arr[j]++;
}
}
}
4/28
Answer #2: Typed Assembly Language!
(Morrisett et al, POPL 1998)
source code
(e.g. C#)
Compiler
typed
assembly
language
Type checker
• catches type errors in assembly language
program
• types for objects, stacks, code pointers, etc.
5/28
Answer #2: Typed Assembly Language!
(but run-time systems and operating systems have bugs)
source code
(e.g. C#)
Compiler
typed
assembly
language
run-time
system (GC, ...)
OS
services
Type checker
Linker / loader
6/28
Example GC vulnerabilities
MS07-057: Cumulative security update for Internet Explorer
Date: October 2007
...Internet Explorer 6 may exit with an access violation when the JavaScript
garbage collector runs and you have dynamically removed a TBODY, THEAD,
or TFOOT HTML tag from a table in Windows XP...
Mozilla Firefox Bug in JavaScript Garbage Collector Lets Remote Users Deny Service
Advisory: Mozilla Foundation Security Advisory
Date: Apr 16 2008
A remote user can create specially crafted HTML that, when loaded by the target
user, will trigger a flaw in the JavaScript garbage collector code and cause the target
user's browser to crash. ... The vendor indicates that similar crashes have been
exploitable in the past, so arbitrary code execution may be possible...
From: Apple Product Security
Date: Fri, 11 Jul 2008
...
Available for: iPhone v1.0 through v1.1.4,iPod touch v1.1 through v1.1.4
Description: A memory corruption issue exists in JavaScriptCore's handling
of runtime garbage collection. Visiting a maliciously crafted website may
lead to an unexpected application termination or arbitrary code execution.
This update addresses the issue through improved garbage collection.
7/28
Answer #3: Verification!
(via automated theorem proving)
source code
(e.g. C#)
Compiler
typed
assembly
language
run-time
system (GC, ...)
Type checker
low-level OS
services
Verifier
Linker / loader
8/28
Nucleus
Kernel
Verve: a verifiably safe OS
Small Operating System (C#)
Verify
safety
with TAL
checker
Bartok
Typed Assembly Language
Verified
Garbage
Collector
Verified
Threads
Verified
Interrupt
Handlers
“every assembly
language instruction
checked for safety”
Verified
Device
Interface
Verified
Startup
Verify
safety &
correctness
with
Boogie/Z3
Boot Loader
x86 Hardware
9/28
Verve: a verifiably safe OS
Small Operating System (C#)
Nucleus
Kernel
Bartok
Typed Assembly Language
GC Heap
AllocObject
AllocVector
GarbageCollect
Throw
(readField)
(writeField)
(readStack)
(writeStack)
•
•
•
•
•
•
Class types, interface types
Array types
Method invocations
Stack frames
Casts, array store checks
...
Threads
GetStackState
ResetStack
YieldTo
Device IO
VgaTextWrite
TryReadKeyboard
StartTimer
SendEoi
PciConfigRead32
PciMemSetup
PciMemRead32
PciMemWrite32
BUILD!
10/28
Related work
• (Mostly) type-based
– House (Hallgren et al)
– TALK (Maeda et al)
– Typed GC interface (Vanderwaart et al)
• (Mostly) interactive theorem proving
– FLINT / certified code (Shao et al)
– seL4 (Klein et al)
11/28
Demo: Boogie/Z3
12/28
Z3: Automated theorem prover
DECIDABLE THEORIES
boolean expressions
e ::= true | false | !e | e && e | e ==> e | ...
linear integer arithmetic e ::= ... | -2 | -1 | 0 | 1 | 2 | e + e | e – e | e <= e | ...
bit vector arithmetic
e ::= ... | e & e | e << e | ...
arrays
e ::= ... | e[e] | e[e := e]
quantifiers
UNDECIDABLE
e ::= ... | forall x.e | exists x.e
13/28
procedure CopyAndForward(ptr:int, _tj:int)
requires ecx == ptr;
requires CopyGcInv(...);
requires Pointer(r1, ptr, r1[ptr]);
...
{
call edx := GcRead(ecx + 4);
esp := esp - 4; call GetSize(ptr, edx, r1, r1);
call ebp := Mov(eax);
...
call edi := Mov(0);
automatic
call edx := Mov(0);
translation
loop:
assert 4 * edi == edx;
assert CopyGcInv(...);
...
if (edx >= ebp) { goto loopEnd; }
call copyWord(ptr, _tj, esi, edi, ebp);
call edi := Add(edi, 1);
call edx := Add(edx, 4);
goto loop;
Practical, verified
copying collector code
mov edi, 0
mov edx, 0
CopyAndForward$loop:
cmp edx, ebp
jae CopyAndForward$loopEnd
loopEnd:
call eax := Lea(esi + 4);
call GcWrite(ecx + 4, eax);
...
14/28
Memory management
Trusted specification
Code,
Interrupt IO-MMU DMA
page
area
Static fields, table
tables
GC info
Nucleus PCI
private tables
stack
General-purpose
memory
Thread C#/TAL
contexts stacks
GC
heap
Untrusted definitions
15/28
Memory management
...
by (trusted) specification
&& (forallDefined
i:int::{T(i)}
T(i) && Fi <= i && i < Fk && r1[i] != NO_ABS &&
(IsFwdPtr(gcMem[i + 4]) ==>
IO-MMU
DMA
Code,
Interrupt
Pointer(r2,
gcMem[i
+ 4] - 4, r1[i])
&& AlignedHeapAddr(i
+ 4)
page
area
Static fields,
table
&& word(gcMem[i + 4]))
tables
GC
info
...
Nucleus PCI
private tables
stack
fromspace
tospace
General-purpose
memory
Thread C#/TAL
contexts stacks
GC
heap
Untrusted definitions
16/28
Memory management
Trusted specification
Code,
Interrupt IO-MMU DMA
page
area
Static fields, table
tables
GC info
Nucleus PCI
private tables
stack
General-purpose
memory
Thread C#/TAL
contexts stacks
GC
heap
Untrusted definitions
17/28
Memory management
Trusted specification
Code,
Interrupt IO-MMU DMA
page
area
Static fields, table
tables
GC info
General-purpose
memory
IO-MMU
IO page
table
...
and(ptr, 4095)
== 0
Nucleus
PCI
GC
IO page
&&(forall i:int::{T(i)}
Thread
C#/TAL
private
tables
heap
table
T(i) && 0 <= i && i < 512 ==>
contexts
stackIoPageTableEntry(IomMem[ptr
+ 8 * i], stacks
IomMem[ptr + 8 * i + 4])
...
ptr
IO page
table
Untrusted definitions
18/28
Threads and interrupts
TAL
code
void KernelMain() {
…
Interrupt
// Schedule thread, wait for exception or
table
0
// interrupt
Interrupt/error handling
ScheduleNextThread();
Stacks
procedure InterruptHandler(stackState:[int]StackState,
…);
// CurrentThread received exception,
requires StackState[S] ==
// StackRunning;
interrupt, or exited voluntarily
ensures NucleusInv(... uint cid = CurrentThread;
StackState[S
:= StackInterrupted(eax,
Thread
t = threadTable[cid];ebx, …)]
[Stack0
:= StackRunning]
…
…);
}
19/28
Micro-benchmarks
Verve
functionality
Round-trip
yield
Round-trip
wait + signal
Cycles
Comparisons
Cycles
98
L4 (IPC)
224
SeL4 (IPC)
448
Singularity (yield)
2156
Linux (yield)
2390
Windows (yield)
3554
216
20/28
Size of code, specification
C# code (100% safe)
35,000
Copying Mark-sweep
Specification Boogie lines
1517
Verified Boogie lines
5189
5734
3x code
x86 instructions
1747
Boogie verification
• ~1 person-year work
• Boogie/Z3 runs in ~10 minutes
1859
CODE!
21/28
Building Verve
Kernel.cs
Compiler
Boogie/Z3
Translator /
Assembler
Verified
Nucleus.bpl (x86)
Kernel.obj (x86)
Specification
Boot loader
TAL checker
Linker /
ISO generator
Verve
.iso
DEMO!
22/28
Bugs in the trusted computing base
Bug
Whose fault?
InitializeGC: clobber ebp
AllocObject: off-by-4
debugger stub
linking GC tables
String GC descriptor
Boogie/Z3
Translator /
Assembler
Specification
Windows/Bartok
procedure
procedureInitializeGc();
AllocObject(...);
Specification
TAL checker
requires
requires
SMemRequireRA(...);
isStack(S);
public sealed class String : ...
Specification
Debugger stub
requires
requires
NucleusInv(...);
{ MemInv(...);
Code,
......
private int m_arrayLength;
Linker
/
ISO
gen
TAL
checker
Static
fields,
modifies
ensures Eip,
eax
eax,
== 0int
...,
ebp,
esp;
private
m_stringLength;
GC info
ensures
|| Pointer(toAbs,
WellFormed(toAbs);
eaxm_chars;
- 4, abs);
internal
char[]
Specification
TAL checker
ensures
ensures ebp
ebp
==old(ebp);
old(ebp);
... ==
Specification
Boot loader
TAL checker
Debugger stub
Linker /
ISO generator
23/28
Towards foundational Verve
(Gregory Malecha)
Specification for values
Specification for objects
Specification for stack frames
...
Nucleus
specification
Well-typed registers
Well-typed objects
Well-typed stack frames
...
TAL checker
Goal: mechanized
connection
24/28
Unified invariant
...
&& (forall i:int::{T(i)}
T(i) && Fi <= i && i < Fk && r1[i] != NO_ABS &&
(IsFwdPtr(gcMem[i + 4]) ==>
Inductive
Pointer(r2, gcMem[i
+ 4] - 4,WellTypedIns
r1[i])
-> Instr -> CodeType -> Prop :=
&& AlignedHeapAddr(i: CodeType
+ 4)
| Tmov : forall st st' from to ty,
&& word(gcMem[i + 4]))
opdType st from ty ->
...
regTyUpd st to ty = st' ->
WellTypedIns st (Imov to from) st‘
| ...
Nucleus invariant
+ TAL well-typedness
25/28
Unified invariant
MOV
edx, esi
CALL
...Nucleus...
MOV
edx, esi
CALL
...Nucleus...
MOV
esi, eax
Nucleus invariant
+ TAL well-typedness
TAL instruction = 1 step
Nucleus call = 1 step
Each step maintains unified invariant
26/28
Progress on “foundational Verve”
YieldTo(s:int,
•procedure
Approach
so far...);
(roughly)
requires ecx == s;
– Mechanically
Boogie&&
Spec
requires
(StackState[s]translate
== StackRunning
...) into Coq
|| (StackState[s]
== StackYielded(...)
– Specify
“step” relation
in Coq && ...)
|| (StackState[s] == StackInterrupted(...) && ...)
– Boogie/Z3
proofs
become Coq
|| (StackState[s]
== StackEmpty
&&axioms
...)
|| (!isStack(s));
– (Try
to!) prove invariant holds after each step
implementation YieldTo(s:int, ...)
{
if (ecx >= ?NumStacks) { ... call debugBreak(); }
...
}
• We’re not done yet, but we’ve found spec bugs
27/28
Conclusions
Every x86 instruction checked for safety!
Automated tools: checking scales to large code.
Open challenges
– Complete, foundational TAL/runtime/OS
– Concurrency, multicore
– GPUs
28/28
Descargar

Typed Assembly Language from an Optimizing Compiler