Flux: Liquid Types for Rust
Flux: Liquid Types for Rust
复制标题
助焊剂：用于防锈的液体类型
DOI：
10.1145/3591283
复制
发表时间：
2023
影响因子：
--
通讯作者：
Jhala, Ranjit
中科院分区：
文献类型：
--
作者：
Lehmann, Nico;Geller, Adam T.;Vazou, Niki;Jhala, Ranjit
我们介绍Flux，它展示了逻辑改进如何与Rust的所有权机制一起工作，以产生符合人体工程学的基于类型的低级指针操作程序的验证。首先，我们为Rust设计了一个新的精炼类型系统，该系统索引可变位置，纯（不可变）值可以出现在精炼中，然后利用Rust的所有权机制来抽象Rust多态类型构造函数中位置的子结构推理，同时支持强更新。我们通过利用Stacked Borrows别名模型来证明“良好类型程序的良好借用评估不会卡住”，从而形式化了对Rust强别名保证的关键依赖。其次，我们在Flux中实现了我们的类型系统，Flux是Rust编译器的一个插件，它利用复杂不变量到类型和细化的因素来有效地合成循环注释-包括描述容器内容的复杂量化不变量-通过液体推理。第三，我们评估通量与基准套件的向量操作程序和部分先前验证的安全沙箱库，以证明在最先进的Prusti验证器中实现的程序逻辑的优势，细化类型。虽然Prusti的更具表现力的程序逻辑通常可以验证深层功能正确性规范，但对于我们的基准测试所涵盖的轻量级但普遍存在且重要的验证用例，Liquid typing通过将规范行削减两倍，验证时间减少一个数量级，并且注释开销高达代码大小的24%，从而使验证符合人体工程学（平均14%），一点也不。
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 14%), to nothing at all.
登录
查看更多内容
DOI：
10.1109/sp46215.2023.10179357
发表时间：
2023-05
期刊：
2023 IEEE Symposium on Security and Privacy (SP)
影响因子：
--
作者：
Evan Johnson;Evan Laufer;Zijie Zhao;D. Gohman;Shravan Narayan;S. Savage;D. Stefan;Fraser Brown-Fraser-Brow
通讯作者：
Evan Johnson;Evan Laufer;Zijie Zhao;D. Gohman;Shravan Narayan;S. Savage;D. Stefan;Fraser Brown-Fraser-Brow
通过状态视图使用指针进行安全编程
DOI：
--
发表时间：
2005
期刊：
International Symposium on Practical Aspects of Declarative Languages
影响因子：
--
作者：
Dengping Zhu;H. Xi
通讯作者：
H. Xi
Aeneas：通过功能翻译进行 Rust 验证
DOI：
--
发表时间：
2022
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Son Ho;Jonathan Protzenko
通讯作者：
Jonathan Protzenko
触发选择策略以稳定程序验证者
DOI：
--
发表时间：
2016
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
K. Leino;Clément Pit
通讯作者：
Clément Pit
DOI：
10.1145/3453483.3454036
发表时间：
2021-06
期刊：
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Michael Sammler;Rodolphe Lepigre;R. Krebbers;Kayvan Memarian;Derek Dreyer;D. Garg
通讯作者：
Michael Sammler;Rodolphe Lepigre;R. Krebbers;Kayvan Memarian;Derek Dreyer;D. Garg