CAREER: Scalable Concolic Execution

随着我们的日常生活越来越依赖网络系统，查找和纠正编程错误从未像现在这样重要。这类编程错误也称为“错误”，攻击者可以利用这些错误来危害关键系统。然而，发现关键的软件错误/漏洞就像大海捞针：人类编写的测试用例不能触发角落用例引起的错误，随机生成的测试用例无法达到计算机程序的深度执行状态。该项目将通过提出动态符号执行(也称为并发执行)来解决这些限制，该测试用例生成技术可以系统地探索所有可能的执行状态。该项目旨在通过缩小搜索空间和提高搜索速度来提高并发执行的可扩展性。较小的搜索空间将导致更好的代码覆盖率或更快地实现相同的覆盖率。通过使用强化学习技术自动推断和修剪不会导致新的程序状态的执行路径，例如错误路径，将实现缩小搜索空间的目标。通过更高效的符号约束收集和约束求解，达到提高搜索速度的目的。通过用高度优化的动态数据流分析取代传统的符号解释，将完成更高效的约束收集。通过用高吞吐量的局部随机搜索代替传统的定理证明器，可以实现更高效的约束求解。这些技术旨在使关键应用程序(如操作系统内核、物联网固件，甚至硬件设计)更加安全。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

As our daily life depends more and more on cyber systems, finding and correcting programming errors are never more important. Such programming errors, also known as "bugs," can be exploited by adversaries to compromise critical systems. However, finding critical software bugs/vulnerabilities are like finding a needle in a haystack: test cases written by humans cannot trigger bugs caused by corner cases, and randomly generated test cases cannot reach deep execution states of a computer program. This project will address these limitations by advancing dynamic symbolic execution (a.k.a., concolic execution), a test case generation technology that can systematically explore all possible execution states.This project aims to advance the scalability of concolic execution by narrowing the search space and improving the search speed. A smaller search space will lead to better code coverage or achieve the same coverage faster. The goal of narrowing the search space will be achieved by using reinforcement learning techniques to automatically infer and prune execution paths that will not lead to new program states, such as error paths. The goal of improving search speed will be achieved with more efficient symbolic constraint collection and constraint solving. More efficient constraint collection will be done by replacing traditional symbolic interpretation with highly optimized dynamic data-flow analysis. More efficient constraint solving will be done by replacing traditional theorem provers with high throughput local stochastic search. The techniques aim to make critical applications, such as OS kernels, IoT firmware, and even hardware designs more secure.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.