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

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

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.