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

随着社会越来越依赖软件程序，软件漏洞已成为网络安全中最关键的问题之一。研究人员一直在开发解决软件安全问题和保护程序免受攻击的技术。在这些技术中，符号执行是一种非常有效的软件安全技术。尽管有了它的承诺，但由于应用于现实世界的软件安全任务时的基本可用性和可伸缩性限制，符号执行一直在努力产生现实世界的影响。该项目旨在了解缺乏符号执行背后的原因，并利用这种理解来实现现实世界场景中可行的符号执行，以帮助网络安全分析师或软件开发人员成功发现漏洞。该项目将创建特定于场景的符号执行（S3E），这是一种可定制的符号执行框架，将使不同的用户能够在各种实际场景中利用符号执行。通过对符号执行的任务分析和人类主题研究，该项目将创建有效的人机界面，并开发一个可用的框架，以提高符号执行在现实世界网络安全任务中的可行性。该项目将系统地确定符号执行在现实场景中的工作效果，或者为什么它会失败，以便开发特定于场景的符号执行的概念。该项目将开发一个人机交互模型和一个符号执行框架，作为特定场景符号执行工具的基础。结果将是一种新型的符号执行技术——人类增强的符号执行——这将使人类能够增强符号执行的可扩展性，并使该技术在更多的现实场景中可行。开源工具将向公众发布。将实施针对符号执行的漏洞赏金计划。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.