Translating legacy code for a safer future: DARPA backs effort to convert C to Rust

The C programming language, which powers 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 Wisconsin–Madison, the University of California, Berkeley, the University of Edinburgh, and the University of Illinois Urbana-Champaign has received a $5 million award from the Defense Advanced Research Projects Agency under its Translating All C to Rust 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.

The team's approach, Formally-Verified Compositional Lifting of C to Rust (which the researchers call 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.

"Memory safety remains one of the most persistent and costly sources of vulnerabilities in low-level software," says Somesh Jha, professor of Computer Sciences at the University of Wisconsin–Madison and lead researcher on the ForCLift project. "This project is about more than rewriting code—it's about fundamentally making our software base robust and secure."

Sanjit Seshia, professor of electrical engineering and computer sciences at UC Berkeley and ForCLift co-principal investigator, 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 says.

"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," says Alvin Cheung, also a ForCLift co-PI and UC Berkeley professor of electrical engineering and computer sciences.

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," says Elizabeth Polgreen, professor of informatics at the University of Edinburgh and ForCLift co-PI.

"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.

Varun Chandrasekaran, professor of electrical and computer engineering at the University of Illinois Urbana-Champaign and ForCLift co-PI, sees broader potential. "By building tooling that's both precise and practical, we hope to lower the barrier for secure software development across domains."

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," says Jha. "But with the right tools, we can retrofit those guarantees into the code that powers our cyber-world."

Provided by University of Wisconsin-Madison