Memory and Type Safety in System Design
Explore the concept of ensuring memory and type safety in system design, featuring safe systems, verified code, hardware specifications, and end-to-end safety measures. Learn about Verve, a type-safe OS, and the Verve Nucleus designed for partial correctness and safety verification at the hardware level.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Safe to the Last Instruction: Jean Yang MIT CSAIL Chris Hawblitzel Microsoft Research
Safe to the Last Instruction: Jean Yang MIT CSAIL Chris Hawblitzel Microsoft Research
Memory Safety Safe to the Last Instruction / Jean Yang 5
Type Safety Safe to the Last Instruction / Jean Yang 6
Previously: Safe Systems Type-checked OS Applications File System Drivers Microkernel What currently exists Untyped Unsafe code (GC, stacks, drivers, ) Hardware Safe to the Last Instruction / Jean Yang 7
End-to-End Safe Systems Type-checked OS Applications File System Drivers Microkernel What we want Untyped Unsafe code (GC, stacks, drivers, ) (GC, stacks, drivers, ) Verified code Hardware Safe to the Last Instruction / Jean Yang 8
Verve, a Type-Safe OS Verify partial correctness of low- level Nucleus using Hoare logic based on a hardware spec. Verify an interface to typed assembly for end-to-end safety. Applications Type-checked File System Drivers Microkernel Interface specification Verified Nucleus Hardware specification Safe to the Last Instruction / Jean Yang 9
The Verve Nucleus Applications Interface specification Interface specification Type-checked Verified File System Drivers Interrupt table Microkernel GC Heap Interrupt/error handling Interface specification Allocator and GC [POPL 2009] Stacks Verified x86 instructions Memory bounds Nucleus Devices Hardware specification Safe to the Last Instruction / Jean Yang 10
Thread Context Invariant function StateInv (s:StackID, state:StackState, ) returns(bool) { (!IsEmpty(state) && (IsInterrupted(state) && (IsYielded(state) && state == StackYielded( StackEbp(s, tMems) , StackEsp(s, tMems) + 4 , StackRA(s, tMems, fMems)) && } Safe to the Last Instruction / Jean Yang 11
Load Specification procedureLoad(ptr:int) returns(val:int); requiresmemAddr(ptr); requiresAligned(ptr); modifies Eip; ensuresword(val); ensuresval == Mem[ptr]; Safe to the Last Instruction / Jean Yang 12
Assembling Verve Source file Verification tool Compilation tool Verified Nucleus.bpl (x86) Boogie/Z3 Translator/ Assembler Safe to the Last Instruction / Jean Yang 13
Boogie to x86 implementation ReadKeyboard(){ call KeyboardStatusIn8(); call eax := And(eax, 1); if (eax != 0) { goto proc; } call eax := mov(256); return; proc: call KeyboardDataIn8(); call eax := And(eax, 255); return; } ReadKeyboard proc in al, 064h and eax, 1 cmp eax, 0 jne ReadKeyboard$proc mov eax, 256 ret ReadKeyboard$skip: in al, 060h and eax, 255 ret Safe to the Last Instruction / Jean Yang 14
Building Verve Source file Verification tool Kernel.cs Compilation tool C# compiler Verified Nucleus.bpl (x86) Kernel.obj (x86) Boogie/Z3 TAL checker Translator/ Assembler Linker/ISO generator Verve.iso Safe to the Last Instruction / Jean Yang 15
Verve Performance Verve Cycles Comparisons Cycles functionality Round-trip L4 (IPC) 224 98 yield SeL4 (IPC) 448 Round-trip wait + signal 216 Singularity (yield) 2156 Linux (yield) 2390 Windows (yield) 3554 Safe to the Last Instruction / Jean Yang 16
Low Annotation Burden Copying Mark-sweep 1185 4309 Specification Boogie lines Verified Boogie lines 4854 3x code x86 instructions 1377 1489 9 person-months Safe to the Last Instruction / Jean Yang 17
Verve vs. SeL4? Applications File System Drivers 120-240 person-months SeL4 Verified microkernel C# kernel Verve 8,700 lines of C Verified Nucleus ~1500 lines of x86 ~600 lines ARM assembly 200,000 lines of Isabelle 20x code Safe to the Last Instruction / Jean Yang 18
Contributions First automatically, mechanically verified OSfor type safety. Real system running on x86 with efficient code. Approach for using automated techniques to verify safety. Applications Type-checked File System Drivers Microkernel Interface specification Verified Verified nucleus Hardware specification http://www.codeplex.com/singularity Safe to the Last Instruction / Jean Yang 19
