Ronghui Gu (Columbia University): Computer and Information Science Seminar

Title: “Scaling Machine-Checkable Systems Verification in Coq”

Ronghui Gu

Associate Professor, Columbia University

Ronghui Gu is the Tang Family Associate Professor of Computer Science at Columbia University. His thesis work on building certified OS kernels received the Yale Doctoral Dissertation Award. He is the primary designer and developer of CertiKOS, the first verified concurrent OS kernel, and SeKVM, the first verified commodity cloud hypervisor. Gu co-founded CertiK, a Web3 cybersecurity unicorn startup valued at $2 billion. CertiK has collectively served over 4,700 enterprise clients and secured more than $300 billion worth of assets in cryptocurrency. For his work in systems verification, Gu received: an NSF CAREER Award, a VMware Systems Research Award, three Amazon Research Awards, an OSDI Jay Lepreau Best Paper Award, an SOSP Best Paper Award, and a CACM Research Highlight. He obtained his Ph.D. from Yale University in 2016 and a bachelor’s degree from Tsinghua University in 2011.

Research Synopsis:

System software like operating systems and hypervisors forms the critical backbone of our computing infrastructure. However, due to their size and complexity, these systems often contain vulnerabilities that can compromise security. Formal verification offers a solution by mathematically proving software correctness, but its adoption is hindered by the substantial effort required to create these proofs.

In this talk, I will introduce Spoq, a highly automated verification framework designed to dramatically reduce the proof effort in verifying system software. Spoq leverages LLVM to automatically translate C code—including full C semantics like macros, inline assembly, and compiler directives—into Coq, a proof assistant for formal verification. This automation eliminates the need for manual modification of source code prior to verification. Spoq leverages a layering proof strategy and introduces novel Coq tactics and transformation rules to automatically generate layer specifications and refinement proofs to simplify verification of concurrent system software. Spoq also supports easy integration of manually written layer specifications and refinement proofs. We applied Spoq to verify a multiprocessor KVM hypervisor implementation. Verification using Spoq required 70% less proof effort than the manually written specifications and proofs to verify an older implementation. Furthermore, the proofs using Spoq hold for the unmodified implementation that is directly compiled and executed.