RustBelt: Securing the Foundations of the Rust Programming Language
RustBelt: Securing the Foundations of the Rust Programming Language
复制标题
DOI：
10.1145/3158154
复制
发表时间：
2018-01-01
影响因子：
1.8
通讯作者：
Dreyer, Derek
中科院分区：
文献类型：
--
作者：
Jung, Ralf;Jourdan, Jacques-Henri;Dreyer, Derek
Rust是一种新的系统编程语言，有望克服高级安全保证与对资源管理的低级控制之间看似基本的权衡。不幸的是，Rust的安全要求都没有得到正式证明，并且有充分的理由质疑它们是否真正持有。具体而言，Rust采用了强大的，基于所有权的类型系统，但然后通过内部使用不安全功能的库扩展了该核心类型系统的表现力。在本文中，我们为代表逼真的生锈子集的语言提供了第一个正式（和机器检查）的安全证明。我们的证明是可以扩展的，从某种意义上说，对于使用不安全功能的每个新的Rust库，我们可以说出它必须满足的验证条件，以便将其视为对语言的安全扩展。我们已经对整个Rust生态系统中使用的一些最重要的库进行了验证。
Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.