Recent work directed by professors Ronghui Gu and Jason Nieh introduced a new tool, Spoq, that significantly reduces the complex efforts people must use to verify real-world software and makes it possible to verify existing C systems code without modifications. Formal verification offers a systematic and rigorous approach to software and hardware verification, helping to ensure that systems behave correctly and meet their intended specifications. With Spoq, many aspects of formal verification can be automated, significantly reducing manual proof efforts for verification. The paper was presented at the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) Conference on July 12, 2023.

Why it matters

System software forms the software foundations of our computing infrastructure. Modern system software is large, complex, and imperfect, with vulnerabilities that can be exploited to compromise the security of a system. Formal verification offers a potential solution to this problem by mathematically proving that system software can provide critical security guarantees. Unfortunately, it remains too difficult and requires too much human effort to apply in practice.

Previous tools developed by Nieh’s and Gu’s teams introduced verification techniques to make certain proofs possible that could not have been done before. Spoq’s key feature is that it automates the tedious and time-consuming parts of many proofs. “Spoq can generate results in about an hour compared to doing it manually, which can take months or years to formally verify a system,” says Xupeng Li, the paper's lead author and a PhD student with both Nieh and Gu.

What's next

Over the next few months, the lab is focused on making Spoq open-source so that formal verification can be widely deployed to secure the foundations of our computing infrastructure's software.

About the Study

Conference: 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) Conference (July 10-12, 2023, Boston, MA)

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

Authors: Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh, Columbia Engineering

Funding: This work was supported in part by three Amazon Research Awards, a Guggenheim Fellowship, a VMware Systems Research Award, an NSF CAREER Award, DARPA contract N66001-21-C-4018, and NSF grants CCF-1918400, CNS-2052947, and CCF-2124080. 

COI: Ronghui Gu is the founder of and has an equity interest in CertiK.

Header image: Tang Family Assistant Professor of Computer Science Rongui Gu (left) and Professor of Computer Science Jason Nieh (right).