Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compiling C to Safe Rust, Formalized

Aymeric Fromherz, Jonathan Protzenko

TL;DR

This work tackles the problem of migrating existing, formally verified C code to memory-safe Rust without resorting to unsafe blocks. It proposes a data-oriented Mini-C subset and a type-directed translation pipeline, augmented by novel static analyses (split trees for pointer arithmetic and a mutability inference pass) and ownership-aware handling of struct definitions. The approach is implemented in KaRaMeL Lowstar and validated on large-scale codebases, including the 80k-line HACL$^\star$ cryptographic library and the CBOR parser from EverParse, showing that the subset suffices to produce safe Rust code with negligible performance overhead in practice. The results demonstrate that automated, semi-active rewrites can enable memory-safe porting of formally verified C code, preserving performance and enabling integration into Rust ecosystems such as NSS/OpenSSH. The work advances practical migration strategies by balancing automated translation with minimal program rewrites, delivering a pathway to safer, verifiably correct systems software.

Abstract

The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C, and cannot be realistically rewritten by hand. Automatically translating C to Rust is thus an appealing course of action. Several works have gone down this path, handling an ever-increasing subset of C through a variety of Rust features, such as unsafe. While the prospect of automation is appealing, producing code that relies on unsafe negates the memory safety guarantees offered by Rust, and therefore the main advantages of porting existing codebases to memory-safe languages. We instead explore a different path, and explore what it would take to translate C to safe Rust; that is, to produce code that is trivially memory safe, because it abides by Rust's type system without caveats. Our work sports several original contributions: a type-directed translation from (a subset of) C to safe Rust; a novel static analysis based on "split trees" that allows expressing C's pointer arithmetic using Rust's slices and splitting operations; an analysis that infers exactly which borrows need to be mutable; and a compilation strategy for C's struct types that is compatible with Rust's distinction between non-owned and owned allocations. We apply our methodology to existing formally verified C codebases: the HACL* cryptographic library, and binary parsers and serializers from EverParse, and show that the subset of C we support is sufficient to translate both applications to safe Rust. Our evaluation shows that for the few places that do violate Rust's aliasing discipline, automated, surgical rewrites suffice; and that the few strategic copies we insert have a negligible performance impact. Of particular note, the application of our approach to HACL* results in a 80,000 line verified cryptographic library, written in pure Rust, that implements all modern algorithms - the first of its kind.

Compiling C to Safe Rust, Formalized

TL;DR

This work tackles the problem of migrating existing, formally verified C code to memory-safe Rust without resorting to unsafe blocks. It proposes a data-oriented Mini-C subset and a type-directed translation pipeline, augmented by novel static analyses (split trees for pointer arithmetic and a mutability inference pass) and ownership-aware handling of struct definitions. The approach is implemented in KaRaMeL Lowstar and validated on large-scale codebases, including the 80k-line HACL cryptographic library and the CBOR parser from EverParse, showing that the subset suffices to produce safe Rust code with negligible performance overhead in practice. The results demonstrate that automated, semi-active rewrites can enable memory-safe porting of formally verified C code, preserving performance and enabling integration into Rust ecosystems such as NSS/OpenSSH. The work advances practical migration strategies by balancing automated translation with minimal program rewrites, delivering a pathway to safer, verifiably correct systems software.

Abstract

The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C, and cannot be realistically rewritten by hand. Automatically translating C to Rust is thus an appealing course of action. Several works have gone down this path, handling an ever-increasing subset of C through a variety of Rust features, such as unsafe. While the prospect of automation is appealing, producing code that relies on unsafe negates the memory safety guarantees offered by Rust, and therefore the main advantages of porting existing codebases to memory-safe languages. We instead explore a different path, and explore what it would take to translate C to safe Rust; that is, to produce code that is trivially memory safe, because it abides by Rust's type system without caveats. Our work sports several original contributions: a type-directed translation from (a subset of) C to safe Rust; a novel static analysis based on "split trees" that allows expressing C's pointer arithmetic using Rust's slices and splitting operations; an analysis that infers exactly which borrows need to be mutable; and a compilation strategy for C's struct types that is compatible with Rust's distinction between non-owned and owned allocations. We apply our methodology to existing formally verified C codebases: the HACL* cryptographic library, and binary parsers and serializers from EverParse, and show that the subset of C we support is sufficient to translate both applications to safe Rust. Our evaluation shows that for the few places that do violate Rust's aliasing discipline, automated, surgical rewrites suffice; and that the few strategic copies we insert have a negligible performance impact. Of particular note, the application of our approach to HACL* results in a 80,000 line verified cryptographic library, written in pure Rust, that implements all modern algorithms - the first of its kind.

Paper Structure

This paper contains 28 sections, 2 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Artifact Submission.
  3. Translating Mini-C to Safe Rust
  4. Type Translation
  5. Type-Directed Translation of Expressions
  6. Translating Array Allocations.
  7. Pointers and Array Accesses.
  8. Conversions Between Rust Abstractions.
  9. Function Calls.
  10. Handling Pointer Arithmetic
  11. Split Trees.
  12. Symbolic Solver.
  13. Limitations.
  14. Generalizing to Whole Programs: Struct Definitions and Function Declarations
  15. Tuples as structural types.
  16. ...and 13 more sections

Figures (9)

  • Figure 1: Grammar of mini-C types, statements and expressions
  • Figure 2: Grammar of Rust types and expressions. The $^?$ denotes optional syntax.
  • Figure 3: Translation from Mini-C to Rust: types
  • Figure 4: Translation from Mini-C to Rust: selected statements and expressions
  • Figure 5: Successive split trees during C translation. Internal nodes of the form (x, i) have been subjected to a split at Rust index i and are therefore borrowed at this program point. Leaf nodes are available.
  • ...and 4 more figures