Everything is Good for Something: Counterexample-Guided Directed Fuzzing via Likely Invariant Inference

Everything is Good for Something: Counterexample-Guided Directed Fuzzing via Likely Invariant Inference

Speakers: Heqing Huang, Anshunkang Zhou, Mathias Payer, Charles Zhang

Conference: IEEE S&P

YouTube: https://www.youtube.com/watch?v=r1Te0e7oVGY

Overview

In an era where software underpins nearly every facet of modern society, the prevalence and potential impact of software bugs have escalated dramatically. From critical infrastructure to personal devices, vulnerabilities can lead to severe consequences, including financial loss and even threats to human life. The challenge of securing software is compounded by its ever-increasing scale and complexity; projects like the Linux kernel and Chrome browser boast tens of millions of lines of code, while hardware-reliant systems like Tesla vehicles exceed hundreds of millions. Detecting vulnerabilities in such vast codebases is akin to finding a needle in a haystack, a task made even more daunting by the explosive number of execution paths and intricate path conditions. This talk introduces a novel approach to directed fuzzing, named Hollow, which significantly enhances the efficiency of bug detection by addressing a fundamental limitation in existing directed fuzzing techniques: the indirect generation of inputs.

Presented by Heqing Huang and his collaborators from City University of Hong Kong, Hong Kong University of Science and Technology, and EPFL, this research tackles the problem of inefficient bug triggering in directed fuzzing. While current methods excel at guiding the fuzzer towards target code locations, they often struggle to generate the precise inputs required to trigger a bug once that location is reached. Hollow proposes a counterexample-guided directed fuzzing framework that leverages dynamic likely invariant inference to approximate the complex path conditions necessary to activate a vulnerability. By transforming the challenge of path condition solving into an iterative refinement process guided by both reachable and unreachable inputs, Hollow achieves substantial speedups and demonstrates the ability to uncover previously missed vulnerabilities, including incomplete fixes for known CVEs.

The significance of Hollow lies in its ability to bridge the gap between reaching a target and effectively triggering a bug. Existing directed fuzzers prioritize seeds based on their proximity to a target, but often rely on largely random mutations for input generation, leading to wasted computational resources. Hollow’s innovative use of invariant inference to directly guide input generation, coupled with a mechanism to learn from "unreachable" inputs as counterexamples, represents a paradigm shift. This methodology not only accelerates the discovery of bugs by orders of magnitude but also provides a more systematic approach to identifying subtle, hard-to-reach vulnerabilities that evade conventional fuzzing strategies, thereby bolstering the security posture of large and complex software systems.

Background

▶ Watch: Introduction: Software bugs in large codebases (0:00)

The pervasive nature of software in modern society means that software bugs are not just an inconvenience but a significant security and operational risk. The sheer scale of contemporary software projects, such as Linux and Chrome with over 10 million lines of code, or Tesla's codebase exceeding 100 million lines, makes comprehensive vulnerability detection incredibly challenging. As highlighted by the Heartbleed vulnerability, which involved 13,000 lines of code across seven files within a larger 1.5 million-line project, even critical bugs can be deeply embedded and difficult to isolate amidst vast codebases and complex execution paths.

Traditional fuzzing has emerged as a lightweight and effective technique for automated bug detection. It operates by generating numerous test cases through methods like random mutation, executing them against a target program, and reporting any triggered bugs. A key feedback mechanism in fuzzing involves preserving inputs that trigger new program behaviors, such as increased code coverage, as "seed templates" for future input generation. This iterative process allows fuzzers to gradually explore the program's state space.

Directed fuzzing builds upon this foundation by introducing an explicit goal: to detect specific bugs or reach particular code locations. It achieves this by incorporating additional execution feedback to prioritize seed inputs that are deemed "closer" to the defined targets. For instance, if two execution paths lead to a target, directed fuzzers will favor the path with a shorter control flow distance, increasing the likelihood of reaching the target. This makes directed fuzzing highly applicable for scenarios like patch verification, generating zero-day exploits, and identifying regressions.

Despite these advancements, the speakers identify a critical limitation: existing directed fuzzing techniques suffer from deficient bug triggering. While they may efficiently guide the fuzzer to the vicinity of a target, they often spend an inordinate amount of time attempting to generate the precise input required to activate the bug once the target is reached. Their evaluation of Magma using AFLgo, a state-of-the-art directed fuzzer, revealed that triggering a bug could take 1,000 times longer than merely reaching the target location. The root cause of this inefficiency is that the vast majority (nearly 100% in their observations) of generated inputs fail to even reach the target program points where bugs occur. Even with sophisticated filtration techniques like Beacon, which aim to prune "invisible" (unreachable) inputs, over 88% of fuzzing time was still wasted on executing these irrelevant test cases. This problem is summarized as the indirect input generation problem: current directed fuzzers primarily focus on seed prioritization based on proximity, overlooking the crucial aspect of directly generating inputs that satisfy the intricate path conditions leading to and triggering the target bug. Solving these path conditions directly through symbolic execution or SMT solvers is often impractical due to path explosion and computational expense, necessitating a more efficient and scalable approach.

Key Findings

▶ Watch: Problem: Deficient bug triggering after reaching target (4:00)

The central contribution of this research is Hollow, a novel counterexample-guided directed fuzzer designed to overcome the "indirect input generation problem" prevalent in existing directed fuzzing techniques. Hollow's primary objective is to significantly improve the efficiency of bug triggering by generating inputs that are more likely to satisfy the complex conditions required to reach and activate a target vulnerability.

The key findings and contributions of Hollow are:

1. Enhanced Reachability and Test Case Generation: Hollow demonstrates a remarkable improvement in generating test cases that successfully reach the target. In their evaluations, Hollow generated 6.2 times more test cases that reached the specified targets compared to state-of-the-art directed fuzzers. This increased density of reachable inputs is crucial for efficient bug detection.

1. Significant Speedup in Bug Detection: By focusing on generating more relevant inputs, Hollow achieves a substantial acceleration in the bug-finding process. The tool demonstrated a 15.3 times speedup in detecting the same bugs that existing directed fuzzers could find. This translates to discovering vulnerabilities much faster, reducing the time and computational resources required for security testing.

1. Discovery of Incomplete CVE Fixes: Beyond merely accelerating known bug detection, Hollow's enhanced precision and efficiency enabled the discovery of new, subtle vulnerabilities. The researchers successfully identified 10 incomplete fixes of previous CVEs or bugs. This highlights Hollow's capability to uncover lingering security flaws that were thought to be patched but remained exploitable under specific, hard-to-reach conditions. This finding underscores the importance of advanced fuzzing techniques for thorough patch verification and regression testing.

1. Leveraging Unreachable Inputs as Counterexamples: A core innovative insight of Hollow is to harness the vast majority of "unreachable" inputs—those that do not reach the target—not as wasted effort, but as valuable counterexamples. These counterexamples are used to refine and improve the precision of the approximated path conditions, guiding subsequent input generation more effectively. This adaptive learning mechanism allows Hollow to continuously improve its understanding of the target's requirements.

1. Efficient Condition Approximation via Dynamic Invariant Inference: Hollow addresses the challenge of directly solving complex path conditions by approximating them efficiently using lightweight dynamic likely invariant inference. This technique iteratively refines the understanding of the conditions based on observed inputs and their execution outcomes, providing a scalable alternative to computationally expensive symbolic execution.

In essence, Hollow redefines the approach to directed fuzzing by shifting the focus from merely prioritizing seeds to actively guiding input generation through an adaptive, learning-based mechanism. This fundamental change results in a significantly more effective and efficient bug discovery process, capable of finding elusive vulnerabilities that traditional methods often miss.

Technical Deep Dive

▶ Watch: Our solution: Hollow, counter-example guided fuzzing (6:00)

Hollow's technical core revolves around addressing the "indirect input generation problem" by directly guiding input generation towards satisfying target path conditions, rather than relying solely on seed prioritization. The proposed solution is counterexample-guided directed fuzzing, which leverages dynamic likely invariant inference to approximate these conditions efficiently.

The overarching intuition is to transform the problem of solving complex path conditions into an iterative process of approximating these conditions based on observed fuzzer inputs and outputs. This approximation then guides the generation of new inputs, increasing the probability of reaching and triggering the target. The iterative nature of fuzzing allows for the adaptive refinement of the approximated conditions.

The process begins with an initial approximation derived from a set of executed inputs. This approximation is then continuously refined using newly executed inputs. Crucially, even the "invisible" or unreachable inputs play a vital role; they serve as counterexamples that help reduce the over-approximation of the inferred invariants, making the approximation more precise. These invariants effectively define a boundary or a constrained search space for input generation. For each input byte, Hollow samples values from this refined search space, which is more likely to satisfy the necessary path conditions. For example, if the invariant inference determines that the first four bytes of an input must have fixed values for a variable X to become 10 and satisfy a condition at line three, Hollow will prioritize generating inputs that adhere to this constraint.

Two main technical challenges need to be overcome to realize this insight:

1. How to efficiently infer the condition from executed inputs.
2. How to efficiently generate inputs constrained by the inferred condition.

Both challenges are fundamentally linked to the scalability of approximating the condition, particularly concerning relevant input bytes and their values and relations.

Challenge 1: Efficiently Inferring Conditions from Executed Inputs

Invariant inference, especially for large input sizes, can be computationally intensive. To make it scalable, Hollow employs a preliminary step: identifying relevant input bytes. This is achieved by adapting a taint inference approach. A byte is deemed relevant if its value influences a variable involved in a branch condition that is reachable to the target. For example, by sequentially mutating each byte in an input, the system observes if a change in byte 1 influences the value of variable X at line 3, which is on a path to the target at line 6. If such an influence is detected, byte 1 is marked as relevant, and invariant inference is then focused only on these relevant bytes. This significantly reduces the search space for inference.

Once relevant bytes are identified, the next step is to obtain the related values of the target condition. Not all inputs contribute equally to approximating a condition. The intuition is that only inputs near the boundaries of the condition are most helpful. To illustrate, for a condition like X > 10, inputs like 11, 12, 9, or 8 are more informative for precisely approximating the boundary 10 than inputs like 100 or -50, which are far from it.

To precisely select these useful inputs, Hollow measures the distance of each input towards the boundary. A condition is conceptualized as a function whose inputs are the related variables. The set of inputs that make the output of this function zero constitutes the boundary. The distance is then measured as the absolute value of this function collected during execution. For instance, inputs that yield a smaller absolute value for the function are considered closer to the boundary and thus more valuable for approximation. Based on statistical principles, the sample size of these useful inputs is calculated to satisfy a confident interval (e.g., alpha > 0.95), ensuring that the approximated condition is sufficiently precise.

Challenge 2: Efficiently Generating Inputs Constrained by the Condition

Once invariants are inferred, the next hurdle is to effectively generate new inputs based on these constraints, which requires tackling the precision of the relations. Conventional invariant inference can provide diverse forms of invariants (e.g., interval invariants like X in [5, 10] or more precise polyhedral invariants like X + Y < 20). While more precise invariants are desirable, generating inputs from them can be significantly more expensive (e.g., polyhedral invariants require complex constraint solving, whereas interval invariants might only need random sampling within a range). Moreover, the input generation speed based on sampling relations is linearly complex based on the number of provided invariants.

Hollow addresses this challenge using importance sampling. Each inferred invariant is assigned an initial "importance" score. This importance score is adaptively adjusted throughout the fuzzing process based on the success rate of generating reachable inputs using that specific invariant. For example, if an invariant like X > 5 is used to guide input generation, its importance is decreased whenever a generated input, guided by this invariant, fails to reach the target (i.e., acts as a counterexample). Conversely, if it successfully leads to a reachable input, its importance is increased. This dynamic adjustment mechanism ensures that the fuzzer prioritizes and preserves the most precise and effective invariants for guiding input generation. If no existing invariant achieves sufficient precision, the invariant inference engine is re-invoked to refine the invariants further.

In summary, Hollow leverages both reachable and unreachable inputs towards the targets to gradually approximate the complex path conditions required to reach a target. This is achieved through a scalable, dynamic invariant inference technique that focuses on relevant input bytes and prioritizes precise invariants via importance sampling. This comprehensive approach significantly increases the proportion of reachable inputs generated and, consequently, the probability of triggering the targeted bugs.

Demo / Proof of Concept

▶ Watch: Technical approach: Dynamic likely invariant inference (8:00)

While the talk does not describe a live demonstration of the Hollow tool in action, the researchers clearly articulate its practical application and effectiveness through their evaluation results. They mention "our evaluation of Magma using AFLgo," indicating that Hollow was implemented and tested against existing state-of-the-art directed fuzzers. The core proof of concept lies in the quantitative improvements achieved: generating 6.2 times more test cases that reach targets and a 15.3 times speedup in detecting bugs. The most compelling evidence of its capability is the discovery of 10 incomplete fixes of previous CVEs or bugs, which serves as a powerful testament to Hollow's ability to uncover subtle, real-world vulnerabilities that had previously been missed or inadequately addressed. This demonstrates that Hollow is not merely a theoretical concept but a functional and impactful security testing tool.

Defensive Implications

▶ Watch: Addressing scalability: Identifying relevant input bytes (9:40)

The insights and capabilities presented by Hollow have profound implications for software defenders, developers, and security teams seeking to enhance the robustness and security of their systems.

1. Re-evaluate Existing Fuzzing Strategies: Defenders should recognize the limitations of current directed fuzzing techniques, particularly their inefficiency in triggering bugs even after reaching target code. Relying solely on distance-based prioritization might lead to a false sense of security if the precise conditions for exploitability remain unmet. Security teams should explore integrating advanced fuzzing methodologies that focus on direct input generation.

1. Adopt Advanced Directed Fuzzers for Critical Tasks: For high-stakes activities like patch verification, regression testing, and identifying zero-day vulnerabilities, adopting tools like Hollow (or similar counterexample-guided, invariant-inference-based fuzzers) becomes crucial. The ability to find incomplete fixes of previous CVEs highlights that even "patched" vulnerabilities might still be exploitable under specific, hard-to-reach conditions. Thorough re-testing with more sophisticated fuzzers is essential to ensure true remediation.

1. Prioritize Hard-to-Trigger Bugs: The research underscores that some vulnerabilities require extremely specific input patterns to manifest. These "hard-to-trigger" bugs, while difficult to find, are often critical and can be exploited by determined attackers. Development teams should pay particular attention to addressing vulnerabilities that involve complex path conditions, as these are precisely the types of issues Hollow is designed to uncover.

1. Integrate Invariant Inference into Development Pipelines: Understanding program behavior at a deeper level, particularly the invariants and conditions governing critical code paths, can significantly aid in both development and security. While Hollow uses invariant inference for fuzzing, the technique itself could inform developers about implicit assumptions and constraints in their code, potentially leading to more robust designs and fewer bugs from the outset.

1. Focus on Input Validation and Sanitization: The emphasis on precise input generation for bug triggering reinforces the paramount importance of strict input validation and sanitization at all program boundaries. If a fuzzer needs to precisely craft specific byte sequences to trigger a bug, robust input handling can act as a primary defense by preventing such malformed inputs from reaching sensitive code paths.

In essence, Hollow provides a powerful reminder that merely reaching a vulnerable code location is not enough; the ability to precisely craft the input to trigger the vulnerability is equally critical. Defenders must adapt their strategies to leverage these advanced techniques to identify and mitigate the most elusive and dangerous software flaws.

Key Takeaways

• Traditional directed fuzzing often struggles with deficient bug triggering, spending vast amounts of time failing to generate the precise inputs needed to activate a bug, even after reaching the target code location.
• Hollow, a novel counterexample-guided directed fuzzer, addresses this by employing dynamic likely invariant inference to approximate complex path conditions required for bug activation.
• Hollow leverages both reachable and unreachable inputs; unreachable inputs serve as crucial counterexamples to refine and increase the precision of the inferred invariants.
• The system achieves significant performance improvements, including 6.2 times more reachable test cases and a 15.3 times speedup in detecting bugs, by guiding input generation directly towards satisfying path conditions.
• A key practical outcome is Hollow's ability to discover 10 incomplete fixes of previous CVEs or bugs, highlighting its effectiveness in uncovering subtle, previously missed vulnerabilities.
• Technical innovations like identifying relevant input bytes, measuring distance to boundaries for useful input selection, and using importance sampling for invariant selection contribute to Hollow's efficiency and precision.

About the Speaker(s)

The talk "Everything is Good for Something: Counterexample-Guided Directed Fuzzing via Likely Invariant Inference" was presented by Heqing Huang, who is credited as the primary presenter. The research is a collaborative effort involving Heqing Huang, Anshunkang Zhou, Mathias Payer, and Charles Zhang. The team represents institutions including City University of Hong Kong, Hong Kong University of Science and Technology, and EPFL. The transcript does not provide further biographical details about the individual speakers beyond their names and affiliations.