überSpark: Enforcing Verifiable Object Abstractions for Automated...
summary
Architecture that enforces verifiable object abstractions for compositional hypervisor verification, using Frama‑C, ComCert, SMT solvers and a hardware model plus a C‑embedded Assembly dialect CASM. Refactors xmhf into 11 uber objects (~7k LOC), writes 5,544 lines of ACSL annotations, verifies objects in 48s–23min (cumulative <1 hour), and reports about 2% runtime overhead versus vanilla xmhf. Builds work end‑to‑end; proofs target memory/control‑flow invariants and composition without hardware deep‑privileging.
AI-written summary · about
chapters (19)
- 0:00Intro
- 3:58An extensible hypervisor
- 5:04Code size vs. HW de privileging
- 5:46Continuous Development
- 6:22Shared Resources
- 6:45Different Configurations
- 7:33Verification vs. Programming Paradigm
- 8:51über Spark from above
- 11:44The überObject
- 13:05überObject: Sentinel
- 13:52überBlueprint & Concurrency
- 17:22überObject: CASM Functions & HW Model
- 19:13überObject: Coding and Behavior Specification
- 20:17überObject: Resource Interface Confinement
- 21:31überObject: Summary
- 22:16An über Micro-Hypervisor (ÜXMHF)
- 23:25ÜXMHF Verification Results
- 25:15ÜXMHF: Micro & Application Benchmarks
- 28:49Questions?
related talks
30mModularity, Code Specialization, and Zero-Cost Abstractions for Program Verifica...
19mA Verification Methodology for the Arm® Confidential Computing Architecture: Fr...
21mPractical Verification Of Smart Contracts Using Memory Splitting
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 05mKeynote: Can we reason about the security of concurrent systems code?
30mVerifying Solidity Smart Contracts Via Communication Abstraction in SmartACE