Relaxed virtual memory in Armv8-A
View / Open Files
Authors
Simner, Ben
Armstrong, Alasdair
Pichon-Pharabod, Jean
Pulte, Christopher
Grisenthwaite, Richard
Conference Name
European Symposium on Programming
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Simner, B., Armstrong, A., Pichon-Pharabod, J., Pulte, C., Grisenthwaite, R., & Sewell, P. Relaxed virtual memory in Armv8-A. European Symposium on Programming. https://doi.org/10.17863/CAM.80994
Abstract
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, for the first time.
Sponsorship
This work was partially funded by an Arm/EPSRC iCASE PhD studentship (Simner), Arm Limited, Google, ERC Advanced Grant (AdG) 789108 ELVER, and the UK Government Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694).
Funder references
Engineering and Physical Sciences Research Council (EP/K008528/1)
European Research Council (789108)
Innovate UK (105694)
EPSRC (2097768)
Identifiers
External DOI: https://doi.org/10.17863/CAM.80994
This record's URL: https://www.repository.cam.ac.uk/handle/1810/333577
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.
Recommended or similar items
The current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk