RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code
RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code
复制标题
DOI：
10.1145/3519939.3523704
复制
发表时间：
2022-06
期刊：
影响因子：
--
通讯作者：
Yusuke Matsushita;Xavier Denis;Jacques-Henri Jourdan;Derek Dreyer
中科院分区：
文献类型：
--
作者：
Yusuke Matsushita;Xavier Denis;Jacques-Henri Jourdan;Derek Dreyer
Rust是一种系统编程语言，通过禁止别名状态突变的强大所有权类型系统，提供低级内存操作和高级安全保证。在以前的工作中，Matsushita et al.开发了RustHorn，这是一种很有前途的Rust代码功能验证技术：它利用Rust类型的强大不变量来用一阶逻辑(FOL)公式来表达有状态Rust代码的行为，其验证服从于现成的自动化技术。RustHorn的关键思想是使用预言来描述可变借入的行为。然而，RustHorn的健壮性只是针对Rust的一个安全子集建立的，并且还不清楚如何扩展它以支持封装不安全代码的各种安全API(即，放松Rust别名规则的代码)。在本文中，我们提出了RustHornBelt，它是RustHorn风格验证的第一个机器检查的可靠性证明，它支持给用不安全代码实现的安全API提供FOL规范。RustHornBelt使用了Jung等人的S RustBelt框架中使用的语义类型方法，但它扩展了RustBelt的模型，不仅考虑了安全性，还考虑了功能的正确性。RustHornBelt的关键挑战是开发RustHorn风格的预测的语义模型，我们通过一种新的分离逻辑机制来实现，我们称之为参数预测。
Rust is a systems programming language that offers both low-level memory operations and high-level safety guarantees, via a strong ownership type system that prohibits mutation of aliased state. In prior work, Matsushita et al. developed RustHorn, a promising technique for functional verification of Rust code: it leverages the strong invariants of Rust types to express the behavior of stateful Rust code with first-order logic (FOL) formulas, whose verification is amenable to off-the-shelf automated techniques. RustHorn’s key idea is to use prophecies to describe the behavior of mutable borrows. However, the soundness of RustHorn was only established for a safe subset of Rust, and it has remained unclear how to extend it to support various safe APIs that encapsulate unsafe code (i.e., code where Rust’s aliasing discipline is relaxed). In this paper, we present RustHornBelt, the first machine-checked proof of soundness for RustHorn-style verification which supports giving FOL specs to safe APIs implemented with unsafe code. RustHornBelt employs the approach of semantic typing used in Jung et al.’s RustBelt framework, but it extends RustBelt’s model to reason not only about safety but also functional correctness. The key challenge in RustHornBelt is to develop a semantic model of RustHorn-style prophecies, which we achieve via a new separation-logic mechanism we call parametric prophecies.