BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Executable Specification of a Production Hypervisor - Kayvan Memar
 ian (University of Cambridge)
DTSTART:20250602T123000Z
DTEND:20250602T133000Z
UID:TALK232945@talks.cam.ac.uk
CONTACT:Dr Meven Lennon-Bertrand
DESCRIPTION:Developing systems code that robustly provides its intended se
 curity guarantees remains very challenging: conventional practice does not
  suffice\, and full functional verification\, while now feasible in some c
 ontexts\, has substantial barriers to entry and use.\n\nIn this work\, we 
 explore an alternative\, more lightweight approach to building confidence 
 for a production hypervisor: the pKVM hypervisor developed by Google to pr
 otect virtual machines and the Android kernel from each other.  The basic 
 approach is very simple and dates back to the 1970s: we specify the desire
 d behaviour in a way that can be used as a test oracle\, and check corresp
 ondence between that and the implementation at runtime.  The setting makes
  that challenging in several ways: the implementation and specification ar
 e intertwined with the underlying architecture\; the hypervisor is highly 
 concurrent\; the specification has to be loose in certain ways\; the hyper
 visor runs bare-metal in a privileged exception level\; naive random testi
 ng would quickly crash the whole system\; and the hypervisor is written in
  C using conventional methods. We show how all of these can be overcome to
  make a practically useful specification\, finding a number of critical bu
 gs in pKVM along the way. \n\nThis is not at all what conventional develop
 ers (nor what formal verifiers) normally do -- but we argue that\, with th
 e appropriate mindset\, they easily could and should.\n
LOCATION:FW26\, Computer Laboratory
END:VEVENT
END:VCALENDAR