Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor

Simple item page
dc.creatorMemarian, Kayvan
dc.creatorSimner, Ben
dc.creatorKaloper-Meršinjak, David
dc.creatorPérami, Thibaut
dc.creatorSewell, Peter
dc.date2025-09-11T11:27:48Z
dc.date2025-10-13
dc.date.accessioned2026-08-03T03:27:26Z
dc.descriptionDeveloping 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 paper, 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.
dc.descriptionUK Research and Innovation award number(s): EP/Y035976/1 SAFER European Research Council award number(s): 789108, 101189371 Innovate UK award number(s): DSbD 105694 EPSRC award number(s): EP/Z000580/1 Google
dc.formatapplication/pdf
dc.identifier979-8-4007-1870-0
dc.identifierhttps://www.repository.cam.ac.uk/handle/1810/389347
dc.identifierhttps://doi.org/10.17863/CAM.121274
dc.identifier.urihttps://repo.dare.co.zw/handle/123456789/176827
dc.languageeng
dc.publisherAssociation for Computing Machinery (ACM)
dc.publisherDepartment of Computer Science and Technology
dc.publisherhttps://doi.org/10.1145/3731569.3764817
dc.rightsAttribution 4.0 International (CC BY 4.0)
dc.rightshttps://creativecommons.org/licenses/by/4.0/
dc.subject46 Information and Computing Sciences
dc.subject4612 Software Engineering
dc.titleGhost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor
dc.typeConference Object

Files

Collections

University of Cambridge Apollo