Executable Specification of a Production Hypervisor

Add to your list(s) Download to your calendar using vCal

• Kayvan Memarian (University of Cambridge)
• Monday 02 June 2025, 13:30-14:30
• FW26, Computer Laboratory.

If you have a question about this talk, please contact Dr Meven Lennon-Bertrand.

Developing systems code that robustly provides its intended security guarantees remains very challenging: conventional practice does not suffice, and full functional verification, while now feasible in some contexts, has substantial barriers to entry and use.

In this work, we explore an alternative, more lightweight approach to building confidence for a production hypervisor: the pKVM hypervisor developed by Google to protect virtual machines and the Android kernel from each other. The basic approach is very simple and dates back to the 1970s: we specify the desired behaviour in a way that can be used as a test oracle, and check correspondence between that and the implementation at runtime. The setting makes that challenging in several ways: the implementation and specification are intertwined with the underlying architecture; the hypervisor is highly concurrent; the specification has to be loose in certain ways; the hypervisor runs bare-metal in a privileged exception level; naive random testing 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 bugs in pKVM along the way.

This is not at all what conventional developers (nor what formal verifiers) normally do—but we argue that, with the appropriate mindset, they easily could and should.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FW26, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.