Keynote: Can we reason about the security of concurrent systems code?
summary
Goal is to verify Google’s PKVM hypervisor running on ARM, not just papers: ARM semantics is captured in 420,000 lines of ARM spec (Sail/ASL), the hypervisor is ~20–30k ARM instructions, and a runnable top-level executable C spec is implemented. Work includes Sail/ASL → Isabelle proofs for translation properties, Iris proofs for specific exception-handler assembly after symbolic simplification, a proposed simplified/DRF-like VM model, CN/refined-C tooling, and proposed translation-validation of clang; partial results exist, but full end-to-end verification remains open.
AI-written summary · about
chapters (21)
- 0:00Keynote intro
- 1:03Verifying PKVM hypervisors
- 4:20Concurrent systems code challenges
- 8:55ARM semantics and memory models
- 16:30ARM's relaxed memory complexities
- 21:24Sequential and concurrent verification
- 23:53Verifying sequential hypervisor parts
- 27:44ARM instruction behavior verification
- 30:20Connecting verification foundations
- 33:13Reasoning about hypervisor concurrency
- 36:54Proof framework for hypervisor
- 41:54Verifying C in hypervisor
- 45:45Classic verification pitfalls
- 47:31Testing with development teams
- 50:24C as hypervisor spec language
- 53:55Feasibility of concurrent security reasoning
- 55:20Q&A: Compiler verification
- 58:31Q&A: Maintaining verification
- 1:00:40Q&A: C and assembly composition
- 1:02:45Q&A: Security and memory models
- 1:04:32Q&A: Speculative execution impact
related talks
18mVMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…)
43mKeynote: Security Under the BEAM
11mSpecifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
23mMorello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…)
16mKeynote: RISC-V Security - Current Initiatives and Future Trends
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era
19mA Verification Methodology for the Arm® Confidential Computing Architecture: Fr...
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...