Microverification of the Linux KVM Hypervisor-顾荣辉

1 .Microveri cation of the Linux KVM Hypervisor Ronghui Gu, CS@Columbia (Joint work with Jason Nieh, Xupeng Li, et al.) fi 

2 .A Secure and Formally Veri ed Linux KVM Hypervisor Shih-wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Hui. S&P (Oakland) 2021 Formally Veri ed Memory Protection for a Commodity Multiprocessor Hypervisor Shih-wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Hui. USENIX Security 2021 Formal Veri cation of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware Runzhou Tao, Jianan Yao, Xupeng Li, Shih-wei Li, Jason Nieh, and Ronghui Gu. SOSP 2021 Spoq: Scaling Machine-Checkable Systems Veri cation in Coq Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh. OSDI 2023 (to appear) fi fi fi fi 

3 .Formal veri cation is an act of proving that a program meets its programmer’s intention fi 

4 . hard and costly Formal veri cation is an act of proving that a program meets its speci cation simple (multicore) memory safety OS kernels functional correctness le systems con dentiality hypervisors integrity fi fi fi fi 

5 . uniprocessor hard microkerneland costly Formal veri cation is an act of proving that seL4 a program meets its Proof speci 11 py cation [SOSP’09] simple (multicore) memory safety OS kernels C functional 7.5k LOC correctness le systems con dentiality hypervisors integrity fi fi fi fi 

6 . hard to extend hard to reuse hard to maintain hard and costly Formal veri cation is an act of proving that a program meets its speci cation simple (multicore) memory safety OS kernels functional correctness le systems con dentiality hypervisors integrity fi fi fi fi 

7 . Deep Speci cation and Certi ed Abstraction Layers [POPL’15] Deep spec L2 captures all we need to know about M over L1 memory safety functional correctness con dentiality integrity system deep spec fi fi fi 

8 . mCertiKOS[POPL’15] seL4[SOSP’09] certi ed sequential OS kernels Ironclad[OSDI’14] 3k C&Asm, 1 py IronFleet[SOSP’15] Interrupt&Device Driver[PLDI’16a] 0.5 py FSCQ[SOSP’15][SOSP’15] Security[PLDI’16b] 0.5 py Komodo[SOSP’17] AtomFS[SOSP’19] CertiKOS[OSDI’16] [PLDI’18] [CACM RH] the rst formally certi ed multicore Perennial[SOSP’19] OS kernel, 6.5k C&Asm, 2 py Push-button Veri cation [OSDI’16][SOSP’17] RT-CertiKOS[POPL’20] [OSDI’18][SOSP’19] schedulability, temporal isolation fi fi fi fi 

9 . mCertiKOS[POPL’15] seL4[SOSP’09] certi ed sequential OS kernels Ironclad[OSDI’14] 3k C&Asm, 1 py IronFleet[SOSP’15] Interrupt&Device Driver[PLDI’16a] 0.5 py FSCQ [SOSP’15][SOSP’15] None of them Komodo are [SOSP’17] Security[PLDI’16b] 0.5 py commodity systems AtomFS[SOSP’19] CertiKOS[OSDI’16] [PLDI’18] [CACM RH] the rst formally certi ed multicore Perennial [SOSP’19] OS kernel, 6.5k C&Asm, 2 py Push-button Veri cation RT-CertiKOS[POPL’20] [OSDI’16][SOSP’17] [OSDI’18][SOSP’19] schedulability, temporal isolation fi fi fi fi 

10 .CertiKOS 6.5k LOC 

11 .CertiKOS Commodity Systems, e.g., 6.5k LOC 70+ Layers of Deep Spec Linux KVM 2M LOC ? 

12 . Microveri cation Reduce the proof effort of commodity systems in three ways: fi 

13 . Microveri cation Reduce the proof effort of commodity systems in three ways: 1. Given desired properties, reduce the code requiring veri cation. fi fi 

14 . Microveri cation Given desired properties, Servs Commodity we retro t System into Core such that the properties of the entire system can be veri ed using only Core regardless of the behavior of Servs fi fi fi 

15 . Microveri cation Servs Commodity System Core much smaller TCB same interface same functionality similar performance fi 

16 . Microveri cation Reduce the proof effort of commodity systems in three ways: 1. Given desired properties, reduce the code requiring veri cation. 2. Prove Core re nes spec in SW/HW layers that preserve desired properties. fi fi fi 

17 . Microveri cation Servs Core fi 

18 . Microveri cation Re nement in a multiprocessor setting may not preserve security guarantees. - D. Stefan, et al. Servs Desired properties Core fi fi 

19 . Microveri cation Reduce the proof effort of commodity systems in three ways: 1. Given desired properties, reduce the code requiring veri cation. 2. Prove Core re nes spec in SW/HW layers that preserve desired properties. 3. Prove Servs interacting with spec of Core cannot violate desired properties. fi fi fi 

20 . Deep Speci cation v.s. Microveri cation Desired properties Desired properties Servs Deep Spec Core re ne retro t System Commodity System fi fi fi fi 

21 . Deep Speci cation v.s. Microveri cation Desired properties Desired properties Desired properties Desired properties Servs Deep Spec Core re ne retro t System Commodity System fi fi fi fi 

22 .Microveri cation of Linux KVM hypervisor fi 

23 .Microveri cation — Desired Properties of Linux KVM hypervisor VM con dentiality and integrity VM con dentiality: VM secrets cannot be leaked to an adversary VM integrity: VM secrets cannot be modi ed by an adversary Out of scope: availability, side-channel attacks, physical attacks fi fi fi fi 

24 .Microveri cation — Work ow of Linux KVM hypervisor 1. Design the security policies 2. Retro tting according to the policies 3. Verify the Core using in security-preserving layers 4. Prove security guarantees using the interface of the Core fi fl fi 

25 .Microveri cation — Work ow of Linux KVM hypervisor 1. Design the security policies 2. Retro tting according to the policies 3. Verify the Core using in security-preserving layers 4. Prove security guarantees using the interface of the Core fi fl fi 

26 .Microveri cation — Security Policies of Linux KVM hypervisor • VM-dataiso: A given VM’s data in CPU registers, private memory, and assigned devices are isolated from KServ and all other VMs. • VM-iodataiso: The con dentiality and integrity of a given VM’s I/O data is protected from KServ and all other VMs. • Data-declassi cation: a given VM’s non-private data may be intentionally released (and thereby innocuously compromised) to support virtualization features. fi fi fi 

27 .Microveri cation — Security Policies of Linux KVM hypervisor • VM-dataiso: A given VM’s data in CPU registers, private memory, and assigned devices are isolated from KServ and all other VMs. • VM-iodataiso: The con dentiality and integrity of a given VM’s I/O data is protected from KServ and all other VMs. • Data-declassi cation: a given VM’s non-private data may be intentionally released (and thereby innocuously compromised) to support virtualization features. • A VM may send encrypted data via shared I/O devices virtualized via untrusted KServ fi fi fi 

28 .Microveri cation — Work ow of Linux KVM hypervisor 1. Design the security policies 2. Retro tting according to the policies 3. Verify the Core using in security-preserving layers 4. Prove security guarantees using the interface of the Core fi fl fi 

29 .Microveri cation — Retro tting of Linux KVM hypervisor EL1 VM1 VM2 KVM EL2 Linux hardware KVM fi fi