Enabling Developers to Write Provably Correct Software

Monday, November 18, 2024 - by Krista Burns

Computer code is the foundation of technology today. As software becomes an increasingly pervasive part of our lives, we need ways to ensure that critical software systems remain free of certain classes of defects and vulnerabilities.

Bryan Parno, the Kavčić-Moura Professor of Electrical & Computer Engineering and Computer Science, along with Marijn Heule and Ruben Martins, professors in the computer science department, and Jeremy Avigad, a professor in the philosophy department, are focusing on just that. The team of Carnegie Mellon University (CMU) researchers received a Defense Advanced Research Projects Agency (DARPA) research grant from the Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program to make it possible for non-experts to formally prove that their code is correct, reliable, and secure. As part of the PROVERS program, the CMU team is collaborating with an international team of experts at several companies and universities.

“Our team is creating tools and techniques to enable scalable verification of critical software components,” explains Parno. “We want to ensure that the code that forms our digital infrastructure lives up to people’s expectations. The goal of our work, and the PROVERS program, is to make these verification tools accessible to a broad community of developers.”

The Carnegie Mellon researchers are developing a tool called Verus for mathematically proving the correctness, reliability, and security of code written in the Rust programming language. To discharge those proofs, Verus uses various reasoning engines, including the Lean theorem prover and Satisfaction Modulo Theory (SMT) solvers.

“Our tools take a mathematical specification of what code is intended to do, like encrypt messages or sort messages, then they convert the code itself into a mathematical representation, and finally they check whether the code will obey the specification for all possible inputs,” says Parno. “If that check passes, we know that the code will behave as intended.”

Engineering practices for software-reliant systems have evolved steadily over many decades, and so too have the assurance techniques that confirm systems’ correctness and security. As just one of DARPA’s research programs, the PROVERS program will develop formal methods tools to guide software engineers through designing proof-friendly software systems and to reduce the proof repair workload.

"The interdisciplinary nature of Carnegie Mellon University strengthens our contribution to the PROVERS program,” says Parno. “Our team is made up of experts from CMU’s computer engineering, computer science, and philosophy departments. By approaching software problems through a diverse lens, I believe our team will provide a unique perspective on this research."

Media Contact:

Krista Burns