arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 2203.00642cs.ARcs.OScs.PL
收藏

Armv8-A(扩展版)中的宽松虚拟内存

Relaxed virtual memory in Armv8-A (extended version)

Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell

摘要:

虚拟内存是一种强制执行安全边界的基本机制,但其松弛内存并发语义以前没有被详细研究。管理虚拟内存的并发系统代码完全是非正式的,操作系统和虚拟机管理程序验证必须做出主要的简化假设。我们探索宽松的虚拟内存语义在Armv 8-A架构的设计空间,以支持未来的系统软件验证。在与Arm的讨论中,我们确定了许多设计问题;开发了一个测试套件,包括来自Google正在开发的pKVM生产管理程序的用例;用公理式并发模型划分设计空间;证明在简单的稳定配置下,我们的架构模型可以折叠到以前的“用户”模型;开发工具来计算与完整的Armv 8-A ISA语义集成的模型中允许的行为;开发一个硬件测试设备这列出了一些主要问题,在宽松的虚拟内存把这些安全关键系统的现象到域的编程语言语义和验证与基础架构语义。本文是ESOP 2022中一篇论文的扩展版本,在正文中有额外的解释和示例,附录详细介绍了我们的石蕊测试,模型,证明和测试结果。

英文摘要:

Virtual memory is an essential mechanism for enforcing security boundaries, but its relaxed-memory concurrency semantics has not previously been investigated in detail. The concurrent systems code managing virtual memory has been left on an entirely informal basis, and OS and hypervisor verification has had to make major simplifying assumptions. We explore the design space for relaxed virtual memory semantics in the Armv8-A architecture, to support future system-software verification. We identify many design questions, in discussion with Arm; develop a test suite, including use cases from the pKVM production hypervisor under development by Google; delimit the design space with axiomatic-style concurrency models; prove that under simple stable configurations our architectural model collapses to previous "user" models; develop tooling to compute allowed behaviours in the model integrated with the full Armv8-A ISA semantics; and develop a hardware test harness. This lays out some of the main issues in relaxed virtual memory bringing these security-critical systems phenomena into the domain of programming-language semantics and verification with foundational architecture semantics. This document is an extended version of a paper in ESOP 2022, with additional explanation and examples in the main body, and appendices detailing our litmus tests, models, proofs, and test results.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑