SaTC: CORE: Small: Sound Automatic Exploit Generation

现代社会依赖于计算机软件。软件系统的安全漏洞越来越多地被利用来泄露用户的机密数据、泄露计算机系统的特权信息、劫持计算机系统进行恶意行为等，对软件系统构成了严重的威胁。当前用于检测可利用的软件漏洞的技术缺乏数学基础，因为它们无法证明检测到的漏洞的可靠性或证明不存在漏洞的类别。该项目将开发能够建立一类与内存相关的可利用软件漏洞的技术。因此，如果一个给定的软件有这样的漏洞，项目的技术就可以保证检测到它们。该项目针对的是源代码可能不完全可用的遗留软件系统，因此针对的是它们的二进制代码。该项目的方法包括将二进制代码转换为一个模型，该模型允许相对容易地推理代码的可利用漏洞。在这样的模型上，该方法的算法计算初始程序值，如果存在这样的值，则可能导致代码的可利用漏洞出现。该方法的每一步都在定理证明器中被数学证明是正确的，定理证明器是一种允许用数学方法证明算法属性的软件工具。该项目的技术将应用于工业强度的生产软件系统，以检测可利用的漏洞，从而证明技术的有效性。项目的结果将通过相关软件安全文献和开放项目工具实现的结果出版物广泛传播。软件系统的安全漏洞对现代社会构成了严重的威胁。现有的检测可利用软件漏洞的技术在很大程度上是非正式的。也就是说，当前的漏洞检测技术不能证明是否存在漏洞（如果存在的话）。该项目的目标是开发正式的技术和工具链，以证明一类与内存损坏相关的漏洞的存在，并针对源代码可能无法完全获得的遗留（二进制）软件系统。该项目将漏洞检测定义为可达性问题：计算可证明保证在程序的某些执行中达到可利用程序状态的初始程序状态。该项目使用程序逻辑三元组，这是Hoare逻辑三元组的一种变体，它正式定义了利用状态的可达性与允许它们发生的前提条件之间的关系。然后使用这个关系来计算先决条件的搜索空间。该项目的方法包括将二进制代码提升到一个高级模型，该模型可证明是过度近似的，因为该模型包含了程序员预期的和非预期的代码行为。然后使用描述一类与内存损坏相关的漏洞的断言对提升的模型进行检测。然后计算填充利用状态搜索空间的先决条件。该方法的步骤在定理证明器中被证明是正确的，这使得可以证明地确定漏洞的存在。该项目的工具链将作为应用案例研究应用于工业强度的生产软件系统。项目的结果将通过相关软件安全文献和开放项目工具实现的结果出版物广泛传播。此外，它们将被集成到流行的集成开发环境和反编译器中，并被集成到弗吉尼亚理工大学的研究生课程中。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

Modern society relies on computer software. Security vulnerabilities in software systems pose a serious threat as vulnerabilities are increasingly exploited to leak users' confidential data, leak computer systems' privileged information, and hijack computer systems to create malicious behaviors, among others. Current techniques for detecting exploitable software vulnerabilities lack a mathematical basis in that they cannot prove soundness of detected exploits or prove the absence of classes of exploits. The project will develop techniques that can establish the presence of a class of memory-related exploitable software vulnerabilities. Thus, if a given software has such vulnerabilities, the project's techniques are guaranteed to detect them. The project targets legacy software systems for which source codes may not be fully available, and therefore targets their binary codes. The project's methodology involves translating the binary code to a model that permits relatively easier reasoning of the code's exploitable vulnerabilities. On such a model, the methodology's algorithms compute initial program values that can result in the code's exploitable vulnerabilities to manifest, if there exist such values. Each step of the methodology is mathematically proven correct in a theorem-prover, a software tool that allows mathematically proving properties of algorithms. The project's techniques will be applied to industrial-strength production software systems to detect exploitable vulnerabilities and thereby demonstrate the techniques' effectiveness. The project's results will be broadly disseminated through publications of the results in the relevant software security literature and open sourcing the project's tool implementations. Security vulnerabilities in software systems pose a serious threat to modern society. Existing techniques for detecting exploitable software vulnerabilities are largely non-formal. That is, current exploit detection techniques do not provably establish the presence of exploits (if they exist). The project's objective is to develop formal techniques and toolchains that can prove the presence of a class of memory corruption-related exploits, and targets legacy (binary) software systems for which source codes may not be fully available. The project formulates exploit detection as a reachability problem: computing initial program states that are provably guaranteed to reach exploitable program states in some execution of the program. The project uses program logic triples, a variant of Hoare Logic triples, that formally defines the relation between the reachability of exploit states and the preconditions which allow them to occur. This relation is then used to compute the search space of preconditions. The project's methodology involves lifting the binary code to a high-level model that is provably over-approximative in that the model subsumes programmer-intended as well as unintended code behaviors. The lifted model is then instrumented with assertions that describe a class of memory corruption-related exploits. Preconditions that populate the search space of exploit states are then computed. The methodology's steps are proven correct in a theorem prover, which enables provably establishing the presence of exploits. The project's toolchain will be applied to industrial-strength production software systems as application case studies. The project's results will be broadly disseminated through publications of the results in the relevant software security literature and open sourcing the project's tool implementations. Additionally, they will be integrated into popular Integrated Development Environments and decompilers, and into a graduate course at Virginia Tech.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.