Ziqiao Zhou

Senior Researcher

论文与出版物

查看方式：

- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github 项目
- VeriSMo: A Verified Security Module for Confidential VMs
  
  Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui
  
  OSDI 2024 | July 2024
  
  Jay Lepreau Best Paper Award
  
  Awarded Best Paper!
  
  Publication Github 项目
- Leveraging Large Language Models for Automated Proof Synthesis in Rust
  
  Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
  
  arXiv:2311.03739 | November 2023
  
  Publication
- Core slicing: closing the gap between leaky confidential VMs and bare-metal cloud
  
  Ziqiao Zhou, Yizhou Shan, Weidong Cui, Xinyang Ge, Marcus Peinado, Andrew Baumann
  
  17th USENIX Symposium on Operating Systems Design and Implementation | July 2023
  
  Publication
- Interpretable Noninterference Measurement and Its Application to Processor Designs
  
  Ziqiao Zhou, Michael K. Reiter
  
  Object-Oriented Programming Systems, Languages, and Applications | October 2021
  
  DOI
- Static Evaluation of Noninterference Using Approximate Model Counting
  
  Ziqiao Zhou, Zhiyun Qian, Michael K. Reiter, Yinqian Zhang
  
  2018 IEEE Symposium on Security and Privacy | April 2018
  
  DOI Publication
- A Software Approach to Defeating Side Channels in Last-Level Caches
  
  Ziqiao Zhou, Michael K. Reiter, Yinqian Zhang
  
  2016 Computer and Communications Security | October 2016
  
  DOI Publication
- Fingerprint-free tracking with dynamic enhanced field division
  
  Qingquan Zhang, Ziqiao Zhou, Wei Xu, Jing Qi, Chenxi Guo, Ping Yi, Ting Zhu, Sheng Xiao
  
  2015 International Conference on Computer Communications | August 2015
  
  DOI Publication

- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github 项目
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github 项目
- Interpretable Noninterference Measurement and Its Application to Processor Designs
  
  Ziqiao Zhou, Michael K. Reiter
  
  Object-Oriented Programming Systems, Languages, and Applications | October 2021
  
  DOI
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github 项目
- Fingerprint-free tracking with dynamic enhanced field division
  
  Qingquan Zhang, Ziqiao Zhou, Wei Xu, Jing Qi, Chenxi Guo, Ping Yi, Ting Zhu, Sheng Xiao
  
  2015 International Conference on Computer Communications | August 2015
  
  DOI Publication
- VeriSMo: A Verified Security Module for Confidential VMs
  
  Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui
  
  OSDI 2024 | July 2024
  
  Jay Lepreau Best Paper Award
  
  Awarded Best Paper!
  
  Publication Github 项目
- Leveraging Large Language Models for Automated Proof Synthesis in Rust
  
  Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
  
  arXiv:2311.03739 | November 2023
  
  Publication
- Core slicing: closing the gap between leaky confidential VMs and bare-metal cloud
  
  Ziqiao Zhou, Yizhou Shan, Weidong Cui, Xinyang Ge, Marcus Peinado, Andrew Baumann
  
  17th USENIX Symposium on Operating Systems Design and Implementation | July 2023
  
  Publication
- Interpretable Noninterference Measurement and Its Application to Processor Designs
  
  Ziqiao Zhou, Michael K. Reiter
  
  Object-Oriented Programming Systems, Languages, and Applications | October 2021
  
  DOI
- Static Evaluation of Noninterference Using Approximate Model Counting
  
  Ziqiao Zhou, Zhiyun Qian, Michael K. Reiter, Yinqian Zhang
  
  2018 IEEE Symposium on Security and Privacy | April 2018
  
  DOI Publication
- A Software Approach to Defeating Side Channels in Last-Level Caches
  
  Ziqiao Zhou, Michael K. Reiter, Yinqian Zhang
  
  2016 Computer and Communications Security | October 2016
  
  DOI Publication

- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github 项目
- VeriSMo: A Verified Security Module for Confidential VMs
  
  Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui
  
  OSDI 2024 | July 2024
  
  Jay Lepreau Best Paper Award
  
  Awarded Best Paper!
  
  Publication Github 项目
- Leveraging Large Language Models for Automated Proof Synthesis in Rust
  
  Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
  
  arXiv:2311.03739 | November 2023
  
  Publication
- Core slicing: closing the gap between leaky confidential VMs and bare-metal cloud
  
  Ziqiao Zhou, Yizhou Shan, Weidong Cui, Xinyang Ge, Marcus Peinado, Andrew Baumann
  
  17th USENIX Symposium on Operating Systems Design and Implementation | July 2023
  
  Publication
- Interpretable Noninterference Measurement and Its Application to Processor Designs
  
  Ziqiao Zhou, Michael K. Reiter
  
  Object-Oriented Programming Systems, Languages, and Applications | October 2021
  
  DOI
- Static Evaluation of Noninterference Using Approximate Model Counting
  
  Ziqiao Zhou, Zhiyun Qian, Michael K. Reiter, Yinqian Zhang
  
  2018 IEEE Symposium on Security and Privacy | April 2018
  
  DOI Publication
- A Software Approach to Defeating Side Channels in Last-Level Caches
  
  Ziqiao Zhou, Michael K. Reiter, Yinqian Zhang
  
  2016 Computer and Communications Security | October 2016
  
  DOI Publication
- Fingerprint-free tracking with dynamic enhanced field division
  
  Qingquan Zhang, Ziqiao Zhou, Wei Xu, Jing Qi, Chenxi Guo, Ping Yi, Ting Zhu, Sheng Xiao
  
  2015 International Conference on Computer Communications | August 2015
  
  DOI Publication

Ziqiao Zhou

论文与出版物

AutoVerus: Automated Proof Generation for Rust Code

VeriSMo: A Verified Security Module for Confidential VMs

Leveraging Large Language Models for Automated Proof Synthesis in Rust

Core slicing: closing the gap between leaky confidential VMs and bare-metal cloud

Interpretable Noninterference Measurement and Its Application to Processor Designs

Static Evaluation of Noninterference Using Approximate Model Counting

A Software Approach to Defeating Side Channels in Last-Level Caches

Fingerprint-free tracking with dynamic enhanced field division

AutoVerus: Automated Proof Generation for Rust Code

AutoVerus: Automated Proof Generation for Rust Code

Interpretable Noninterference Measurement and Its Application to Processor Designs

AutoVerus: Automated Proof Generation for Rust Code

Fingerprint-free tracking with dynamic enhanced field division

VeriSMo: A Verified Security Module for Confidential VMs

Leveraging Large Language Models for Automated Proof Synthesis in Rust

Core slicing: closing the gap between leaky confidential VMs and bare-metal cloud

Interpretable Noninterference Measurement and Its Application to Processor Designs

Static Evaluation of Noninterference Using Approximate Model Counting

A Software Approach to Defeating Side Channels in Last-Level Caches

AutoVerus: Automated Proof Generation for Rust Code

VeriSMo: A Verified Security Module for Confidential VMs

Leveraging Large Language Models for Automated Proof Synthesis in Rust

Core slicing: closing the gap between leaky confidential VMs and bare-metal cloud

Interpretable Noninterference Measurement and Its Application to Processor Designs

Static Evaluation of Noninterference Using Approximate Model Counting

A Software Approach to Defeating Side Channels in Last-Level Caches

Fingerprint-free tracking with dynamic enhanced field division

联系 Ziqiao Zhou

Microsoft Research Lab – Redmond