seL4 Formal Veri cation of an OS Kernel Gerwin Klein Kevin Elphinstone Gernot Heiser June Andronick Dhammika Elkaduwe Michael Norrish David Cock Kai Engelhardt Thomas Sewell Simon Winwood Philip Derrin Rafal Kolanski Harvey Tuch 1 microkernel 8 700 li nes of C 0 bugs qed conditions apply The Goal 2 The Problem 3 Small Kernels Small trustworthy foundation hypervisor microkernel nano kernel virtual machine separation kernel exokernel Untrusted Trusted Legacy AppsApp Legacy Sensitive App Legacy App High assurance components in presence of other components Trusted Service Linux Server seL4 API NICTA 2009 IPC Threads VM IRQ Hardware Capabilities 5 Small Kernels Small trustworthy foundation hypervisor microkernel nano kernel virtual machine separation kernel exokernel Untrusted Trusted Legacy AppsApp Legacy Sensitive App Legacy App High assurance components in presence of other components Trusted Service Linux Server seL4 API NICTA 2009 IPC Threads seL4 VM IRQ Hardware Capabilities 5 The Proof The Proof Functional Correctness Specification Proof Code NICTA 2009 7 Functional Correctness What Specification constdefs switch to idle thread unit s monad switch to idle thread do thread gets idle thread arch switch to idle thread modify s s cur thread thread od definition schedule unit s monad where schedule do threads allActiveTCBs thread select threads switch to thread thread od OR switch to idle thread end Proof 22 Code Threads and TCBs theory Tcb A imports CSpace A ArchVSpace A Schedule A Ipc dec begin constdefs set thread state obj ref thread state set thread state ref ts do tcb assert opt get get tcb ref set object ref TCB tcb tcb state ts od NICTA 2009 defs 7 Functional Correctness What Specification constdefs switch to idle thread unit s monad switch to idle thread do thread gets idle thread arch switch to idle thread modify s s cur thread thread od definition schedule unit s monad where schedule do threads allActiveTCBs thread select threads switch to thread thread od OR switch to idle thread end Proof 22 How Code Threads and TCBs theory Tcb A imports CSpace A ArchVSpace A Schedule A Ipc dec begin constdefs set thread state obj ref thread state set thread state ref ts do tcb assert opt get get tcb ref set object ref TCB tcb tcb state ts od NICTA 2009 defs 7 conditions apply Specification Proof Code NICTA 2009 8 conditions apply Specification Proof Code Assumptions NICTA 2009 8 conditions apply Expectation Specification Proof Code Assumptions NICTA 2009 8 conditions apply Assume correct Specification Proof Expectation compiler linker wrt C op sem assembly code 600 loc hardware ARMv6 cache and TLB management boot code 1 200 loc Code Assumptions NICTA 2009 8 Implications Execution always defined Specification no null pointer de reference no buffer overflows C Code no code injection no memory leaks out of kernel memory no div by zero no undefined shift no undefined execution no infinite loops recursion Not implied NICTA 2009 secure define secure zero bugs from expectation to physical world covert channel analysis 9 Proof Architecture Specification Proof C Code NICTA 2009 10 Proof Architecture Specification Design C Code NICTA 2009 11 Proof Architecture Specification Design C Code NICTA 2009 12 Proof Architecture Access Control Spec Confinement Specification Design C Code NICTA 2009 12 Proof Architecture Access Control Spec Confinement Specification Design Haskell Prototype C Code NICTA 2009 12 Proof Architecture Access Control Spec Specification arch switch to thread t modify s s cur thread t od constdefs switch to idle thread unit s monad switch to idle thread do thread gets idle thread arch switch to idle thread Confinement modify s s cur thread thread od definition schedule unit s monad where schedule do threads allActiveTCBs thread select threads switch to thread thread od OR switch to idle thread end Haskell Prototype Design 22 Threads and TCBs theory Tcb A imports CSpace A ArchVSpace A Schedule A Ipc decls A begin C Code NICTA 2009 constdefs set thread state obj ref thread state unit set thread state ref ts do 12 tcb assert opt get get tcb ref Proof Architecture Access Control Spec Confinement Specification Design Haskell Prototype C Code NICTA 2009 12 Proof Architecture Access Control Spec Confinement Specification Design Haskell Prototype C Code NICTA 2009 12 System Model States User Kernel Idle I Events Syscall Exception IRQ VM Fault idle event idle kernel exit K U event kernel mode NICTA 2009 13 System Model States User Kernel Idle I Events Syscall Exception IRQ VM Fault idle event idle kernel exit K U event kernel mode NICTA 2009 13 seL4 Kernel Design for Veri cation Kernel Design for Veri cation Two Teams Formal Methods Practitioners Kernel Developers NICTA 2009 16 Two Teams Formal Methods Practitioners Kernel Developers The Power of Abstraction Liskov 09 NICTA 2009 Exterminate All OS Abstractions Engler 95 16 Iterative Design and Formalisation Whiteboard Haskell Prototype Formal Design Formal Specification C Code NICTA 2009 17 Iterative Design and Formalisation Whiteboard Haskell Prototype Formal Design Formal Specification C Code NICTA 2009 17 Iterative Design and Formalisation Whiteboard Haskell Prototype Formal Design Formal Specification C Code NICTA 2009 18 Iterative Design and Formalisation Whiteboard Haskell Prototype Formal Design Formal Specification C Code NICTA 2009 18 Design for Verification Reducing Complexity Hardware drivers outside kernel Concurrency event based kernel limit preemption Code NICTA 2009 derive from functional representation 19 C subset Everything from C standard including data types structs padding pointers into structs precise finite integer arithmetic minus goto switch fall through reference to local variable side effects in expressions function pointers restricted unions plus compiler assumptions on NICTA 2009 pointers casts pointer arithmetic data layout encoding endianess 20 Did you find any Bugs Bugs found Effort during testing 16 during verification in C 160 in design 150 in spec 150 Haskell design 2 py First C impl 2 weeks Debugging Testing 2 months Kernel verification 12 py Formal frameworks 10 py Total 25 py Cost Common Criteria EAL6 L4 verified 87M 6M 460 bugs NICTA 2009 21 Did you find any Bugs Bugs found Effort during testing 16 during verification in C 160 in design 150 in spec 150 Haskell design 2 py First C impl 2 weeks Debugging Testing 2 months Kernel verification 12 py Formal frameworks 10 py Total 25 py Cost Common