Linear types for large-scale systems verification
Linear types for large-scale systems verification
复制标题
用于大规模系统验证的线性类型
DOI：
10.1145/3527313
复制
发表时间：
2022
影响因子：
--
通讯作者：
Hawblitzel, Chris
中科院分区：
文献类型：
--
作者：
Li, Jialin;Lattuada, Andrea;Zhou, Yi;Cameron, Jonathan;Howell, Jon;Parno, Bryan;Hawblitzel, Chris
在软件验证中，内存混淆和变异的推理是一个难题。这对于使用基于SMT的自动定理证明器的系统尤其如此。SMT验证中的内存推理通常需要大量的手动工作来指定堆不变量，以及SMT求解器的大量别名推理。在本文中，我们提出了一种混合的方法，结合线性类型与基于SMT的验证记忆推理。我们将线性类型集成到Dafny中，Dafny是一种具有SMT后端的验证语言，并表明这两种方法相互补充。通过将内存推理与验证条件分离，线性类型减少了SMT求解时间。同时，SMT查询的表达能力扩展了线性类型系统的灵活性。特别是，它允许我们的线性类型系统以新颖的方式轻松正确地混合线性和非线性数据，将线性数据封装在非线性数据中，反之亦然。我们正式我们的扩展的核心，证明合理性，并提供线性类型检查的算法。我们评估我们的方法，通过转换的验证存储系统（约24K行的代码和证明）在Dafny编写的实现，使用我们的扩展Dafny。结果系统使用线性类型的91%的代码和基于SMT的堆推理的其余9%。我们发现，转换后的系统有28%的证明线和30%的验证时间缩短整体。我们讨论了由于基于SMT的堆推理而导致的原始系统中的开发开销，并强调了使用线性类型时改进的开发人员体验。
Reasoning about memory aliasing and mutation in software verification is a hard problem. This is especially true for systems using SMT-based automated theorem provers. Memory reasoning in SMT verification typically requires a nontrivial amount of manual effort to specify heap invariants, as well as extensive alias reasoning from the SMT solver. In this paper, we present a hybrid approach that combines linear types with SMT-based verification for memory reasoning. We integrate linear types into Dafny, a verification language with an SMT backend, and show that the two approaches complement each other. By separating memory reasoning from verification conditions, linear types reduce the SMT solving time. At the same time, the expressiveness of SMT queries extends the flexibility of the linear type system. In particular, it allows our linear type system to easily and correctly mix linear and nonlinear data in novel ways, encapsulating linear data inside nonlinear data and vice-versa. We formalize the core of our extensions, prove soundness, and provide algorithms for linear type checking. We evaluate our approach by converting the implementation of a verified storage system (about 24K lines of code and proof) written in Dafny, to use our extended Dafny. The resulting system uses linear types for 91% of the code and SMT-based heap reasoning for the remaining 9%. We show that the converted system has 28% fewer lines of proofs and 30% shorter verification time overall. We discuss the development overhead in the original system due to SMT-based heap reasoning and highlight the improved developer experience when using linear types.
登录
查看更多内容
动态框架：支持无限制的框架、依赖和共享
DOI：
--
发表时间：
2006
期刊：
World Congress on Formal Methods
影响因子：
--
作者：
Ioannis T. Kassios
通讯作者：
Ioannis T. Kassios
Steel：依赖类型并发分离逻辑中的面向证明编程
DOI：
--
发表时间：
2021
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Aymeric Fromherz;Aseem Rastogi;N. Swamy;Sydney Gibson;Guido Martínez;Denis Merigoux;T. Ramananandro
通讯作者：
T. Ramananandro
DOI：
--
发表时间：
2021
期刊：
--
影响因子：
--
作者：
Ankit Bhardwaj;C. Kulkarni;Reto Achermann;I. Calciu;Sanidhya Kashyap;Ryan Stutsman;Amy Tai;Gerd Zellweger
通讯作者：
Ankit Bhardwaj;C. Kulkarni;Reto Achermann;I. Calciu;Sanidhya Kashyap;Ryan Stutsman;Amy Tai;Gerd Zellweger
DOI：
--
发表时间：
2020
期刊：
--
影响因子：
--
作者：
Vikram Narayanan;Tianjiao Huang;David Detweiler;Daniel M. Appel;Zhaofeng Li;Gerd Zellweger;A. Burtsev
通讯作者：
Vikram Narayanan;Tianjiao Huang;David Detweiler;Daniel M. Appel;Zhaofeng Li;Gerd Zellweger;A. Burtsev
SteelCore：用于有效依赖类型程序的可扩展并发分离逻辑
DOI：
--
发表时间：
2020
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
N. Swamy;Aseem Rastogi;Aymeric Fromherz;Denis Merigoux;Danel Ahman;Guido Martínez
通讯作者：
Guido Martínez