VeriSMo: A Verified Security Module for Confidential VMs
Talkat 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) · 2024-07-10..07-12·
summary
VERISMO implements a Rust security module for AMD SEV-SNP that is formally verified for functional correctness, secure information flow, and VM confidentiality and integrity using the VaroS-style Rust verifier. Verification covers the low-level memory and CPU operations that the untrusted hypervisor can interrupt, finds and fixes a subtle SVSM bug that could expose secrets, verifies 4,000 lines of executable Rust in 3 minutes, achieves C-like performance, and claims zero verification runtime overhead.
AI-written summary · about
chapters (10)
- 0:00VeriSMo introduction
- 1:30Security module role
- 2:57Hardware features
- 4:49Rust verification needs
- 6:34Attack model approach
- 9:00Memory state transitions
- 10:46Formal verification
- 12:12Implementation results
- 13:40Security bug fix
- 15:50Conclusion
related talks
28mProviding Confidential Guest Services with a Secure VM Service Module on AMD
45mSecuring Confidential VMs with COCONUT-SVSM
25mProtecting from MaliciousHypervisor Using AMD SEV-SNP
15mRemote Attestation in AMD SEV-SNP Confidential VMs
31mConfidential Computing for RISC-V-based Platforms
13mVM Security with Confidential Computing
40mUpcoming x86 Technologies for Malicious Hypervisor Protection
11mTrusted in-guest hypervisor services with secure VM service module