OS Conference-顧榮輝.pdf

1、Microverification of the Linux KVM HypervisorRonghui Gu,CSColumbia(Joint work with Jason Nieh,Xupeng Li,et al.)A Secure and Formally Verified Linux KVM HypervisorShih-wei Li,Xupeng Li,Ronghui Gu,Jason Nieh,and John Hui.S&P(Oakland)2021Formally Verified Memory Protection for a Commodity Multiprocesso

2、r HypervisorShih-wei Li,Xupeng Li,Ronghui Gu,Jason Nieh,and John Hui.USENIX Security 2021Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory HardwareRunzhou Tao,Jianan Yao,Xupeng Li,Shih-wei Li,Jason Nieh,and Ronghui Gu.SOSP 2021Spoq:Scaling Machine-Checkable Systems Verificatio

3、n in CoqXupeng Li,Xuheng Li,Wei Qiang,Ronghui Gu,and Jason Nieh.OSDI 2023(to appear)Formal verification is an act of proving that a program meets its programmers intentionFormal verification is an act of proving that a program meets its specificationmemory safety functional correctness confidentiali

4、ty integrityhard and costlysimple(multicore)OS kernels file systems hypervisorsFormal verification is an act of proving that a program meets its specificationmemory safety functional correctness confidentiality integrityhard and costlysimple(multicore)OS kernels file systems hypervisorsseL4 SOSP09C7

5、.5k LOCProof11 pyuniprocessor microkernelFormal verification is an act of proving that a program meets its specificationmemory safety functional correctness confidentiality integrityhard and costlysimple(multicore)OS kernels file systems hypervisorshard to extend hard to reuse hard to maintainDeep S

6、pecification and Certified Abstraction Layers POPL15systemdeep specDeep spec captures all we need to know about overL2ML1memory safety functional correctness confidentiality integrityCertiKOSOSDI16 PLDI18 CACM RH the first formally certified multicore OS kernel,6.5k C&Asm,2 pymCertiKOSPOPL15 certifi

7、ed sequential OS kernels 3k C&Asm,1 pySecurityPLDI16b 0.5 pyInterrupt&Device DriverPLDI16a 0.5 py RT-CertiKOSPOPL20 schedulability,temporal isolationseL4SOSP09IroncladOSDI14FSCQSOSP15SOSP15KomodoSOSP17AtomFSSOSP19PerennialSOSP19IronFleetSOSP15Push-button Verification OSDI16SOSP17 OSDI18SOSP19CertiKO

8、SOSDI16 PLDI18 CACM RH the first formally certified multicore OS kernel,6.5k C&Asm,2 pymCertiKOSPOPL15 certified sequential OS kernels 3k C&Asm,1 pySecurityPLDI16b 0.5 pyInterrupt&Device DriverPLDI16a 0.5 py RT-CertiKOSPOPL20 schedulability,temporal isolationseL4SOSP09IroncladOSDI14FSCQSOSP15SOSP15K

9、omodoSOSP17AtomFSSOSP19PerennialSOSP19IronFleetSOSP15Push-button Verification OSDI16SOSP17 OSDI18SOSP19None of them are commodity systemsCertiKOS 6.5k LOCCertiKOS 6.5k LOC70+Layers of Deep SpecCommodity Systems,e.g.,Linux KVM 2M LOC?Microverification Reduce the proof effort of commodity systems in t

10、hree ways:Microverification Reduce the proof effort of commodity systems in three ways:1.Given desired properties,reduce the code requiring verification.Microverification Given desired properties,Commodity Systemwe retrofitintoCoreServssuch that the properties of the entire systemcan be verified usi

11、ng onlyCoreregardless of the behavior of ServsMicroverification same interfaceCommodity SystemCoreServssame functionalitysimilar performancemuch smaller TCBMicroverification Reduce the proof effort of commodity systems in three ways:1.Given desired properties,reduce the code requiring verification.2

12、.Prove Core refines spec in SW/HW layers that preserve desired properties.CoreServsMicroverification CoreServsDesired propertiesMicroverification Refinement in a multiprocessor setting may not preserve security guarantees.-D.Stefan,et al.Microverification Reduce the proof effort of commodity systems

13、 in three ways:1.Given desired properties,reduce the code requiring verification.2.Prove Core refines spec in SW/HW layers that preserve desired properties.3.Prove Servs interacting with spec of Core cannot violate desired properties.Microverification SystemDeep Specification v.s.Deep SpecrefineDesi

14、red propertiesCommodity SystemCoreServsretrofitDesired propertiesCoreDesired propertiesMicroverification SystemDeep Specification v.s.Deep SpecrefineCommodity SystemCoreServsretrofitCoreDesired propertiesDesired propertiesDesired propertiesMicroverification of Linux KVM hypervisorMicroverification o

15、f Linux KVM hypervisorVM confidentiality and integrityVM confidentiality:VM secrets cannot be leaked to an adversaryVM integrity:VM secrets cannot be modified by an adversaryOut of scope:availability,side-channel attacks,physical attacks Desired PropertiesMicroverification of Linux KVM hypervisor Wo

16、rkflow1.Design the security policies 2.Retrofitting according to the policies 3.Verify the Core using in security-preserving layers 4.Prove security guarantees using the interface of the CoreMicroverification of Linux KVM hypervisor Workflow1.Design the security policies 2.Retrofitting according to

17、the policies 3.Verify the Core using in security-preserving layers 4.Prove security guarantees using the interface of the CoreMicroverification of Linux KVM hypervisor Security PoliciesVM-dataiso:A given VMs data in CPU registers,private memory,and assigned devices are isolated from KServ and all ot

18、her VMs.VM-iodataiso:The confidentiality and integrity of a given VMs I/O data is protected from KServ and all other VMs.Data-declassification:a given VMs non-private data may be intentionally released(and thereby innocuously compromised)to support virtualization features.Microverification of Linux

19、KVM hypervisor Security PoliciesVM-dataiso:A given VMs data in CPU registers,private memory,and assigned devices are isolated from KServ and all other VMs.VM-iodataiso:The confidentiality and integrity of a given VMs I/O data is protected from KServ and all other VMs.Data-declassification:a given VM

20、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 KServMicroverification of Linux KVM hypervisor Workflow1.Design the security policies 2.Retrofitting a

21、ccording to the policies 3.Verify the Core using in security-preserving layers 4.Prove security guarantees using the interface of the CoreMicroverification of Linux KVM hypervisor RetrofittingKVMLinuxhardwareVM1VM2KVMEL2EL1Microverification of Linux KVM hypervisor RetrofittingKCoreseKVMKVMLinuxKServ

22、LinuxhardwareVM1hardwareVM2VM1VM2retrofitKVMEL1EL2EL2EL1Microverification of Linux KVM hypervisor RetrofittingKVMLinuxhardwareVM1VM2retrofitKVMEL2EL1Microverification of Linux KVM hypervisor RetrofittingseKVMKServLinuxhardwareVM1VM2NPT1NPT2NPTsvNPT1vNPT1access control+validationto protect VM memory

23、CPU registers boot images I/O buffersidentical map to free/shared pagescopy of NPTsMicroverification of Linux KVM hypervisor RetrofittingseKVMKServLinuxhardwareVM1VM2NPT1NPT2NPTsvNPT1vNPT1access control+validationto protect VM memory CPU registers boot images I/O buffersallocate page for VM1Microver

24、ification of Linux KVM hypervisor Workflow1.Design the security policies 2.Retrofitting according to the policies 3.Verify the Core using in security-preserving layers 4.Prove security guarantees using the interface of the CoreMicroverification of Linux KVM hypervisor Refine KCore via Game Semantics

25、multicore hardwareseKVMMicroverification of Linux KVM hypervisor Refine KCore via Game SemanticsstrategyHow the program p will generate events on behalf of CPU i at each step regarding the given log l,pimulticore hardwarestrategy2strategy1HW schedulerseKVMMicroverification of Linux KVM hypervisor Re

26、fine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)0multicore hardwarestrategy2strategy1HW schedulerseKVM q2Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)01multicore hardwarestrategy2strategy1HW schedule

27、rseKVM q2Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)012multicore hardwarestrategy2strategy1HW schedulerseKVM q2Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(

28、n%3=0)012multicore hardwarestrategy2strategy1HW schedulerseKVM q2Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)0123multicore hardwarestrategy2strategy1HW schedulerseKVM q2Microverification of Linux KVM hypervisor Refine KCore v

29、ia Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)01234multicore hardwarestrategy2strategy1HW schedulerseKVM q2Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)012345multicore hardwarestrategy2strategy1HW schedulerseK

30、VM q2Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)0123456multicore hardwarestrategy2strategy1HW schedulerseKVM q2Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(

31、n%3=0)0multicore hardwarestrategy2strategy1HW schedulerseKVMstrategy1event oracleeoMicroverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)02multicore hardwarestrategy2strategy1HW schedulerseKVMstrategy1event oracleeo1Microverification o

32、f Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)023multicore hardwarestrategy2strategy1HW schedulerseKVMstrategy1event oracleeo1Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)0

33、2345multicore hardwarestrategy2strategy1HW schedulerseKVMstrategy1event oracleeo1Microverification of Linux KVM hypervisor Refine KCore via Game Semantics p1:inc n by 1 if(n%3!=0):inc n by 1 if(n%3=0)02356multicore hardwarestrategy2strategy1HW schedulerseKVMstrategy1event oracleeo14Microverification

34、 of Linux KVM hypervisor Refine KCore via Game Semantics:inc n by 2 if(n%3!=0):inc n by 1 if(n%3=0)0multicore hardwarestrategy2strategy1HW schedulerseKVMstrategy1event oracleeostrategy1event oracle 0p1trace refinementMicroverification of Linux KVM hypervisor Refine KCore via Game Semantics:inc n by

35、2 if(n%3!=0):inc n by 1 if(n%3=0)03multicore hardwarestrategy2strategy1HW schedulerseKVMstrategy1event oracleeo1strategy1event oracle 0p1trace refinementMicroverification of Linux KVM hypervisor Refine KCore via Game Semantics:inc n by 2 if(n%3!=0):inc n by 1 if(n%3=0)036multicore hardwarestrategy2s

36、trategy1HW schedulerseKVMstrategy1event oracleeo14strategy1event oracle 0p1trace refinementMicroverification of Linux KVM hypervisor Refine KCore via Game Semantics map pageitrace refinementMicroverification of Linux KVM hypervisor Refine KCore via Game Semantics map pageitrace refinementdoes not pr

37、eserve securityMicroverification of Linux KVM hypervisor Refine KCore via Game SemanticsMicroverification of Linux KVM hypervisor Transparent RefinementMicroverification of Linux KVM hypervisor Workflow1.Design the security policies 2.Retrofitting according to the policies 3.Verify the Core using in

38、 security-preserving layers 4.Prove security guarantees using the interface of the CoreMicroverification of Linux KVM hypervisor NoninterferenceTwo states are indistinguishable to p if ps private data lens are the sameMicroverification of Linux KVM hypervisor NoninterferenceTwo states are indistingu

39、ishable to p if ps private data lens are the sameMicroverification of Linux KVM hypervisor NoninterferenceTwo states are indistinguishable to p if ps private data lens are the same State indistinguishability is preserved during the whole executionMicroverification of Linux KVM hypervisor Noninterfer

40、enceHow to deal with declassified data?For encrypted data.How to distinguish intentional information release with information leakage?Microverification of Linux KVM hypervisor NoninterferenceUse data oracle:intentional information release is masked by the next integer returned by data oracle that is

41、 independent with the historical executionExtend SeKVM using hardware layersExtend SeKVM Realistic Hardware Model Security21TLBCoherent CachePTsCoherent CacheCoherent CachesMain MemoryCPU1CPU0.Model AExtend SeKVM Realistic Hardware Model Security21TLBCoherent CachePTsCoherent CacheCoherent CachesPTs

42、Shared CacheMain MemoryMain MemoryCPU1CPU0.CPU1CPU0.Model BModel Ahardware layer refinementExtend SeKVM Relaxed Memory Model SOSP21We introduce six weak DRF(wDRF)conditions wDRF only requires most of the kernel to be DRF Extra constraints for the non-DRF parts of the systemExtend SeKVMWe introduce s

43、ix weak DRF(wDRF)conditions wDRF only requires most of the kernel to be DRF Extra constraints for the non-DRF parts of the system Relaxed Memory Model SOSP21Results of microverification of Linux KVM hypervisorMicroverification of Linux KVM hypervisorVM confidentiality and integrityVM confidentiality:VM secrets cannot be leaked to an adversaryVM integrity:VM secrets cannot be modified by an adversary Verified seKVMKCoreseKVMKServLinuxhardwareVM1VM2Microverification of Linux KVM hypervisor Performance