High-fidelity Symbolic Execution for Vulnerability Hunting

当采用符号执行进行漏洞搜索时，安全研究人员经常面临完整理论和实用工具之间的权衡。虽然尽一切努力忠实地翻译程序语义，但妥协，如有界循环展开，通常是在假设不这样做会使后端求解器过载的情况下引入的。这些妥协使得程序语义的保真度很低，这会导致错误警报和遗漏错误。然而，多年来，实用性一直是权衡中获胜的一方。低保真度的符号化实践通过几代符号执行者的积累，即使限制不再存在。由于这种惯性，最先进的工具很难声称战胜任何漏洞类型，因为有无数种方式触发假警报和/或遗漏错误。理论和实践之间日益扩大的差距不利于软件安全研究。我研究的长期目标是通过正式化实际漏洞狩猎的艺术并建立一个理论框架来解释安全工具的新奇，可组合性和权衡来缩小这一差距。作为基础性步骤，短期目标侧重于通过研究HISE（高保真符号执行的缩写）作为下一代符号执行程序，“理论化”一种特定的错误搜索技术-符号执行。在HISE中，可靠性和完整性是一等公民，这是由无损符号化过程保证的，该过程将程序转换为SMT公式，同时保留代码中的所有信息。这意味着所有的实用性解决方案，即使是那些被认为对现代符号执行器至关重要的解决方案，都将被重新审视，并使用新技术进行改进。无损符号化开启了一个有趣的机会：为漏洞搜索管道中的所有构建块提供一种通用且明确的语言。示例构建块包括程序语义的近似、可解性优化、领域知识和漏洞建模。每个构建块都可以独立开发，而不会失去与其他构建块组合的机会。通过这种方式，可以对实用性妥协进行改造，但只能以可量化的方式进行。HISE通过为可量化的实用性提供一个公共场所来推进软件安全研究。这使得问题本地化，解决方案组合，并最终以整体的方式发展整个领域。HISE还将通过发现传统软件中的错误（例如，Linux内核）和新的编程范例（例如，智能合约）。该研究项目将培养一批高技能的安全从业人员，具有丰富的查杀漏洞和构建安全软件的经验。随着网络安全在各行各业的发展势头，这些候选人将在就业市场上受到高度要求。

When adopting symbolic execution for vulnerability hunting, security researchers often face a trade-off between a complete theory and a practical tool. While every effort is made to translate program semantics faithfully, compromises, such as bounded loop unrolling, are often introduced with a presumption that not doing so will overload the backend solver. These compromises make a low-fidelity representation of program semantics, which causes both false alarms and missing bugs. However, throughout the years, practicality has always been on the winning side in the trade-off. Low-fidelity symbolization practices accumulate through generations of symbolic executors even when the limitations no longer exist. Because of this inertia, state-of-the-art tools can hardly claim triumph over any vulnerability type given innumerable ways to trigger false alarms and/or missing bugs. A growing gap between theory and practice is detrimental to the software security line of research. The long-term goal of my research is to close this gap by formalizing the arts of practical vulnerability hunting and building a theoretical framework to explain novelty, composability, and trade-offs of security tools. As a foundational step, the short-term objective focuses on 'theorizing' a specific bug hunting technique--symbolic execution--through the research on HISE, short for High-fidelity Symbolic Execution, as the next generation symbolic executor. Soundness and completeness are first-class citizens in HISE, which is guaranteed by a lossless symbolization procedure that transpiles a program into SMT formulae while preserving all information in the code. This means all practicality workarounds, even those that have been deemed crucial to modern symbolic executors, will be re-examined and revamped with novel techniques. Lossless symbolization unlocks an intriguing opportunity: a common and unambiguous language for all building blocks in the vulnerability hunting pipeline. Example building blocks include approximations of program semantics, solvability optimizations, domain knowledge, and vulnerability modeling. Each building block can be independently developed without losing the chance compose with other building blocks. In this way, practicality compromises can be retrofitted but only in a quantifiable manner. HISE advances software security research by providing a common playground for quantifiable practicality. This enables problem localization, solution composition, and ultimately, evolving the whole field in a holistic way. HISE will also make real-world impacts by finding errors in both traditional software (e.g., the Linux kernel) and new programming paradigms (e.g., smart contracts). This research program will train a batch of highly-skilled security practitioners with rich experience on hunting bugs and building secure software. These candidates will be highly demanded in the job market as cybersecurity gain momentum across industries.