SaTC: CORE: Small: Sound Automatic Exploit Generation

点击翻译按钮获取中文摘要

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.