:::

Announcements

:::

[2021-10-01] Prof. Shih-Wei Li, National Taiwan University, "A Secure and Formally Verified Commodity Multiprocessor Hypervisor"(English Speech)

專題討論演講公告
Poster:Post date:2021-09-23
因應防疫,本學期seminar課程改為線上教學,然10/1仍提供40位師生可到場聽講。
 
因座位有限,請務必於9/29(三)前完成報名,當天請依系辦安排之座位號碼入座(將張貼於R103門口),並請全程配戴口罩,保持社交距離。
報名網址: https://forms.gle/QWVpTak9Gy2nwq4c9


Title:
A Secure and Formally Verified Commodity Multiprocessor Hypervisor
Date: 2021-10-01 2:20pm-3:30pm
Location: R103, CSIE
Speaker: Prof. Shih-Wei Li, National Taiwan University
 
 

Abstract:

 
Commodity hypervisors are widely deployed to support virtual machines (VMs) on multiprocessor hardware. Their growing complexity poses a security risk. To enable formal verification over such a large codebase, we introduce microverification, a new approach that decomposes a commodity hypervisor into a small core and a set of untrusted services so that we can prove the security properties of the entire hypervisor by verifying the core alone. To verify the multiprocessor hypervisor core, we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification, and the top layer specification is refined by all layers of the core implementation. To verify commodity hypervisor features that require dynamically changing information flow, we introduce data oracles to mask intentional information flow. We can then prove noninterference at the top layer specification and guarantee the resulting security properties hold for the entire hypervisor implementation. Using microverification, we retrofitted the Linux KVM hypervisor with only modest modifications to its codebase. Using Coq, we proved that the hypervisor protects the confidentiality and integrity of VM data while retaining KVM’s functionality and performance. Our work is the first machine-checked security proof for a commodity multiprocessor hypervisor.
 
Biography:
 
Shih-Wei Li is an Assistant Professor of Computer Science and Information Engineering at National Taiwan University. He was a Ph.D. candidate in computer science at Columbia University, advised by Professor Jason Nieh. His research interests span across areas in operating systems, security, virtualization, verification, and performance evaluation. He has authored several peer-reviewed papers that were published in top-tier conferences including, IEEE Security and Privacy, USENIX Security, SOSP, ISCA, and Usenix ATC.
 
 
Last modification time:2021-09-23 PM 2:09

cron web_use_log