CRISP & CLEAR

Challenge

Most existing software systems are built on legacy C code that is highly vulnerable to memory safety exploits. While migrating these systems to a memory-safe language like Rust is the ideal fix, this process is currently far too expensive and labor-intensive for almost all real-world use cases. Existing automated transpilers (like c2rust) can translate C code, but they only output unsafe, unidiomatic, and highly verbose Rust code. Attempting to rely purely on modern AI to rewrite this code leads to compiler errors, token limit issues, and unpredictable "hallucinations."

Solution

Under the DARPA TRACTOR program, Galois and its partners (Immunant, UT Austin, and the University of Pennsylvania) are developing a two-part solution: CRISP and CLEAR. CRISP (C to Rust for Idiomatic and Safe Programming) is an automated transpiler that uses a portfolio of both symbolic and AI tools in a step-by-step refactoring loop to incrementally rewrite C code into safe, idiomatic Rust. CRISP combines LLM-based synthesis with trustworthy symbolic program analysis to strictly guide and validate the translation. To guarantee correctness, the team is also building CLEAR (Concurrent LLVM Equivalence Analysis through Refinement), a rigorous testing tool based on formal LLVM semantics (Vellvm) that formally verifies the behavioral equivalence between the original concurrent C code and the newly generated Rust.

Value Add

• Cost-Effective Legacy Modernization: By fully automating the translation of C to safe Rust, CRISP dramatically lowers the financial and labor barriers required to harden critical legacy systems.
• Maintainable and Safe Output: The step-by-step pipeline moves beyond raw, unsafe translations, instead automatically producing clean, safe, and idiomatic Rust code that human developers can easily maintain.
• Controlled and Reliable AI Integration: By using strict symbolic analysis to guide and prune AI-based rewrites, the system minimizes LLM hallucinations, eliminates token-limit failures, and ensures a highly accurate translation.
• Verifiable and Trustworthy Code Translation: The CLEAR testing tool continuously cross-checks execution traces to mathematically ensure the generated concurrent Rust behaves exactly like the original C program.

‍

This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR00112590133.