High-fidelity Symbolic Execution for Vulnerability Hunting

点击翻译按钮获取中文摘要

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.