RT DF A1 Li, Shih-Wei. T1 A Secure and Formally Verified Commodity Multiprocessor Hypervisor