> For the complete documentation index, see [llms.txt](https://sliu583.gitbook.io/blog/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://sliu583.gitbook.io/blog/specific-work/seminar-and-talk/fall-21-reading-list/incremental-path-towards-a-safe-os-kernel.md).

# Incremental Path Towards a Safe OS Kernel

* Recent progress towards kernel safety 
  * ![](/files/G7eEBPletbpMUPR7xmks)
* 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