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

Information Flow