Operating systems

[Google Scholar] [Wikipedia]


NOVA hypervisor, Serval solver-based verifier

  • Automated verification of a small hypervisor [alkassar:vstte:2010]
  • A high assurance virtualization platform for ARMv8 [baumann:eucnc:2016]
  • Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor [becker:fm:2016]
  • A structured TCP in Standard ML [biagioni:sigcomm:1994]
  • A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C [blanchard:fmics:2015]
  • Theseus: A state spill-free operating system [boos:plos:2017]
  • Local verification of global invariants in concurrent programs [cohen:cav:2010]
  • Machine code verification of a tiny ARM hypervisor [dam:ted:2013]
  • Machine code verification of a tiny ARM hypervisor [dam:trusted:2013]
  • Using continuations to implement thread management and communication in operating systems [draves:sosp:1991]
  • Aspect weaving as component knitting: Separating concerns with Knit [eide:aspse:2001]
  • Static and dynamic structure in design patterns [eide:icse:2002]
  • Microkernels meet recursive virtual machines [ford:sosp:1996]
  • The Flux OSKit: A substrate for kernel and language research [ford:sosp:1997]
  • 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]
  • Interposition agents: transparently interposing user code at the system interface [jones:sosp:1993]
  • SeL4: Formal verification of an OS kernel [klein:sosp:2009]
  • On the duality of operating system structures [lauer:osr:1979]
  • Verifying the Microsoft Hyper-V hypervisor with VCC [leinenbach:fm:2009]
  • The case for writing a kernel in Rust [levy:apsys:2017]
  • Ownership is theft: Experiences building an embedded OS in Rust [levy:plos:2015]
  • Multiprogramming a 64kB computer safely and efficiently [levy:sosp:2017]
  • A secure and formally verified Linux KVM hypervisor [li:sandp:2021]
  • Formally verified memory protection for a commodity multiprocessor hypervisor [li:usenix:2021]
  • VMSL: A separation logic for mechanised robust safety of virtual machines communicating above FF-A [liu:pldi:2023]
  • Vx86: x86 assembler simulated in C powered by automated theorem proving [maus:amast:2008]
  • Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
  • Lock inference for systems software [regehr:acp4is:2003]
  • Evolving real-time systems using hierarchical scheduling and concurrency analysis [regehr:rtss:2003]
  • Knit: Component composition for systems software [reid:osdi:2000]
  • Integrated semantics of intermediate-language C and macro-assembler for pervasive formal verification of operating systems and hypervisors from VerisoftXT [schmaltz:vstte:2012]
  • SecVisor: A tiny hypervisor to provide lifetime kernel code integrity for commodity OSes [seshadri:sosp:2007]
  • Translation validation for a verified OS kernel [sewell:pldi:2013]
  • Program verification in the presence of cached address translation [syeda:itp:2018]
  • Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware [tao:sosp:2021]
  • Design, implementation and verification of an extensible and modular hypervisor framework [vasudevan:secpriv:2013]
  • überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]