SHF: Small: Integrating separation logic and SMT for better heap verification

SHF：小型：集成分离逻辑和 SMT 以实现更好的堆验证

• 批准号: 1320583
• 负责人: Thomas Wies
• 金额: $ 50万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1320583&HistoricalAwards=false
• 关键词: SHF; Small; Integrating; separation; logic

Heap-allocated pointer structures are a common source of software errors. In particular, pointer safety errors, like memory leaks and dereferencing null or dangling pointers, often cause programs to fail or leave them vulnerable to be exploited by malware. Tools that are able to detect such errors at compile time have long been considered impractical because they scale badly to large programs. This has started to change recently with the advent of verification tools based on separation logic (SL), which scale to software components of industrial size. The aim of this project is to increase the degree of automation, precision, and soundness of today's SL-based verification tools and broaden the scope of tools that could use separation logic. Because heap-allocated data structures are among the most difficult software constructs to reason about, this work has the potential to make a significant impact on the reliability of software.SL-based tools depend on theorem provers for separation logic to automatically discharge proof obligations concerned with properties about pointer structures. Today's tools implement tailor-made provers for this task. However, the analysis of real-world programs involves reasoning about other data types including, for instance, integers, arrays, and bit-vectors. To cope with this, existing separation logic tools make simplifying (and in general unsound) assumptions, rely on interactive help from the user, or implement ad-hoc and incomplete extensions of their tailor-made provers. The PIs will investigate a more systematic approach towards combined reasoning about heap and other data types by integrating an SL theorem prover into a satisfiability modulo theories (SMT) solver. This research is motivated by the observation that reasoning about separation logic fragments can be reduced entirely to reasoning in decidable first-order theories that fit well into the SMT framework. Modern SMT solvers implement decision procedures for many first-order theories that are relevant in program verification, such as linear arithmetic, arrays, and bit-vectors. A reduction to first-order logic enables a seamless combination of separation logic with these theories. Moreover, SMT solvers are already an integral part in the tool chain of many existing verification tools. These tools could directly benefit from an integrated SL prover. In addition, we expect that specific capabilities added to the SMT solver as a result of the project will be useful to a broad set of SMT users.

堆分配的指针结构是软件错误的常见来源。特别是，指针安全错误，如内存泄漏和解引用空指针或悬空指针，经常导致程序失败或使它们容易被恶意软件利用。能够在编译时检测此类错误的工具长期以来被认为是不切实际的，因为它们很难扩展到大型程序。最近，随着基于分离逻辑（SL）的验证工具的出现，这种情况开始发生变化，这种工具可以扩展到工业规模的软件组件。这个项目的目的是增加自动化的程度，精度，以及今天基于sl的验证工具的可靠性，并扩大可以使用分离逻辑的工具的范围。因为堆分配的数据结构是最难理解的软件结构之一，所以这项工作有可能对软件的可靠性产生重大影响。基于语言的工具依赖于分离逻辑的定理证明程序来自动履行与指针结构的属性有关的证明义务。今天的工具为这项任务实现了量身定制的证明程序。但是，对实际程序的分析涉及到对其他数据类型的推理，例如整数、数组和位向量。为了解决这个问题，现有的分离逻辑工具简化了（通常是不健全的）假设，依赖于用户的交互式帮助，或者实现定制的证明程序的特别的和不完整的扩展。pi将研究一种更系统的方法，通过将SL定理证明器集成到可满足模理论（SMT）求解器中，来对堆和其他数据类型进行组合推理。这项研究的动机是观察到关于分离逻辑片段的推理可以完全简化为适合SMT框架的可决定的一阶理论的推理。现代SMT求解器实现了许多与程序验证相关的一阶理论的决策过程，例如线性算法、数组和位向量。还原为一阶逻辑使分离逻辑与这些理论无缝结合。此外，SMT求解器已经成为许多现有验证工具的工具链中不可或缺的一部分。这些工具可以直接受益于集成的SL证明程序。此外，我们期望作为项目的结果添加到SMT求解器中的特定功能将对广泛的SMT用户有用。