[SOSP'73] The UNIX Time-Sharing System
['86] Mach: A New Kernel Foundation For UNIX Development
[USENIX Summer'90] Unix as an Application Program
[SOSP'91 TOSC'92] The Design and Implementation of a Log-Structured File System
[CompSystems'95] Plan 9 from Bell Labs
[USS'96] A secure environment for untrusted helper applications confining the Wily Hacker
[SOSP'97] The Flux OSKit: a substrate for kernel and language research
[SOSP'03] Improving the Reliability of Commodity Operating Systems
[EuroSys'06] Language Support for Fast and Reliable Message-based Communication in Singularity OS
[OSR'07] Singularity: Rethinking the Software Stack
[SOSP'09] seL4: Formal Verification of an OS Kernel
[PLDI'10] Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
[APSys'11] Linux kernel vulnerabilities: State-of-the-art defenses and open problems
[ASPLOS'15] Nested Kernel: An Operating System Architecture for Intra-Kernel Privilege Separation
[OSDI'16] CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels
[APSys'17] The Case for Writing a Kernel in Rust
[Oakland'18] Precise and Scalable Detection of Double-Fetch Bugs in OS Kernels
[OSDI'18] The benefits and costs of writing a POSIX kernel in a high-level language
[CCS'18] Check It Again: Detecting Lacking-Recheck Bugs in OS Kernels
[USS'19] Detecting Missing-Check Bugs via Semantic- and Context-Aware Criticalness and Constraints Inferences
[CPSNA'13] On-Chip Control Flow Integrity Check for Real Time Embedded Systems