Home · ASPLOS 2025 · Operating Systems & Virtualization
Will We Ever have Truly Secure Operating Systems?
Gernot Heiser
- Conference
- ASPLOS 2025
- Published
- 2025
- Pages
- 1-2
- Citations
- 0
The authors' abstract
This is the paper's own summary, in the paper's own words. It is dense on purpose — abstracts are written to compress.
Half a century after PSOS, the first attempts to prove an operating system (OS) secure, OS faults remain a major threat to computer systems security.A major step forward was the verification of the seL4 microkernel, the first proof of implementation correctness of an OS kernel.Over the next 4 years this proof was extended to the binary code, proofs of security enforcement, and sound and complete worst-case execution-time analysis.The proofs now cover 4 ISAs.I also discuss more speculative, early-stage work towards a provably secure, general-purpose OS.
The plain-English explainer is not written yet
When it is, it will replace the abstract above and walk through six questions in order: what problem the paper attacks, what people did before, why that was not good enough, what the paper's idea is, why that idea works, and what the measurements actually showed. Terms get defined the first time they appear.
Related papers on Operating Systems & Virtualization
- Pond: CXL-Based Memory Pooling Systems for Cloud Platforms 2023
- TPP: Transparent Page Placement for CXL-Enabled Tiered-Memory 2023
- IceBreaker: warming serverless functions better with heterogeneity 2022
- NeuPIMs: NPU-PIM Heterogeneous Acceleration for Batched LLM Inferencing 2024
- Clio: a hardware-software co-designed disaggregated memory system 2022