Hyperkernel =========== Paper: "Hyperkernel: push-button verification of an OS kernel" Nelson et al. SOSP 2017 Source code: https://github.com/locore/hv6/ why this paper? Kernel is in TCB for secure systems Bugs in kernel can be expensive How to prove a kernel correct? Challenging: previous successes are labor intensive Hyperkernel: push-button verified kernel Goal: verify kernel Isolation between processes But, allow processes to share a CPU and memory Isolation between processes and kernel Don't allow processes to perform privileged instructions Bugs in kernel can break isolation One process can read/write other process's memory A process may achieve full control over machine Such bugs happen in practice Push-button verification No lines of proof: just source code and spec Powerful: easy to re-check code after making a change Requires careful design System design Code implementation Spec design Verifier design Previous work seL4 and CertiKOS used proof assistants (Isabelle, Coq) substantial amount of proof effort can you use SMT to reduce proof effort? Hyperkernel: kernel design for push-button verification xv6 functionality exokernel-type kernel interface theorems proven with Z3 including an isolation theorem a process can only read/write its own memory limits: single core no I/O concurrency (but able to model DMA) Challenges: standard kernel interface are not amenable to SMT fork, exec, etc. standard VM designs are not amenable to SMTs kernel and user space share address space VM mapping isn't injective kernel can change mapping C is ill defined Key ideas Kernel interfaces are "finite" kernel has no unbounded loops and recursion move "infinite" kernel code to user space wo breaking isolation Kernel has its own address space exploit HW virtualization support kernel runs in host mode user processes in guest mode in ring 0 with "kernel" privileges Implementation verified at LLVM IR LLVM IR better defined semantics than C Verification approach figure 2 state-machine verification (as in the labs) augmented with declarative specifications capture global invariants not necessary for proving implementation meets state-machine spec more confidence that state-machine spec is correct How to formulate state-machine verification for SMT? A Z3 expression for spec transition Python specs using symbolic values A Z3 expression for code transition LLVM IR semantics using symbolic values A Z3 expression for abstraction function Connects symbolic values of spec and impl How to prove state-machine theorems? Code and spec make same transitions Spec makes a transition on spec symbolic state See spec_dup example Code makes a transition on code symbolic state current pid an array of struct proc an array of file descriptors an array of struct file Rep invariant for kernel data structures that is verified for each code transition Ask Z3 if there is an example for which spec and code states are not equivalent Counter example -> bug No counter example -> proof State-machine transitions in spec and code in lock step Implications Single core I/O is an explicit step (executed after another step finishes) DMA modeled by a separate region of memory volatile: read can return any value How to prove declarative specs? Write Z3 expressions over spec state if fd's refcount for file f is 0 -> no fd refers to f Check if Z3 expression holds after each transition assuming it held beforehand Ask Z3 for counter examples Write declartive specs in a away that Z3 can solve them Don't say: forall o,o' own(o) = own(o') => o = o' to capture uniques if pages owned by p is same set as owned by p' -> p = p' Observation: because unique, there is an inverse function owned-by spec writer must provide inverse function Hyperkernel design Use HW virtualization for separate address spaces kernel runs with host privileges (virtual machine monitor) User processes as guest in ring 0 (!) Allows access to IDT Exceptions can be delivered to user space directly Kernel isn't involved (less code to verify) Explicit resource management User space specifies which resource it wants Kernel only checks (no search) Reclaimation is also explicit Typed pages page-table page, a page frame, a stack page fine-grained virtual memory sys calls Process creation 3 pages machine control structure page table root exclusively owned by p stack page fork and exec in user space caller of fork can prepopulate the child's page table new proc provides *isolation* https://github.com/locore/hv6/blob/master/hv6/spec/kernel/spec/top.py#L267 the root page is owned by exclusively by p all writeable pages are owned by p Link lists are not verified, but checked free list and ready list but used in verified way File system and network server in user space Unverified, but *isolated* IPC implemented using virtual memory pages sender sends page to receiver kernel atomically switches page from sender to user Could run Yggdrasil or FSCQ Linux emulation Easy because user code runs in ring 0 (guest) Checkers for initialization and glue code Summary Clever design for a kernel so that SMT can verify it Finite interfaces Separate address space for kernel and processes LLVM IR Many cool tricks (e.g., user code in ring 0, linked list use, ...) Main property: isolation Many kernel functions moved to user space These kernel function are unverified BUT, each user process is isolated Answer to reading question: