CAREER: Scalable Concolic Execution

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.