权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

SaTC: CORE: Small: Sound Automatic Exploit Generation

SaTC：核心：小：声音自动漏洞利用生成

基本信息

批准号：
2234257
负责人：
Binoy Ravindran
金额：
$ 60万
依托单位：
Virginia Polytechnic Institute and State University
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2023
资助国家：
美国
起止时间：
2023-06-15 至 2026-05-31
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2234257&HistoricalAwards=false
关键词：
SaTC CORE Small Sound Automatic

项目摘要

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.

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