seL4

References:

  • About seL4
  • seL4 Documentation
  • Klein, Gerwin, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe et al. “seL4: Formal verification of an OS kernel.” In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP), pp. 207-220. 2009.
  • Murray, Toby, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. “seL4: from general purpose to a proof of information flow enforcement.” In 2013 IEEE Symposium on Security and Privacy, pp. 415-429. IEEE, 2013.
  • Sewell, Thomas Arthur Leck, Magnus O. Myreen, and Gerwin Klein. “Translation validation for a verified OS kernel.” In Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation, pp. 471-482. 2013.
  • Trustworthy Systems Paper Publication

Source codes data:

  • 8700 lines of C code and 600 lines of assembler; ( – 2009 sosp paper)
    • Initially for ARMv6-based platform, with a subsequent port of the kernel to x86;
  • around 9500 lines of C source code; 11736 instructions on the (x86) binary level; – (2013-translation validation paper)

Motivation

“Complete formal verification is the only known way to guarantee that a system is free of programming errors.”

“absence of bugs”

  • “General wisdom has it that bugs in any sizable code base are inevitable. As a consequence, when security or reliability is paramount, the usual approach is to reduce the amount of privileged code, in order to minimize the exposure to bugs.”
    • Security kernels, separation kernels [38,54];
    • MILS approach [4];
    • microkernels [1,12,35,45,57,71];
    • isolation kernels [69];
    • small hypervisors [16,26,56,59];
    • Common Criteria [66] at the strictest evaluation level requires the system under evaluation to have a “simple” design;

seL4 overview

Third generation microkernel, based on L4 [46], influenced by EROS [58];

Features abstractions for virtual address spaces, threads, inter-process communication (IPC);

  • Virtual address spaces have no kernel-defined structure;
  • Page table faults are propagated via IPC to pager threads;
    • pager threads: responsible for mapping frames into virtual addr space;

  • Exceptions and non-native system calls are also propagated via IPC

    • to support virtualization;

  • IPC:

    • synchronous and asynchronous endpoints: port-like destinations without in-kernel buffering;
    • for inter-thread communication;
    • with RPC facilitated via reply capabilities;

  • Capabilities:

    • segregated;
    • stored in capability address spaces;
    • capability container objects, CNodes;

  • Drivers: run as user-mode applications

    • registers and memory are controlled by
    • either by mapping the device to the virtual address space, or
    • by controlled access to device ports on x86 hardware;
    • Interrupts: via IPC
    • receive notification of interrupts
    • acknowledge their receipt

  • Explicit memory management:

    • capability-based explicit management
    • Guarantees all memory allocation in the kernel is explicit and authorised;
    • both in-kernel objects and virtual addr spaces;
    • Physical Memory: untyped capabilities –> retyped as:
    • kernel objects: thread control blocks, CNodes, endpoints
    • frames for mapping in virtual addr spaces

Unlike most L4 kernels, seL4 features capabilities for authorization;

Privilege Modes:

seL4 could run as an OS kernel (supervisor mode in RISC-V) or as a hypervisor (HS-mode in RISC-V, EL2 on ARM, Root Ring-0 on x86). – Whitepaper 20210610.

Verified Property

Functional correctness:

  • The implementation always strictly follows our high-level abstract specification of kernel behavior;
  • e.g., kernel will never crash;
  • e.g., kernel will never perform an unsafe operation;
  • e.g., predict precisely how the kernel will behave in every possible situation;

Worst-Case Execution Time (WCET):

  • Done for ARM v6 processors. “We did the WCET analysis of seL4 for Arm v6 processors. It has since fallen into abeyance, as Arm has stopped providing the required information on the worst-case latencies of instructions, and Intel never provided those of their architecture. However, with the advent of open-source RISC-V processors, we will be able to redo this analysis”

Assumptions

Correctness of:

  • compiler;
  • assembly code;
  • boot code;
  • management of caches;
  • the hardware.

Formal Methods in seL4

OS developers tend to take a bottom-up approach to kernel design. High performance is obtained by managing the hardware efficiently, which leads to designs motivated by low-level details. In contrast, formal methods practitioners tend toward top-down design, as proof tractability is determined by system complexity. This leads to designs based on simple models with a high degree of abstraction from hardware.

seL4 methodology: an intermediate target.

  • use Haskell to provide a programming language for OS developers;
  • provide an artefact that can be automatically translated into theorem proving tool and reasoned about.

sel4 design process

Square box: the formal artefacts;

Double arrows: represent impl. or proof effort;

Single arrows: represent design/impl. influence of artefacts on other artefacts;

Haskell prototype of the kernel: the Central Artefact:

  • (2009-sosp) Linked with software (derived from QEMU) that simulates the hardware platform;
    • normal user-level execution is enabled by the hardware simulator;
    • traps are passed to the kernel model which computes the result of the trap;
    • The prototype modifies the user-level state of the simulator to appear as if a real kernel had executed in privileged mode.
    • e.g., a subset of the Iguana embedded OS37 on the simulator-Haskell combination;

C prototype of the kernel: the final production kernel:

  • (2009-sosp) manually implemented in C;
    • for several reasons: Haskell runtime is hard to verify; Haskell GC not suitable for real-time environment;
    • similar strategy used in SPIN[7] and Singularity [23]

Formal Verification Technique

Use Isabelle/HOL

  • interactive, machine-assisted, and machine-checked proof.

Interactive theorem proving vs Automated verification methods:

Interactive theorem proving has the advantage that it is not constrained to specific properties or finite, feasible state spaces, unlike more automated methods of verification such as static analysis or model checking.

Refinement Proof: functional correctness in the strongest sense.

A refinement proof establishes a correspondence between a high-level (abstract) and a low-level (concrete, or refined) representation of a system.

Security properties: abstract model <==> refined model:

If a security property is proved in Hoare logic about the abstract model (not all security properties can be), refinement guarantees that the same property holds for the kernel source code.

SOSP 09 paper: functional correctness property + security of seL4’s access-control system in Isabelle/HOL;

To verify the function correctness:

  • its behavior is specified precisely, formally, at an abstract level;

  • its formal design is used to prove desirable properties, including termination and execution safety;

  • its implementation is formally proven to satisfy the specification;

Methodology of rapid kernel design and implementation:

Run seL4 on RISC-V machines

runs as supervisor-mode kernel on RISC-V platforms.

  • verifying the RISC-V port of seL4, with proof of functional correctness (to the binary) expected to complete in Q1’20.

  • Time protection with FPGA hardware prototype.

More

  • Camkes

    • References: camkes-tool/docs/ CAmkES More

  • Last Mile

    • References: The Last Mile: An empirical study of timing channels on seL4, Leakage in Trustworthy Systems, by David Cock, August 2014. Overview Side channel data collection. seL4 on Exynos4412 platform: Scope serverl timing channels on seL4 based system with their defenses with low overhead. Do not consider noise-adding solutions (due to their overhead); Only consider black box techniques (require no insight into the internals of software running on seL4, as retrofitting security into complex software is generally impossible);

  • 2019 Time Protection

    • References: The last mile Time Protection: The Missing OS Abstraction, Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. 2019. In Proceedings of the Fourteenth EuroSys Conference 2019 (Dresden, Germany) (EuroSys ’19). ACM, New York, NY, USA, Article 1, 17 pages. https://doi.org/10.1145/3302424.3303976; paper site “No security without time protection: We need a new hardware-software contract.”, Ge, Qian, Yuval Yarom, and Gernot Heiser. In Proceedings of the 9th Asia-Pacific Workshop on Systems, pp.

Created Mar 29, 2022 // Last Updated Dec 6, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?