25 ExoKernel/seL4 Kernel

1 . Today’s Papers EECS 262a • Exokernel: An Operating System Architecture for Application-Level Resource Management, Dawson R. Engler, M. Frans Kaashoek, and James Advanced Topics in Computer Systems O’Toole Jr. Appeared in Proceedings of the ACM Symposium on Operating Lecture 25 Systems Principles, 2005 • seL4: Formal Verification of an OS Kernel, Gerwin Klein, Kevin ExoKernel/seL4 Kernel Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, November 27th, 2018 Thomas Sewell, Harvey Tuch, Simon Winwood. Appeared in Proceedings of the ACM Symposium on Operating Systems Principles, 2009 John Kubiatowicz (With slides from Ion Stoica and Ali Ghodsi) • Thoughts? Electrical Engineering and Computer Sciences University of California, Berkeley http://www.eecs.berkeley.edu/~kubitron/cs262 11/27/2018 cs262a-F18 Lecture-25 2 The Rise of Microkernels! Traditional OS services: Figure ©Wikipedia Management and Protection Microkernel • Provides a set of abstractions Monolithic Kernel – Processes, Threads, Virtual Memory, Files, IPC – APIs, e.g.,: POSIX • Resource Allocation and Management • Moves as much from the kernel into “user” space – Small core OS running at kernel level – OS Services built from many independent user-level processes • Protection and Security – Communication between modules with message passing • Benefits: – Concurrent execution – Easier to extend a microkernel – Easier to port OS to new architectures – More reliable (less code is running in kernel mode) – Fault Isolation (parts of kernel protected from other parts) 4 – More secure • Detriments: – Performance overhead severe for naïve implementation 11/27/2018 cs262a-F18 Lecture-25 3 11/27/2018 cs262a-F18 Lecture-25 4 

2 . On the cost of micro-kernels: Abstractions • What is an abstraction? Generalization – Often an API in CS. Hides implementation details. • What are the advantages of abstractions? – Simpler. Easy to understand and use. Just follow the contract. How we fight complexity. – Standardization. Many implementations all satisfy the abstraction. Loose coupling, e.g. Unix’ everything is a file, many implementations and all apps benefit from this standardization. • What are the disadvantages of abstractions? – Contract is a compromise. Least common denominator. Not perfect for • Above: Ultrix (TAN) vs Mach (Reddish-brown) each use case • Cost of external pagers: page fault of first-generation microkernels – Performance often suffers (if you only could tweak an implementation took up to 1000µs! detail of a particular implementation) • See optional paper “Toward Real Microkernels” by Leidtke – Can create bloated software. • After many iterations, L4 became a “best-in-class” microkernel – Fast IPC – Better resource control than simple pagers (“Address Space Managers”) – Other optimizations 11/27/2018 cs262a-F18 Lecture-25 5 11/27/2018 cs262a-F18 Lecture-25 6 Context for These Papers (1990s) Challenge: “Fixed” Interfaces • Windows was dominating the market • Both papers identify “fixed interfaces” provided by existing – Mac OS downward trend (few percents) OSes as main challenge – Unix market highly fragmented (few percents) – Fixed interfaces provide protection but hurt performance and functionality • OS research limited impact • Exokernel: – “Fixed high-level abstractions hurt application performance because there is – Vast majority of OSes proprietary no single way to abstract physical resources or to implement an abstraction – “Is OS research dead?”, popular panel topic at that is best for all applications.” systems conferences of the era – “Fixed high-level abstractions limit the functionality of applications, because they are the only available interface between applications and hardware resources” • An effort to reboot the OS research, in particular, and OS architecture, in general 11/27/2018 cs262a-F18 Lecture-25 7 11/27/2018 cs262a-F18 Lecture-25 8 

3 . Challenge: “Fixed” Interfaces Problems in existing OSes • Both papers identify “fixed interfaces” provided by existing • Extensibility OSes as main challenge – Abstractions overly general – Fixed interfaces provide protection but hurt performance and functionality – Apps cannot dictate management – Implementations are fixed • SPIN: • Performance – “Existing operating systems provide fixed interfaces and implementations to – Context switching expensive system services and resources. This makes them inappropriate for – Generalizations and hiding information affect performance applications whose resource demands and usage patterns are poorly matched by the services provided.” • Protection and Management offered with loss in Extensibility and Performance 11/27/2018 cs262a-F18 Lecture-25 9 11/27/2018 cs262a-F18 Lecture-25 10 Symptoms Examples Illustrating need for App Control • Very few of innovations making into commercial OSes • Databases know better than the OS what pages they will – E.g., scheduler activations, efficient IPC, new virtual memory policies, … access – Can prefetch pages, LRU hurts their performance, why? • Applications struggling to get better performances – They knew better how to manage resources, and the OS was “standing” in the way 11/27/2018 cs262a-F18 Lecture-25 11 11/27/2018 cs262a-F18 Lecture-25 12 

4 . Two Papers, Two Approaches Exokernel • Exokernel: • A nice illustration of the end-to-end argument: – Very minimalist kernel, most functionality implemented in user space – ``general-purpose implementations of abstractions force applications that do not need a given feature to pay substantial overhead costs.’’ – Assumed many apps have widely different requirements, maximal extensibility – In fact the paper is explicitly invoking it (sec 2.2)! • Corollary: • SPIN: – Kernel just safely exposes resources to apps – Dynamically link extensions into the kernel – Apps implement everything else, e.g., interfaces/APIs, resource allocation – Rely on programming language features, e.g. static typechecking pollcies – Assumed device drivers need flexibility, so focused on how to enable them while staying protected 11/27/2018 cs262a-F18 Lecture-25 13 11/27/2018 cs262a-F18 Lecture-25 14 OS Component Layout Exokernel Main Ideas • Kernel: resource sharing, not policies • Library Operating System: responsible for the abstractions – IPC – VM – Scheduling – Networking Exokernel 11/27/2018 cs262a-F18 Lecture-25 15 11/27/2018 cs262a-F18 Lecture-25 16 

5 . Lib OS and the Exokernel Philosophy • Lib OS (untrusted) can implement traditional OS • “An exokernel should avoid resource management. It should only manage resources to the extent required by abstractions (compatibility) protection (i.e., management of allocation, revocation, and ownership).” • Efficient (LibOS in user space) • The motivation for this principle is our belief that distributed, application-specific, resource management is • Apps link with LibOS of their choice the best way to build efficient flexible systems. • Kernel allows LibOS to manage resources, protects LibOSes 11/27/2018 cs262a-F18 Lecture-25 17 11/27/2018 cs262a-F18 Lecture-25 18 Exokernel design • Securely expose hardware – Decouple authorization from use of resources – Authorization at bind time (i.e., granting access to resource) ABSTRACTIONS – Only access checks when using resource ABSTRACTIONS – E.g., LibOS loads TLB on TLB fault, and then uses it multiple times • Expose allocation – Allow LibOSes to request specific physical resources – Not implicit allocation; LibOS should participate in every allocation decision 11/27/2018 cs262a-F18 Lecture-25 19 11/27/2018 cs262a-F18 Lecture-25 20 

6 . Exokernel design Example: Memory • Expose names (CS trick #1-1) – Remove one level of indirection and expose useful attributes Self-authenticated » E.g., index in direct mapped caches identify physical pages • Guard TLB loads and DMA capability conflicting – Secure binding: using self-authenticating capabilities – Additionally, expose bookkeeping data structures » For each page Exokernel creates a random value, check » E.g., freelist, disk arm position (?), TLB entries » Exokernel records: {Page, Read/Write Rights, MAC(check, Rights)} – When accessing page, owner need to present capability • Expose revocation – Page owner can change capabilities associated and deallocate it – “Polite” and then forcibly abort • Large Software TLB (why?) – TLB of that time small, LibOS can manage a much bigger TLB in software – Expensive checks during page fault can be reduced with a larger TLB 11/27/2018 cs262a-F18 Lecture-25 21 11/27/2018 cs262a-F18 Lecture-25 22 Example: Processor Sharing Example: Network • Downloadable filters • Process time represented as linear vector of time slices • Application-specific Safe Handlers (ASHes) – Round robin allocation of slices – Can reply directly to traffic, e.g., can implement new transport protocols; dramatically reduce • Secure binding: allocate slices to LibOSes – Simple, powerful technique: donate time slice to a particular process • Secure biding happens at download time – A LibOS can donate unused time slices to its process of choice • If process takes excessive time, it is killed (revocation) 11/27/2018 cs262a-F18 Lecture-25 23 11/27/2018 cs262a-F18 Lecture-25 24 

7 . Is this a good paper? Final Project Timing • What were the authors’ goals? • Final abstract/project proposal on the WEBSITE • What about the evaluation/metrics? – Please update your project description and proposal before next week • Did they convince you that this was a good • Poster Session: system/approach? – Next Friday (12/7) from 9:00-12:00 in 5th-floor atrium – Everyone must be setup by 9:30 – if you are late, you may not get a • Were there any red-flags? chance to have your poster reviewed • What mistakes did they make? – Plan on staying whole time, but might be shorter – Who needs posters printed??? • Does the system/approach meet the “Test of Time” challenge? • Final paper: – Due Monday 12/10 @ AOE (by 5am) • How would you review this paper today? – 10 pages, 2- column, conference format – Must have a related work section! – Also, plan on a future work and/or discussion section – Make sure that your METRICs of success are clear and available 11/27/2018 cs262a-F18 Lecture-25 25 11/27/2018 cs262a-F18 Lecture-25 26 L4 MicroKernel Layers of Proof Techniques • Original L4 kernel: Jochen Liedtke – Derived from L3 kernel • Results (including follow-on results) – Developed at GMD (Germany) – Functional correctness verification in Isabelle/HOL framework – Designed to have fast IPC, better memory management, – Functional correctness for hand-optimized IPC • Picked up in several commercial usages – Correctness of access-control enforcement – Automatic poof of refinement between compiled binary and C implementation – Automatic static analysis of worst-case execution time for sys calls 11/27/2018 cs262a-F18 Lecture-25 27 11/27/2018 cs262a-F18 Lecture-25 28 

8 . In a nutshell Three Implementations • Abstract Specification: Isabelle/HOL code – Describes what system does without saying how it is done – Written as series of assertions about what should be true • Executable Specification: Haskel – Fill in details left open at abstract level – Specify how the kernel works (as opposed to what I does) – Deterministic execution (except for underlying machine) – Data structures have explicit data types – Controlled subset of Haskel • The Detailed Implementation: C – Translation from C into Isabelle requires controlled subset of C99 • Apply automatic techniques for “proof” of correctness » No address-of operator & on local (stack) variables – Series of refinements from Abstract Specification  Executable » Only 1 function call in expressions or need proof of side-effect freedom Specification  C implementation » No function calls through pointers – Utilized Isabelle/HOL theorem prover » No goto, switch statements with fall-through • Three different implementations • Machine model: need model of how hardware behaves – Spanning “obvious to humans” and “efficient” 11/27/2018 cs262a-F18 Lecture-25 29 11/27/2018 cs262a-F18 Lecture-25 30 Example: Scheduling Challenges • Smaller Kernel  Increased Interdependence of components – Radical size reduction in microkernel leads to high degree of dependence of remaining components – Proof techniques still possible • Design special versions of each • Figure 3: Isabell/High- of the languages order logic (HOL) • Design multiple implementations code for scheduler at each in different languages abstract level • Huge number of invariants is moving from Abstract specification to Executable specification – Low-level memory invariants – Typing invariants • Figure 4: Haskell Code for Scheduler – Data structure Invariants – Algorithmic Invariants 11/27/2018 cs262a-F18 Lecture-25 31 11/27/2018 cs262a-F18 Lecture-25 32 

9 . Experience and Lessons Learned Is this a good paper? • Performance • What were the authors’ goals? – Optimized IPC path is well performing (via micro-benchmarks) – Other performance not characterized in this paper • What about the evaluation/metrics? • Verification effort: extremely high! • Did they convince you that this was a good – Three phases, each with non-trivial effort system/approach? – Overall size of proof (including automatically generated proofs): • Were there any red-flags? 200,000 lines of Isabelle script – Abstract Spec: 4 person months (4 pm) • What mistakes did they make? – Haskell prototype: 2 person years (2 py) • Does the system/approach meet the “Test of Time” – Executable spec translated from Haskel prototype: 3 pm challenge? – Initial C translation+implementation: 2pm – Cost of the proof: 20py (seL4 specific, 11py) • How would you review this paper today? • What about future: 8py for new kernel from scratch! • Cost of change – Simple or independent small features not huge, say 1 person week – Cost to add new features can be very large: up to 2py! 11/27/2018 cs262a-F18 Lecture-25 33 11/27/2018 cs262a-F18 Lecture-25 34