将 C 编译为安全的 Rust,形式化

主要观点:Rust 语言日益流行,但许多关键代码库仍用 C 编写且难以手动重写,自动将 C 转译为 Rust 有吸引力,但依赖 unsafe 的代码会抵消 Rust 的内存安全保证,所以探索将 C 转译为安全 Rust 的路径。工作有多个原创贡献,包括从(部分)C 到安全 Rust 的类型导向翻译、基于“分裂树”的新静态分析、精确推断所需可变借用的分析以及与 Rust 非拥有和拥有分配区分兼容的 C 结构类型编译策略,将该方法应用于已验证的 HACL密码库和 EverParse 的二进制解析器及序列化器,表明支持的 C 子集足以将两个应用转译为安全 Rust,评估显示少数违反 Rust 别名规则的地方可通过自动重写解决,插入的少量策略复制对性能影响可忽略,将该方法应用于 HACL得到 80,000 行纯 Rust 验证密码库且实现所有现代算法。
关键信息:Rust 流行但 C 代码难重写,探索安全转译路径及相关贡献,应用于特定代码库及评估结果。
重要细节:提及多个作品通过不同 Rust 特征处理 C 子集,工作中的静态分析基于“分裂树”,编译策略兼容 Rust 分配区分等。

阅读 9
0 条评论