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