Operating Systems

Summarised papers

  • 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]
  • 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]
  • The Flask security architecture: System support for diverse security policies [spencer:security:1999]
  • Scalable translation validation of unverified legacy OS code [tahat:fmcad:2019]

Unsummarised papers

Information Flow