Rust 语言的流行度持续飙升，但许多关键代码库仍然是用 C 语言编写的，并且无法通过人工重写的方式进行替换。因此，自动将 C 翻译成 Rust 成为了一种很有吸引力的选择。

一些研究工作已经沿着这条路径发展，通过各种 Rust 特性（例如 unsafe）处理越来越多的 C 子集。虽然自动化的前景很有吸引力，但生成依赖于 unsafe 的代码会否定 Rust 提供的内存安全保证，因此也否定了将现有代码库移植到内存安全语言的主要优势。

相反，本文探索了一条不同的路径，并探讨将 C 翻译成安全 Rust 所需的工作；也就是说，生成代码，因为该代码符合 Rust 的类型系统而没有任何警告，因此代码本身就是内存安全的。本文的工作包含一些原创贡献：从（C 的一个子集）到安全 Rust 的类型导向翻译；一种基于“分裂树”的新型静态分析，允许使用 Rust 的切片和分裂操作来表达 C 的指针算术；一种分析，推断出哪些借用需要是可变的；以及一种与 Rust 区分非拥有和拥有分配兼容的 C 结构体类型的编译策略。

本文将方法应用于现有的正式验证的 C 代码库：HACL* 密码库，以及来自 EverParse 的二进制解析器和序列化器，并表明本文支持的 C 子集足以将这两个应用程序翻译成安全的 Rust。本文的评估表明，对于违反 Rust 别名规则的少数几个地方，自动的手术重写就足够了；并且插入的少数几个策略性复制对性能的影响可以忽略不计。特别值得注意的是，将本文的方法应用于 HACL* 导致了一个用纯 Rust 编写的 80,000 行经过验证的密码库，该库实现了所有现代算法——这是第一款此类库。