Flux：防锈液体
Flux: Liquid Types for Rust
摘要：
我们介绍Flux，它展示了逻辑改进如何与Rust的所有权机制一起工作，以产生符合人体工程学的基于类型的低级指针操作程序的验证。首先，我们为Rust设计了一个新的精炼类型系统，该系统索引可变位置，纯（不可变）值可以出现在精炼中，然后利用Rust的所有权机制来抽象Rust多态类型构造函数中位置的子结构推理，同时支持强更新。我们通过利用堆叠借用别名模型来形式化对Rust的强别名保证的关键依赖，以证明“良好类型程序的良好借用评估不会卡住”。其次，我们在Flux中实现了我们的类型系统，Flux是Rust编译器的一个插件，它利用复杂不变量到类型和细化的因素来有效地合成循环注释-包括描述容器内容的复杂量化不变量-通过液体推理。第三，我们评估通量与基准套件的向量操作程序和部分先前验证的安全沙箱库，以证明在最先进的Prusti验证器中实现的程序逻辑的优势，细化类型。虽然Prusti更具表现力的程序逻辑通常可以验证深层功能正确性规范，但对于我们的基准测试所涵盖的轻量级但普遍存在的重要验证用例，液体类型使验证符合人体工程学，将规范行削减了两倍，验证时间减少了一个数量级，注释开销从代码大小的24%（平均9%）减少到根本没有。
英文摘要：
We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rust that indexes mutable locations, with pure (immutable) values that can appear in refinements, and then exploits Rust's ownership mechanisms to abstract sub-structural reasoning about locations within Rust's polymorphic type constructors, while supporting strong updates. We formalize the crucial dependency upon Rust's strong aliasing guarantees by exploiting the stacked borrows aliasing model to prove that ``well-borrowed evaluations of well-typed programs do not get stuck''. Second, we implement our type system in Flux, a plug-in to the Rust compiler that exploits the factoring of complex invariants into types and refinements to efficiently synthesize loop annotations -- including complex quantified invariants describing the contents of containers -- via liquid inference. Third, we evaluate Flux with a benchmark suite of vector manipulating programs and parts of a previously verified secure sandboxing library to demonstrate the advantages of refinement types over program logics as implemented in the state-of-the-art Prusti verifier. While Prusti's more expressive program logic can, in general, verify deep functional correctness specifications, for the lightweight but ubiquitous and important verification use-cases covered by our benchmarks, liquid typing makes verification ergonomic by slashing specification lines by a factor of two, verification time by an order of magnitude, and annotation overhead from up to 24% of code size (average 9%) to nothing at all.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
