Scientists from the French research institute Inria, in collaboration with Microsoft, have developed an automated method for converting C code into secure Rust code, aiming to address the growing demand for memory safety.
The C programming language, created in the 1970s, has become the foundation of numerous critical systems, applications, and libraries, including the Linux kernel. However, C, along with its natural successor, C++, lacks built-in memory safety. Its manual memory management, while offering flexibility and efficiency, is prone to errors such as out-of-bounds access or use-after-free vulnerabilities.
These errors constitute a significant portion of software vulnerabilities. For instance, in 2019, they accounted for 76% of Android vulnerabilities. However, with the adoption of Rust and its safety features, this figure dropped to 24% by 2024.
Rust allows developers to write both safe and unsafe code, giving them the freedom to choose. In contrast, C and C++ require extensive measures like static analysis and rigorous testing to approximate memory safety, yet fail to guarantee it intrinsically.
In recent years, there has been a strong push to adopt languages with built-in memory safety, such as Rust, Go, Python, and Java. Nevertheless, some developers continue to seek ways to use C and C++ securely, avoiding a complete transition to Rust. Even Google, a prominent advocate for Rust, acknowledges that C and C++ will remain in use for many years to come.
Among efforts to enhance C’s safety are projects like TrapC and Fil-C. The former focuses on creating a safer subset of the language, while the latter, although providing safety, compromises performance and lacks full compatibility with application binary interfaces.
A study titled “Compiling C into Safe Rust,” authored by Aymeric Fromherz (Inria) and Jonathan Protzenko (Microsoft), proposes an alternative approach. The researchers concentrate on translating formally verified industrial code into safe Rust. To achieve this, they devised a C subset called Mini-C, which avoids complex constructs such as pointer arithmetic and implicit mutability that are difficult to translate.
By applying Mini-C through the KaRaMeL compiler, developers achieve automated conversion of code into secure Rust. For example, the HACL cryptography library, comprising 80,000 lines of code, was translated with minimal modifications. The EverParse serialization library, with 1,400 lines of code, was transformed seamlessly without any changes. Remarkably, the performance of the resulting Rust code remained on par with the original C, despite the inclusion of additional checks and enhancements.
The fruits of this research are already being applied in real-world security contexts. For instance, the Rust version of HACL has recently been integrated into Mozilla NSS and OpenSSH libraries.
