How Researchers Auto-Convert C to Safe Rust: The Mini‑C Approach

Inria and Microsoft computer scientists have designed a method that can automatically convert a subset of C code into safe Rust to meet the growing demand for memory‑safe software.

The C programming language, created in the early 1970s, underpins many critical systems such as the Linux kernel, but like C++, it was not designed for memory safety, relying on manual memory management that can lead to errors such as out‑of‑bounds reads and use‑after‑free bugs.

Recent studies show that memory‑safety bugs account for the majority of software vulnerabilities; for example, they comprised 76% of Android’s 2019 vulnerabilities, and projections suggest that adopting Rust and safe‑coding practices could reduce this figure to 24% by the end of 2024.

While Rust can be written in safe or unsafe modes, C and C++ provide no built‑in memory‑safety guarantees. Industry and governments have therefore been pushing for a shift toward memory‑safe languages like Rust, Go, Python, and Java, though legacy C/C++ code remains pervasive.

Efforts such as DARPA’s TRACTOR, TrapC, and Fil‑C aim to make C more memory‑safe, but each has limitations: TrapC targets only a subset of the language, and Fil‑C incurs performance overhead and lacks full ABI compatibility.

In the paper “Compiling C to Safe Rust, Formally”, authors Aymeric Fromherz (Inria) and Jonathan Protzenko (Microsoft) present an alternative automatic translation that produces safe Rust code. They focus on a restricted C subset named “Mini‑C”, which avoids patterns that cannot be directly mapped to safe Rust, such as pointer arithmetic and implicit mutability.

Using the KaRaMeL compiler framework to implement Mini‑C, the researchers generate safe Rust code that may require minimal source‑code adjustments from the user. Once the code conforms to the supported subset, the translation proceeds automatically, yielding correct and memory‑safe Rust.

The approach was evaluated on the HACL* cryptographic library (≈80,000 lines of C) and the EverParse format‑parsing library (≈1,400 lines of C). HACL* required only minor code changes, while EverParse needed none. The resulting Rust code retained the original performance characteristics despite the addition of fat pointers and runtime bounds checks.

This work enables safer downstream applications; the Rust‑compiled HACL* has been incorporated into the libcrux cryptographic library and portions have been merged into Mozilla’s NSS and OpenSSH projects.