VMware is pleased to announce that Ronghui Gu, Tang Family Assistant Professor of Computer Science at Columbia University, is the 2022 early-career VMware Systems Research Award recipient. Professor Gu is recognized for fundamental theory underlying systems verification and for synthesizing the results into realistic bug-free and hacker-resistant systems software. In recognition of his originality, impact, and future potential, the VMware University Research Fund will award Columbia University a gift of USD 125,000 to support Professor Gu’s research.
Computing underpins vital aspects of societal and economic function; therefore, it is increasingly crucial to ensure that software is bug-free and dependable. Professor Gu’s work has involved advances in system verification, which aims to prove that a system meets its requirements in dimensions such as functionality and correctness. Key verification tools include various “formal methods,” which are mathematically rigorous techniques, often involving requirements and implementations expressed in languages that can support meaningful correctness proofs. Historically, the costs, intellectual complexity, lack of scalability, and up-front investment in rigorous verification techniques have been obstacles to their widespread adoption. Because his work helps to address these concerns, Professor Gu’s research contributions have moved the software community closer to the goal of broad adoption of formal methods in some of the most security-sensitive systems under development. Furthermore, his techniques are proving to be helpful in academic clean-slate system designs and in a range of real-world settings requiring high assurance. For these reasons, and because Prof. Gu’s work contributes to an essential dimension of responsible computing, we at VMware are pleased to convey this recognition.
The work for which Professor Gu is best known was his Ph.D. thesis work at Yale University on the certification of the CertiKOS operating system kernel, a challenge involving many complex components ranging from compilers to the OS building blocks themselves. Says his advisor, Professor Zhong Shao, “Certifying an operating system is a huge task, involving models of many components ranging from threads and processes to physical and virtual memory management. Ronghui was a main driver to make the CertiKOS vision become a reality: he addressed the complexity of concurrency, and he got the proofs done for a realistic system.”
Notably, the approach taken in CertiKOS is proving scalable and efficient. Prof. Greg Morrisett, Dean and Vice-Provost of Cornell Tech, says, “I think CertikOS is a tremendous leap forward, not so much in the artifact itself, but rather in the methodology used for constructing the proofs (though the artifact is also cool). It led to literally an order of magnitude reduction in effort/time/person-years compared to SEL4, in spite of the fact that it did something more sophisticated, i.e., dealt with concurrency in the kernel, whereas SEL4 is single-threaded. 20-person-months vs. 20-person-years – that’s a big advance! The secret was finding a way to really modularize the proofs, so that they snapped together. I think this will have a big impact on proof engineering going forward, not just for operating system kernels, but for distributed systems more generally.”
Although it is common wisdom that verification is impractical unless systems are written specifically with verification in mind, Prof. Gu has moved beyond the verification of clean-slate designs with clean-slate interfaces. Says his Columbia colleague Prof. Jason Nieh, “Ronghui showed how small changes to KVM, the commodity hypervisor built in the mainline Linux kernel, make it possible to verify its security properties, specifically protecting the confidentiality and integrity of virtual machines (VMs). Some of the ideas behind his approach have been adopted by industry projects, for example at Arm and in the Ant Group.”
Formal verification is still viewed as practical only for the most sensitive aspects of today’s systems. Recently, “confidential computing” has emerged as a groundbreaking approach to the confidentiality and integrity of data in use. Being a security foundation, confidential computing systems are critical to “get right”. So it is not surprising to see formal verification leveraged in the realm of confidential computing; Ronghui’s work on the Arm “Confidential Computing Architecture” (Arm CCA) project used novel methods of formal verification to help validate security robustness. Says Gareth Stockwell, a systems architect at Arm, “We had drafted a set of desired properties; prior to the collaboration with Ronghui and the team at Columbia University, we believed that a proof of these properties would be pushing the state of the art. Ronghui showed how Mover Oracles could be used to produce such a proof, which is hugely valuable in reinforcing the security properties of Arm CCA, and also improves industry understanding of confidential computing.” This work to retrofit the benefits of formal methods into pre-existing systems without requiring changes to legacy code running on those systems is a testament to the power of Prof. Gu’s underlying approach and his commitment to systems research impact. Says Shoumeng Yan, Senior Director of Secure and Trustworthy Infrastructures in the Ant Group, “SeKVM achieved unprecedented success in rigorous formal verification of large-scale commodity infrastructure software. This was inspirational for the formal verification of HyperEnclave (an open and cross-platform trusted execution environment developed with Rust), which also has a hardware-isolation architecture. Mission-critical code of HyperEnclave has since been verified by building on an SeKVM-inspired approach, utilizing the experience and some common verification components (such as proof library and tactics). Today, HyperEnclave has been put into use in many confidential computing production jobs within Ant Group, which has some of the largest financial confidential computing workload in the world. Based on a software/hardware co-design including HyperEnclave as its core confidential computing layer, Ant Group has also built a dedicated Privacy-preserving Computation Integrated Platform and made successful customer deployments.”
To make verification more practical, Ronghui advanced not only proof techniques, problem decomposition techniques, and systematic approaches to abstraction; he also identified novel ways to simplify the most difficult intellectual challenges of proof generation. One remarkable project with this goal is DuoAI, which shows a data-driven approach to deriving “inductive invariants” for distributed systems. The authors report “DuoAI verifies more than two dozen common distributed protocols automatically, including various versions of Paxos, and outperforms alternative methods both in the number of protocols it verifies and the speed at which it does so, including solving Paxos more than two orders of magnitude faster than previous methods.”
The VMware Systems Research Award celebrates early-career faculty within the first five years of a first tenure-track appointment. In this short window, Ronghui has already emerged as a notable figure in systems research with regular contributions to top systems conferences including 17 papers in recent OSDI, SOSP, PLDI, POPL, and IEEE S&P conferences (including best papers in SOSP and OSDI). His work systematically and thoroughly advances the state-of-the-art in distributed system verification, within academia and industry. “Ronghui’s work represents an important data point in the evolution of formal verification technique,” says VMware Fellow Pratap Subrahmanyam; “Making otherwise esoteric technologies accessible in practical settings is one reason we value Ronghui’s research.” Adds VMware Fellow Christos Karamanolis, “Ronghui’s depth, breadth, and focus on the advancement of formal methods – including both core platforms and emerging areas such as Quantum Computing – is remarkable and representative of the kind of systems research focus we value in making this award.”
This year, the selection committee was chaired by Georgia Tech Dean Charles Isbell and included Professor Anastasia Ailamaki of EPFL (known in English as Swiss Federal Institute of Technology, Lausanne), University of Washington Professor Tom Anderson, UCB Professor Sylvia Ratnasamy, VMware’s Christos Karamanolis, Pratap Subrahmanyam, and Chris Ramming. We see the award as a way to support and give back to the academic research community, which plays a crucial role in exploring new technology.
Comments