7/15/2025 The University of Wisconsin-Madison and The Grainger College of Engineering
Written by The University of Wisconsin-Madison and The Grainger College of Engineering
Varun Chandrasekaran, an Illinois Grainger professor of electrical & chemical engineering, is among a team of researchers who have received a $5 million grant from the Defense Advanced Research Projects Agency (DARPA) to convert legacy C codebases to the Rust programming language.
The C programming language—powering everything from operating systems to aircraft control software—has long been a cornerstone of modern computing. But its flexibility comes at a cost: memory safety issues, like buffer overflows and dangling pointers, continue to plague high-assurance systems with critical vulnerabilities, and users must constantly update their systems to avoid becoming victims of attacks.
To tackle this systemic risk, a team of researchers from the University of Illinois; the University of Wisconsin–Madison; the University of California, Berkeley; and the University of Edinburgh has received a DARPA-issued award under its Translating All C to Rust (TRACTOR) program. The team’s goal is to create automated tools that can safely and verifiably convert legacy C codebases into the memory-safe Rust programming language without sacrificing performance or functionality.
Their approach, Formally-Verified Compositional Lifting of C to Rust (ForCLift), uses Verified Lifting, which combines formal methods and program analysis with AI techniques such as Large Language Models to create accurate translations of complex C code into safe, idiomatic Rust. The approach seeks to enable formal verification of the translated code while also preserving performance-critical behavior.
Chandrasekaran, a co-investigator of the ForCLift project, believes Illinois is well positioned to contribute.
“Illinois sits at the forefront of AI and systems security research,” Chandrasekaran said. “Our unique strength lies in combining advances in machine learning with rigorous security and verification methods, making us especially well-equipped to build AI-driven tools that are both powerful and trustworthy.”
Somesh Jha, a University of Wisconsin–Madison professor of computer sciences and lead investigator of the ForCLift project, identifies memory safety as one of the most persistent and costly sources of vulnerabilities in low-level software. “This project is about more than rewriting code — it’s about fundamentally making our software base robust and secure,” Jha said.
Sanjit Seshia, a professor of electrical engineering and computer sciences at UC Berkeley and co-investigator of the initiative, emphasizes the challenge of ensuring that translation preserves the relevant semantics of the program. “The translated Rust program must preserve the core functionality of the original C program and also satisfy desired security properties,” Seshia said. “Formally verifying the correctness of the translation can be challenging, and requires a modular approach where verification is integrated with program synthesis and data-driven AI.”
“While we have demonstrated Verified Lifting for several application domains, extending the approach to translate C to Rust is still a complex and unsolved problem,” said Alvin Cheung, a UC Berkeley professor of electrical engineering and computer sciences and fellow co-investigator.
To manage this complexity, the team is developing formal semantic models of both C and Rust, along with an integrated suite of verification and synthesis tools that can certify the correctness of the transformation. Their system will target critical infrastructure domains, including aerospace, automotive, and defense.
“Much of today’s critical infrastructure runs on C, and rewriting it manually is infeasible at scale,” said Elizabeth Polgreen, a professor of informatics at the University of Edinburgh and co-investigator of the project. “By combining formal methods with machine-learning driven translation tools, our research aims to develop tools that are not only more trustworthy than human translations but also feasible to apply at scale.”
A central goal is not only correctness but also usability. The team’s pipeline will incorporate developer feedback and iterative refinement to ensure that the resulting Rust code can be maintained by real-world engineering teams.
Chandrasekaran sees even broader potential.
“By building tooling that’s both precise and practical, we hope to lower the barrier for secure software development across domains,” he said. “Not just for defense, but for healthcare, finance, and beyond.”
As the software ecosystem continues to evolve, the researchers say addressing memory safety at its root is essential to creating resilient, next-generation systems.
“The systems we rely on today weren’t built with modern safety guarantees in mind,” Jha said. “But with the right tools, we can retrofit those guarantees into the code that powers our cyber-world.”
The team is made up of the following institutions and researchers:
University of Illinois Urbana-Champaign
Varun Chandrasekaran
University of Wisconsin-Madison
Somesh Jha and Tej Chajed
University of California, Berkeley
Sanjit A. Seshia and Alvin Cheung
University of Edinburgh
Elizabeth Polgreen