High-fidelity Symbolic Execution for Vulnerability Hunting

当采用符号执行进行漏洞搜索时，安全研究人员经常面临完整理论和实用工具之间的权衡。在尽一切努力忠实地翻译程序语义的同时，引入妥协（例如有界循环展开）时，通常假定不这样做将使后端求解器过载。这些妥协使得程序语义的表示保真度较低，从而导致假警报和遗漏bug。然而，多年来，实用性一直是权衡中的赢家。低保真的符号化实践通过一代又一代的符号化执行者积累，即使限制不再存在。由于这种惯性，最先进的工具很难战胜任何漏洞类型，因为有无数种方法可以触发假警报和/或遗漏bug。理论与实践之间越来越大的差距不利于软件安全的研究。我的研究的长期目标是通过形式化实际漏洞搜索的艺术和构建一个理论框架来解释安全性工具的新颖性、可组合性和权衡，从而缩小这一差距。作为基础步骤，短期目标侧重于通过对HISE （High-fidelity symbolic execution的缩写）作为下一代符号执行器的研究，“理论化”一种特定的bug查找技术——符号执行。在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.