Operating Systems
Summarised papers
- Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor [becker:fm:2016]
- Local verification of global invariants in concurrent programs [cohen:cav:2010]
- End-to-end verification of information flow security for C and assembly programs [costanzo:pldi:2016]
- Komodo: Using verification to disentangle secure-enclave hardware from software [ferraiuolo:sosp:2017]
- Attacking, repairing, and verifying SecVisor: A retrospective on the security of a hypervisor [franklin:cmu:2008]
- CertiKOS: An extensible architecture for building certified concurrent OS Kernels [gu:osdi:2016]
- The case for writing a kernel in Rust [levy:apsys:2017]
- Verifying security invariants in ExpressOS [mai:asplos:2013]
- Formal verification of a memory allocation module of Contiki with Frama-C: a case study [mangano:crisis:2016]
- seL4: from general purpose to a proof of information flow enforcement [murray:secpriv:2013]
- Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
- Sound formal verification of Linux's USB BP keyboard driver [penninckx:nfm:2012]
- SecVisor: A tiny hypervisor to provide lifetime kernel code integrity for commodity OSes [seshadri:sosp:2007]
- The Flask security architecture: System support for diverse security policies [spencer:security:1999]
- Scalable translation validation of unverified legacy OS code [tahat:fmcad:2019]
- überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]
Unsummarised papers
- Automated verification of a small hypervisor [alkassar:vstte:2010]
- Verification of TLB virtualization implemented in C [alkassar:vstte:2012]
- Cogent: Verifying high-assurance file system implementations [amani:asplos:2016]
- System programming in Rust: Beyond safety [balasubramanium:hotos:2017]
- A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C [blanchard:fmics:2015]
- The last mile: An empirical study of timing channels on seL4 [cock:ccs:2014]
- Unifying type checking and property checking for low-level code [condit:popl:2009]
- Model checking boot code from AWS data centers [cook:cav:2018]
- Machine code verification of a tiny ARM hypervisor [dam:trusted:2013]
- Labels and event processes in the Asbestos operating system [efstathopoulos:sosp:2005]
- Ironclad apps: End-to-end security via automated full-system verification [hawblitzel:osdi:2014]
- The VFiasco approach for a verified operating system [hohmuth:plos:2005]
- Applying source-code verification to a microkernel: the VFiasco project [hohmuth:sigops:2002]
- SeL4: Formal verification of an OS kernel [klein:sosp:2009]
- Information flow control for standard OS abstractions [krohn:sosp:2007]
- Ownership is theft: Experiences building an embedded OS in Rust [levy:plos:2015]
- Implementing an untrusted operating system on trusted hardware [lie:sosp:2003]
- RedLeaf: Towards an operating system for safe and verified firmware [narayanan:hotos:2019]
- Hyperkernel: Push-button verification of an OS kernel [nelson:sosp:2017]
- Virtualization: Issues, security threats, and solutions [pearce:compsurv:2013]
- Push-button verification of file systems via crash refinement [sigurbjarnarson:osdi:2016]
- Nickel: A framework for design and verification of information flow control systems [sigurbjarnarson:osdi:2018]
- Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security [tiwari:isca:2011]
- Design, implementation and verification of an extensible and modular hypervisor framework [vasudevan:secpriv:2013]
- Safe to the last instruction: automated verification of a type-safe operating system [yang:pldi:2010]
- Making information flow explicit in HiStar [zeldovich:osdi:2006]
Information Flow
- Nickel: A Framework for Design and Verification of Information Flow Control Systems
- Labels and Event Processes in the Asbestos Operating System
- Making Information Flow Explicit in HiStar
- The Flask Security Architecture: System Support for Diverse Security Policies
- Flume: Information Flow Control for Standard OS Abstractions
- seL4: from general purpose to a proof of information flow enforcement