A research collaboration led by the Universities of Wisconsin-Madison, California, Berkeley, Edinburgh, and Illinois Urbana-Champaign has secured a $5 million award from DARPA to develop automated tools converting legacy C code into the Rust programming language. The project, utilising a technique called Formally-Verified Compositional Lifting of C to Rust (ForCLift), aims to create memory-safe Rust code without sacrificing performance, addressing a significant source of vulnerabilities in critical infrastructure domains including aerospace, automotive, and defense. Researchers will combine formal verification methods with AI techniques, seeking to certify the correctness of the translation and enable scalable application of the tools, while also incorporating developer feedback to ensure usability.
Automated Code Translation and Security
The project has received $5 million in funding from the Defense Advanced Research Projects Agency (DARPA) under the Translating All C to Rust (TRACTOR) program, with the stated goal of creating automated tools for converting legacy C codebases into the memory-safe Rust programming language. The research team’s approach, Formally-Verified Compositional Lifting of C to Rust (ForCLift), utilises Verified Lifting, combining formal methods, program analysis, and AI techniques, including Large Language Models, to achieve accurate translations. Preserving performance and functionality while ensuring safe conversion is a key objective of this automated translation process.
A central challenge lies in ensuring the translated Rust program preserves the core functionality of the original C program and satisfies desired security properties; the team is therefore developing formal semantic models of both C and Rust. These models will be integrated with a suite of verification and synthesis tools designed to certify the correctness of the transformation process, employing a modular approach to formal verification. The research aims to produce tools that are not only more trustworthy than human translations but also feasible for application at scale, given the impracticality of manually rewriting extensive C codebases.
The project will target critical infrastructure domains, including aerospace, automotive, and defense, recognising the prevalence of C code in these sectors. The team intends to incorporate developer feedback and iterative refinement into its pipeline to ensure the resulting Rust code is maintainable by real-world engineering teams. This focus on usability is intended to lower the barrier to secure software development across multiple domains, addressing memory safety at its root to create resilient, next-generation systems.
Formal Verification and System Architecture
To manage the complexity of the translation process, the research team is developing formal semantic models of both C and Rust, alongside an integrated suite of verification and synthesis tools that can certify the correctness of the transformation. This system will employ a modular approach where verification is integrated with program synthesis and data-driven AI, enabling formal verification of the translated code while also preserving performance-critical behaviour.
The research aims to develop tools that are not only more trustworthy than human translations but also feasible to apply at scale, recognising that much of today’s critical infrastructure runs on C and manual rewriting is infeasible. The project will specifically target critical infrastructure domains, including aerospace, automotive, and defense, where C code is widely deployed.
A central goal of the project is 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. By building tooling that is both precise and practical, the researchers hope to lower the barrier for secure software development across domains, ultimately addressing memory safety at its root to create resilient, next-generation systems.
Research Collaboration and Project Goals
The research team comprises researchers from the University of Wisconsin-Madison (Somesh Jha and Tej Chajed), the University of California, Berkeley (Sanjit A. Seshia and Alvin Cheung), the University of Illinois Urbana-Champaign (Varun Chandrasekaran), and the University of Edinburgh (Elizabeth Polgreen).
Ensuring that translation preserves the relevant semantics of the program is a key challenge; the translated Rust program must preserve the core functionality of the original C program and also satisfy desired security properties. 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.
Formally verifying the correctness of the translation requires a modular approach where verification is integrated with program synthesis and data-driven AI, enabling formal verification of the translated code while also preserving performance-critical behaviour. The research aims to develop tools that are not only more trustworthy than human translations but also feasible to apply at scale, given the impracticality of manually rewriting extensive C codebases.
More information
External Link: Click Here For More
