Incremental Path Towards a Safe OS Kernel

https://www.youtube.com/watch?v=a6-ZCUG3IVw

• Recent progress towards kernel safety

  • 

• How can we make incremental progress towards a safer Linux?

• Linux vulnerabilities

  • Increasing number of vulnerabilities each year

  • Each stable components contain many latent bugs

• Steps towards a safer OS kernel

  • Approach: incremental benefit for incremental work, improve safety on a module by module basis

    • Modulization

      • Enable incremental development and replacement of kernel modules

      • Necessary

        • Define abstract, implementation-independent interfaces

        • Develop tools to identify interfaces and automate the process

        • Anticipate and mitigate potential performance costs

    • Type safety

      • Redesign interfaces to eliminate type errors and unsafe casting

    • Ownership safety

      • Prevent memory errors and data races without compromising performance

    • Functional correctness

      • Remove semantic bugs through module-by-module specifications and proofs