SHF: Small: Symbolic Execution for Low-Latency Applications

When executing a program, a computer maintains a value for each variable in the program. This project instead considers a type of execution called "symbolic execution", wherein the computer maintains a description of the value of each variable; this description might be its actual value, but it might instead be characteristics of its value. For example, at a certain point in the program's execution, the computer might know only that the variable contains a value larger than five. Symbolic execution has found myriad applications for security analysis and defense, software testing, and debugging. However, it is also much slower than regular execution, which precludes its use for several important purposes. This project’s novelties are in a variety of innovations to make symbolic execution faster. This project's impacts are to enable new applications for symbolic execution in the areas of computer security, debugging, and diagnostics. The investigator seeks to involve students from underrepresented groups in the research and to release software embodying these improvements. The innovations explored in this project to accelerate symbolic execution of a program include methods to reduce instrumentation of the program needed to execute it symbolically; to more quickly find a control-flow path to reach a desired point in the program; to limit the paths explored to a subset allowed by policies on (otherwise unknown) inputs; and to otherwise limit symbolic execution costs. One application that serves as a proving ground for progress in the project is a method by which a verifier determines (using symbolic execution) that the messages received from a remote component are consistent with the claimed or sanctioned component software, e.g., as a means of defending the receiver from malicious inputs. 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.