Designing new low-level systems programming languages suitable for verification - pKVM

点击翻译按钮获取中文摘要

pKVM (protected KVM) is an ongoing project to enable KVM on Google's Android mobile operating system. It has specific goals which make it a challenging, but worthwhile target for formal verification. A hypervisor is a piece of software that creates and manages virtual machines. Though most users are likely to have come across examples such as VirtualBox, VMWare or Parallels Desktop for Mac, this proposal is concerned with a different kind of hypervisor.Bare-metal (also known as Type-1 ) hypervisors run directly on hardware (as opposed to the Type-2 examples given earlier, which require an operating system torun on). KVM (kernel-based virtual machine) is a Linux kernel module which allows the Linux kernel to run as a bare-metal hypervisor.pKVM (protected KVM) is an ongoing project to enable KVM on Google's Android mobile operating system (or more specifically, the Android fork of Linux).Its main, high-level goal is to support Android's security model: "guest data remains private even if the host kernel has been compromised". Expressed another way, pKVM needs to "de-privilege third party code and provide a portable environment in which services are isolated from one another and also from the rest of Android". Achieving this would allow Google to provide a single, extensible kernel binary to platform vendors (such as phone manufacturers), who can then link it (via a small ABI which Google guarantees will be stable across updates) with software to support their particular hardware platform. There are two advantages to doing so: security and functionality.Currently, each hardware platform has its own kernel, which makes delivering security patches for Android difficult, since each vendor needs to update their version of the kernel. A single, extensible binary would eliminate duplication of effort and reduce delays and fragmentation in the dispersion of security updates. It also has a similar effect with regards to exposing new hardware features quickly and at the correct level of abstraction across many different hardware platforms.However, there is an important trade-off here: any vulnerabilities and errors in pKVM itself could undermine the security and functionality benefits mentioned above. As such, it becomes important to gain a higher level of confidence in the correctness of the design and implementation.One way to increase the confidence in both is to keep them very simple, and this is feasible because the features pKVM needs to support are also (relatively) simple (for example, message passing, context switching, and page-table set-up and translations). Another way to do so is to formally reason and prove aspects of (if not the whole) program correct.