• what: technical problem
• why: significance
• gap: limitations of sota
• how: solution. hard, ideally.

History of OSes §

• 1st period
  • libraries
• 1950s
  • batching system
  • magnetic tape, disk
• 1960s and '70s
  • advanced batching os
    • paging (Atlas, 1961)
    • multi-programming
      • virtualize cpu
      • virtualize memory
  • time-sharing os

Principles §

Sources of Complexity:

• emergent properties
• propagation of effects
• trade-offs
• incommensurate scaling

Dealing with complexity:

• modularity
• abstraction
• layering

• programmability
• efficiency
• isolation

Exokernel §

The defining tragedy of the operating system community has been the definition of an OS as a software that both multiplexes and abstracts physical resources.

poor {reliability,adaptability,performance,flexibility}

[…] hardware should provide primitives, not high-level abstractions.

exokernel implementation:

• library operating systems (LibOS)
• manage resources only to the extent that it’s necessary for protection

removing layers of abstraction

they don’t protect the page tables properly?

• large executables?
  • “shared (dl) libs”
• every application has its own interface?
  • “kernel architects anticipating every usecase sucks too”

Sel4 §

• design and implement a kernel using a top-down approach
• microkernel
  • smaller
  • modular
  • ipc
• assumes that the compiler and the hardware are correct
• design workflow
  • haskell prototype
  • qemu-based hardware simulator
  • formal executable spec
  • high-perf c implementation
• proof that the c impl is equivalent to the formal executable spec
• refinement proof
  • establishes a correspondence between a high-level and a low-level representation of a system
  • all transitions in one space must have a corresponding transition in the second space
  • transitive
• verification layers
  • abstract spec
    • isabelle/hol
    • description of what the system does
  • executable spec
    • artifact generated from the haskell prototype
  • proofs
    • verifying invariants
• proof achievements: kernel…
  • api calls terminate and return to user level
  • can never enter an infinite loop
  • will never crash due to a null/misaligned pointer access
  • does arg checking correctly and …
• limitations
  • no multiprocessor supported
  • limited concurrency support
• evaluations
  • biggest perf bottleneck for microkernels is usually ipc

Software Fault Isolation §

• e.g. native client in chromium
• confinement within a process
  • process space partitioned
  • fault domain: data, code, id
  • segments and seg ids
• safe and unsafe instructions
  • unsafe: int, syscall, reg-based jumps, indirect addressing
    • cannot be resolved statically
  • trap upon encountering unsafe instructions
    • runtime checks using extra instructions (overhead (small))
• address sandboxing
  • prevents module from accessing addresses outside its domain
• sfi vs address spaces
  • sfi: no domain switching, but l/s cost (+check cost)
    • constant cost
  • address spaces: high ctxt switch cost
• calls between fault domains
  • rpc
  • trusted stubs for pairs of fault domains
  • cheap: no traps or ctxt switches
• avoid cross-fault domain interference of system resources
  • let OS know where the fault domains are
  • […]
• performance
  • software isolation offers savings over native os services