RedLeaf: Isolation and Communication in a Safe Operating System

• Paper
• Slides

Contribution

Rv6: a POSIX-subset OS.

A language-based isolation domain mechanism which:

• can be dynamically loaded and cleanly terminated
• is zero-copy, fault isolation & transparent recovery of device drivers

IDL (in some way a prototype of Fuchsia’s FIDL)

• Compilation rather than runtime

Background

About OS

• Monolithic OS’ inability to provide fine-grained isolation.
• Hardware-supported mechanisms have unacceptable overhead.
  1. CODOMs: Protecting software with Code-centric memory Domains
  2. The CHERI capability model: Revisiting RISC in an age of risk
• Traditional safe languages requires a managed runtime.
  • The fastest GC is 20%-50% slower than C on typical network driver according to The Case for Writing Network Drivers in High-Level Programming Languages

About Rust

• The only runtime overhead of Rust is bound checking that can be concealed by Out-of-Order of modern computer.
• Language safety alone cannot guarantee fault-isolation and termination of untrusted subsystems.
• A mechanism isolates faults: terminate a faulting or misbehaving computation and leave the system in a clean state.
  • deallocate all previously-used resources
  • preserve the objects that has been passed through communication channels
  • future invocations are prohibited

Trust Base

• Rust compiler
• Rust core libraries
• Non-malicious devices (can be spared by IOMMU)

Implementation

Core Ideas

• Heap isolation
  • private and shared heap
  • memory allocation on the domain heap
• Exchangeable types
• Ownership tracking
  • RRef<T>
• Interface validation:
• Cross-domain call proxying
  • based on IDL compiler
  • static analysis on AST of interfaces

Others

• Dynamic Domain Loading
• Safe Device Drivers
  • non-priviledged domains
• Device Driver Recovery
  • transparent device driver recovery with shadow drivers

Evaluation

• Competiable versus traditional hardware mechanisms on cross-domain calls
  • seL4: 834 cycles
  • VMFUNC: 169 cycles
  • VMFUNC-based call/reply: 396 cycles
  • RedLeaf…: 124-297 cycles
• Efficient Device Drivers with improved security
• Real-world applications
  • Maglev: <40% overhead
  • KV Store: 61%-86% of performance of C implementation
  • Nginx: 2x improvement compared with Linux-based server

Insights

• How to evaluate a secure operating system? … & fault isolation.
• From language safety to system safety: more isolation features.
• Related works: J-Kernel, Kaffee OS, Singularity OS …