Congratulations to Assistant professor Jean Pichon-Pharabod and Professor Lars Birkedal, who both have received $60,000 from the Google ASPIRE fund to continue their work on the pKVM verification project, which is an ongoing effort between Cambridge and Aarhus University aimed at verifying properties of the pKVM hypervisor being developed at Google. 

The purpose of pKVM is to provide memory isolation between a set of security domains, to better separate untrusted code from security-critical code. It is implemented as a hypervisor, where each security domain is a virtual machine, and will run on top of ARM processors.

Jean Pichon-Pharabod will investigate how to bridge the gap between the model of ARMv8 address translation, and the address translation as it is used by pKVM. Lars Birkedal will use the grant to continue current work on a top-level specification of the hypervisor and to prove desired isolation properties of the hypervisor.