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

Memarian, Kayvan; Simner, Ben; Kaloper-Meršinjak, David; Pérami, Thibaut; Sewell, Peter

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

Authors

Memarian, Kayvan

Simner, Ben

Kaloper-Meršinjak, David

Pérami, Thibaut

Sewell, Peter

Publisher

Association for Computing Machinery (ACM)
Department of Computer Science and Technology
https://doi.org/10.1145/3731569.3764817

Description

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 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.
UK 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