SaTC: CORE: Medium: Symbolizing Viability: Paving the Road to Practical Symbolic Execution

As society increasingly depends on software programs, software vulnerabilities have become one of the most critical issues in cybersecurity. Researchers have been developing techniques to address software security issues and protect programs from attacks. Among these techniques, symbolic execution is a highly effective technique for software security. Despite its promise, symbolic execution has struggled to make a real-world impact, due to fundamental usability and scalability limits when applied to real-world software security tasks. This project aims to understand the reasons behind the lack of adoption of symbolic execution and leverage this understanding to achieve viable symbolic execution for real-world scenarios, to help cybersecurity analysts or software developers succeed at finding vulnerabilities. The project will create scenario-specific symbolic execution (S3E), a customizable symbolic execution framework that will enable diverse users to leverage symbolic execution for various real-world scenarios. Using task analysis and human subject studies on symbolic execution, This project will create effective human-machine interfaces and develop a usable framework that improves symbolic execution's viability for real-world cybersecurity missions. The project will systematically identify how well symbolic execution works, or why it fails, in real-world scenarios, in order to develop the notion of scenario-specific symbolic execution. The project will develop a human-machine interaction models and a symbolic execution framework as the basis of scenario-specific symbolic execution tools. The result will be a new type of symbolic execution technology – human-boosted symbolic execution – which will enable humans to enhance symbolic execution’s scalability and make the technology viable for more real-world scenarios. Open source tools will be released to the public. A bug bounty program tailored to symbolic execution will be conducted. 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.