一句话：提出分离逻辑 VMSL，可模块化推理 FF-A hypercall ABI 上通信的虚拟机并机械化证明其鲁棒安全性。
论文研究 Arm FF-A hypercall ABI 的设计是否对虚拟机足够表达且安全，核心问题是超薄 hypervisor 的规范及其跨虚拟机页面共享 ABI 应满足何种保证。作者将 FF-A 的一个较大片段形式化为带简化 ISA 的机器，把 hypercall 视为机器步骤，并提出新的分离逻辑 VMSL，证明其相对机器执行模型可靠，进而对通过 ABI 通信的虚拟机做模块化推理。该逻辑还能证明通信虚拟机的鲁棒安全性：即使部分虚拟机被攻陷并运行未知代码，也无法破坏运行已知代码的虚拟机的安全性质。所有结果均在 Coq 的 Iris 框架中机械化。
Thin hypervisors make it possible to isolate key security components like keychains, fingerprint readers, and digital wallets from the easily-compromised operating system. To work together, virtual machines running on top of the hypervisor can make hypercalls to the hypervisor to share pages between each other in a controlled way. However, the design of such hypercall ABIs remains a delicate balancing task between conflicting needs for expressivity, performance, and security. In particular, it raises the question of what makes the specification of a hypervisor, and of its hypercall ABIs, good enough for the virtual machines. In this paper, we validate the expressivity and security of the design of the hypercall ABIs of Arm's FF-A. We formalise a substantial fragment of FF-A as a machine with a simplified ISA in which hypercalls are steps of the machine. We then develop VMSL, a novel separation logic, which we prove sound with respect to the machine execution model, and use it to reason modularly about virtual machines which communicate through the hypercall ABIs, demonstrating the hypercall ABIs' expressivity. Moreover, we use the logic to prove robust safety of communicating virtual machines, that is, the guarantee that even if some of the virtual machines are compromised and execute unknown code, they cannot break the safety properties of other virtual machines running known code. This demonstrates the intended security guarantees of the hypercall ABIs. All the results in the paper have been formalised in Coq using the Iris framework.
@article{paperbot2002,
title = {VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A},
author = {Zongyuan Liu and Sergei Stepanenko and Jean Pichon-Pharabod and Amin Timany and Aslan Askarov and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591279}
}