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

随着社会对软件程序的依赖程度越来越高，软件漏洞已成为网络安全中最关键的问题之一。研究人员一直在开发技术来解决软件安全问题，保护程序免受攻击。在这些技术中，符号执行是一种高效的软件安全技术。尽管符号执行很有希望，但由于应用于现实世界软件安全任务时的基本可用性和可伸缩性限制，它很难产生现实世界的影响。本项目旨在了解没有采用符号执行的原因，并利用这种理解为现实世界的场景实现可行的符号执行，以帮助网络安全分析人员或软件开发人员成功地找到漏洞。该项目将创建特定于场景的符号执行(S3E)，这是一个可定制的符号执行框架，将使不同的用户能够针对各种真实世界的场景利用符号执行。利用任务分析和人类对符号执行的研究，该项目将创建有效的人机界面，并开发一个可用的框架，以提高符号执行在现实世界网络安全任务中的生存能力。该项目将系统地确定符号执行在现实世界场景中的工作情况，以及失败的原因，以发展特定场景的符号执行概念。该项目将开发人机交互模型和符号执行框架，作为特定场景符号执行工具的基础。其结果将是一种新型的符号执行技术--人类推动的符号执行--它将使人类能够增强符号执行的可扩展性，并使该技术适用于更多真实世界的场景。开源工具将向公众发布。将进行一项针对象征性执行而量身定做的错误赏金计划。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.