好色先生TV

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.

, the Kav膷i膰-Moura Professor of Electrical & Computer Engineering and Computer Science, along with and , professors in the Computer Science Department, and Jeremy Avigad, a professor in the Philosophy Department, are focusing on just that. The team of 好色先生TV (CMU) researchers received a research grant from the 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.

鈥淥ur team is creating tools and techniques to enable scalable verification of critical software components,鈥� explains Parno. 鈥淲e want to ensure that the code that forms our digital infrastructure lives up to people鈥檚 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.

鈥淥ur 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. 鈥淚f 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鈥檚 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 好色先生TV strengthens our contribution to the PROVERS program,鈥� says Parno. 鈥淥ur team is made up of experts from CMU鈥檚 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."