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

pKVM （protected KVM）是一个正在进行的项目，用于在b谷歌的Android移动操作系统上启用KVM。它有特定的目标，这使它成为一个具有挑战性的，但值得正式验证的目标。虚拟机管理程序是一个创建和管理虚拟机的软件。虽然大多数用户可能都遇到过VirtualBox、VMWare或Parallels Desktop for Mac之类的例子，但这个建议涉及的是一种不同的管理程序。裸机（也称为Type-1）管理程序直接在硬件上运行（与前面给出的Type-2示例相反，后者需要在操作系统上运行）。KVM（基于内核的虚拟机）是一个Linux内核模块，它允许Linux内核作为裸机管理程序运行。pKVM（受保护的KVM）是一个正在进行的项目，用于在b谷歌的Android移动操作系统（或者更具体地说，Linux的Android分支）上启用KVM。它主要的高级目标是支持Android的安全模型：“即使主机内核被破坏，客户数据仍然是私有的”。换句话说，pKVM需要“取消第三方代码的特权，并提供一个可移植的环境，在这个环境中，服务彼此隔离，也与Android的其他部分隔离”。实现这一点将允许谷歌向平台供应商（比如手机制造商）提供一个单一的、可扩展的二进制内核，然后他们可以将它（通过谷歌保证在更新期间保持稳定的一个小ABI）与软件链接起来，以支持他们特定的硬件平台。这样做有两个好处：安全性和功能性。目前，每个硬件平台都有自己的内核，这使得为Android提供安全补丁变得困难，因为每个供应商都需要更新自己的内核版本。一个单一的、可扩展的二进制文件将消除重复工作，并减少安全更新分散中的延迟和碎片。在跨许多不同硬件平台以正确的抽象级别快速暴露新硬件特性方面，它也具有类似的效果。然而，这里有一个重要的权衡：pKVM本身的任何漏洞和错误都可能破坏上面提到的安全性和功能优势。因此，对设计和实现的正确性获得更高级别的信心变得非常重要。增加对两者的信心的一种方法是使它们非常简单，这是可行的，因为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.