VeriBin: Adaptive Verification of Patches at the Binary Level

VeriBin: Adaptive Verification of Patches at the Binary Level

Speakers: Hongwei Wu, PhD Candidate, Purdue University & Simon Fraser University

Conference: NDSS Symposium

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

Overview

In the critical realm of software security, maintaining vulnerabilities without introducing new issues is a perpetual challenge. The adage "if it ain't broke, don't fix it" often dictates vendor behavior, particularly in high-reliability domains such as automotive or medical devices, where even minor regressions can have catastrophic consequences. The fear of inadvertently breaking existing functionality or injecting unintended changes frequently leads vendors to hesitate in applying crucial security patches. While advanced tools like Sim, Spider, and ARD have made significant strides in semantic equivalence and patch verification, their reliance on readily available source code or a complete build chain presents a substantial limitation. In many real-world scenarios, especially when dealing with third-party components or legacy systems, this crucial information is simply inaccessible.

This talk introduces VeriBin, a groundbreaking system designed to address this critical gap by enabling adaptive verification of patches directly at the binary level. VeriBin allows an analyst to formally verify that a patched binary, received from a third-party vendor, neither breaks existing functionality nor introduces unwanted modifications, all without needing access to the original source code. The system's innovative approach focuses on formally modeling patch effects and ensuring the preservation of original functionality. Furthermore, VeriBin is "adaptive," meaning it can integrate domain-specific insights from human analysts to refine its verification process and filter out semantically equivalent changes that might otherwise be flagged as violations.

The core challenge VeriBin tackles is the difficulty of performing precise semantic comparisons on compiled binaries, which are often obfuscated by compiler optimizations and lack high-level symbolic information. By overcoming these hurdles, VeriBin provides a vital capability for ensuring the integrity and safety of software in environments where source-code-level verification is impractical or impossible. Its ability to accurately identify both benign, functionality-preserving patches and malicious, functionality-altering changes—demonstrated through real-world case studies—positions it as an indispensable tool for enhancing software supply chain security and reliability.

Background

▶ Watch: Introduction and problem: Verifying binary patches without source (0:00)

The landscape of vulnerability maintenance is fraught with complexity. Traditionally, when source code is available, static analysis tools and formal verification methods can be employed to analyze the impact of patches. Tools like Sim, Spider, and ARD leverage source-level information to determine semantic equivalence between original and patched code. However, the assumption of source code availability is often unrealistic. Many organizations rely on third-party binaries for critical components, or they manage legacy systems where the original source code and build environments have been lost or are poorly documented. In such cases, verifying patches becomes a daunting task.

Without source code, analysts typically resort to laborious and error-prone manual methods. These include comparing byte patterns, performing structural comparisons using binary diffing tools, or painstakingly comparing decompiled code. While these techniques can highlight potential changes, they demand extensive human effort, are highly susceptible to human error, and struggle to formally verify the semantic intent of a patch. A byte-level or structural difference might merely be a compiler optimization, not a functional change, yet manual inspection would struggle to differentiate. Conversely, a subtle, malicious change could easily be overlooked.

The problem is exacerbated in domains where reliability and security are paramount, such as embedded systems in automotive, avionics, or medical devices. In these environments, even a seemingly minor patch must be rigorously validated to ensure it doesn't introduce regressions, security vulnerabilities, or compliance issues. The lack of robust, automated, and formal verification tools for binary-level patches has long been a significant barrier, pushing vendors to either accept the risk of unverified patches or to defer patching altogether, leaving systems vulnerable. VeriBin emerges as a direct response to this critical need, offering a formal, automated, and adaptive solution to verify binary patches, thereby enhancing trust and security in the software supply chain. The project builds upon the foundational work of previous research, such as Spider, which defined "safe to apply" properties relevant to security patches, but extends this capability to the challenging binary domain.

Key Findings

▶ Watch: VeriBin system design overview and phases (2:30)

VeriBin represents a significant leap forward in binary-level patch verification, offering several key findings and contributions:

1. First Adaptive Binary-Level Verification System: VeriBin is presented as the first system capable of describing and verifying patch behaviors at the binary level for "functionality preserving properties." This addresses a long-standing gap in security tools, particularly for scenarios where source code is unavailable. Its adaptive nature, allowing for analyst input, is a novel feature.
2. Accuracy and Reliability: The system demonstrates high accuracy, achieving "no false positives" in its evaluation. This means that unsafe patches are never incorrectly categorized as safe, which is paramount for security-critical applications. This reliability ensures that any patch deemed "safe" by VeriBin truly maintains the original functionality without introducing regressions or new vulnerabilities.
3. Efficiency: VeriBin was evaluated on 86 pairs of original and patched binaries, covering both unstripped and stripped versions. The average runtime for its analysis was approximately 1300 seconds, demonstrating practical applicability for real-world scenarios. This efficiency makes it feasible for integration into patch validation workflows.
4. Novel Solutions for Binary-Level Challenges:

• Compiler-Introduced Offset Change Detection: VeriBin effectively tackles the pervasive issue of compiler-introduced offset changes, which often hinder direct binary comparison. By employing three heuristic-based techniques, it can accurately identify and ignore these benign memory address variations that do not reflect actual functional modifications.
• Simplified Symbolic Comparison via Matching Path Pairs: To overcome the complexity of symbolic expressions generated during binary analysis, VeriBin introduces the concept of matching path pairs. This optimization significantly simplifies the comparison process by allowing direct comparison of symbolic values between corresponding execution paths, rather than merging and comparing highly complex expressions across all paths.

1. Practical Case Study Success: VeriBin's efficacy was demonstrated through two compelling case studies:

• It correctly identified a functionality-preserving security patch in the tidy project as "safe to apply."
• Crucially, it successfully detected a malicious backdoor in the exitus project, which involved an obfuscated change at the assembly level (replacing CPUID with get_CPU_ID). This highlights VeriBin's ability to uncover sophisticated, low-level attacks that might bypass source-code-centric reviews.

1. Open-Sourced for Research: The VeriBin tool has been open-sourced, encouraging further research and development in the critical area of binary-level patch verification. This commitment to transparency and community contribution is vital for advancing the state of the art.

Technical Deep Dive

▶ Watch: Challenge: Handling compiler-introduced offset changes (3:30)

VeriBin's architecture is meticulously designed to navigate the complexities of binary-level analysis, comprising two primary phases: Patch-Aware Symbolic Execution and Adaptive Verification. These phases work in tandem to formally model patch effects and validate functionality-preserving properties.

The process begins with a pre-processor step that extracts static information from both the original and patched binaries. This includes identifying matching functions, matching basic blocks, and inferring function signatures. This initial static analysis provides a foundational map for the subsequent dynamic analysis.

Phase 1: Patch-Aware Symbolic Execution

This phase is dedicated to extracting symbolic expressions that capture the behavior of the patch. The speaker highlights two major challenges inherent in using SMT (Satisfiability Modulo Theories) solvers for comparing functions at the binary level: compiler-introduced offset changes and the generation of overly complicated symbolic expressions due to information loss. VeriBin proposes specific solutions for each:

Challenge 1: Compiler-Introduced Offset Changes

Compiler-introduced offset changes refer to variations in memory addresses between the original and patched binaries, even when the underlying memory content or logical variable remains identical. These are frequently a byproduct of compiler optimizations (e.g., changes in stack frame layout, relocation of global variables) and do not signify functional modifications. Directly comparing binaries without accounting for these shifts would lead to a deluge of false positives, rendering verification impractical.

VeriBin employs three heuristic-based techniques to detect and ignore these benign changes:

1. Comparing Contents at Fixed Addresses for Global Read-Only Variables: For global variables that are constant and read-only, VeriBin directly compares the content at their respective memory addresses in both binaries. If the content is identical (e.g., a string "ABC" at address 0x1000 in the original and 0x2000 in the patched), the address shift is recognized as a compiler-introduced offset and ignored. This method is effective for data segments that are not expected to change functionally.
2. Constant Offset for Local Variables: VeriBin checks if all local variables (including function arguments and stack variables) within a function are consistently shifted by the same constant offset. For instance, if RBP-1 in the original binary corresponds to RBP-5 in the patched binary, and all other stack-relative accesses show a consistent shift of hex 20 (as in the example where all function arguments are shifted by hex 20), this uniform shift is identified and accounted for. This heuristic is particularly useful for handling changes in stack frame alignment or variable packing.
3. Matching Expressions in Similar Abstract Syntax Tree (AST) Positions: This technique involves comparing symbolic expressions that occupy similar positions within the reconstructed Abstract Syntax Tree (AST) of the original and patched code. If these expressions differ only by a constant memory offset, they are deemed semantically equivalent. This allows VeriBin to recognize that (RBP-1) and (RBP-5), when representing the same logical variable A, are equivalent despite their different memory addresses, as long as the offset is the only difference in their AST representation. This requires a robust IR (Intermediate Representation) that can capture the structural semantics of the assembly code. The speaker clarifies that VeriBin performs symbolic execution on assembly code, which is first converted to a high-level IR like VEX IR, and these IRs may still not retain all original symbol information, necessitating these offset handling mechanisms.

Challenge 2: Complicated Symbolic Expressions

When comparing functions, especially those with multiple execution paths, SMT solvers can generate extremely complex symbolic expressions if they attempt to merge all possible path constraints. This complexity can lead to performance bottlenecks and make verification intractable.

VeriBin addresses this with Matching Path Pairs. A matching path pair is defined as a pair of valid exit paths, O from the original function and P from the patched function, where any input I that executes path P in the patched function also executes path O in the original function. Crucially, this means the path constraint of P implies the path constraint of O.

By identifying such matching path pairs, VeriBin can directly compare the symbolic values (e.g., return values, modified global variables) between these specific, corresponding paths. This is significantly simpler than attempting to compare merged symbolic expressions across all possible paths. For security patches, which are typically small in scope and often involve adding checks or minor logic changes, the existence of such matching path pairs is common, making this optimization highly effective. An example given is a switch case where a global variable's content is determined by the case. If a patch modifies only one case, comparing values within the matching path pair for that case is straightforward, involving simple integer comparisons, rather than a complex SMT query over a merged expression representing all switch branches.

Phase 2: Adaptive Verification

After extracting symbolic expressions representing patch behaviors, VeriBin moves to the adaptive verification phase. This phase verifies "safe to apply" properties and involves human analysts when violations are detected.

Key Terminologies:

• Valid Exit Path: A complete execution path through a function that takes valid inputs.
• Error Handling Exit Path: A complete execution path through a function that takes invalid inputs.

VeriBin's verification focuses exclusively on valid exit paths to ensure the patch does not break original functionality under legitimate usage.

VeriBin checks four specific "safe to apply" properties, derived from previous research (like the Spider project), which are highly relevant to security patches. These properties assess the patch from two perspectives:

1. Not Increasing Input Space: This ensures the patch doesn't broaden the range of acceptable inputs, which could inadvertently expose new attack surfaces. Security patches typically restrict input space by adding checks.
2. Output Equivalence: This verifies that for any given valid input, the patched function produces the same output as the original function, ensuring functional preservation.

The verification process is automated. If all four properties evaluate to true, the patch is deemed "safe to apply." However, if any property fails, VeriBin enters its adaptive mode. It identifies the root cause of the failure and prompts the analyst for validation. The analyst's feedback is then used to refine the analysis.

An illustrative example involves a patch replacing an insecure encryption function, 3DES, with a more secure version, AES. By strict definition, this patch is not "safe to apply" because the output (encrypted data) is fundamentally different. VeriBin would detect this violation. At this point, it would engage the analyst, asking: "Can we consider these two functions (3DES and AES) semantically equivalent in the context of this patch?" If the analyst, possessing domain-specific knowledge, confirms their equivalence (e.g., both are encryption functions serving the same logical purpose, despite different algorithms), VeriBin integrates this information. This refinement allows the system to re-evaluate and potentially determine the patch as "safe to apply," demonstrating its flexibility and ability to incorporate human intelligence to resolve ambiguities that purely automated systems cannot.

Demo / Proof of Concept

▶ Watch: Adaptive verification phase: properties and analyst feedback (6:30)

The talk showcased VeriBin's capabilities through two distinct case studies, demonstrating its precision in identifying both benign and malicious binary-level changes.

Case Study 1: Safe-to-Apply Patch in tidy

The first case study involved a minimal security patch applied to the tidy project. This patch's primary function was to add an input validation check, which, if triggered, would terminate the execution. By its nature, such a patch restricts the input space without altering any existing, valid functionality.

VeriBin was applied to this original and patched tidy binary pair. The system successfully verified all four "safe to apply" properties. Since the patch only introduced a stricter input constraint and did not modify the outputs for previously valid inputs, it was correctly determined that "no functionality-breaking modifications were introduced." Consequently, VeriBin concluded that this patch was safe to apply. This demonstration highlights VeriBin's ability to accurately validate security patches that correctly enhance robustness without introducing regressions.

Case Study 2: Detecting the exitus Backdoor

The second, more critical case study involved the recently discovered exitus backdoor. This backdoor was maliciously introduced into the exitus project not via direct source code modification, but through an obfuscated build script during compilation. This subtle manipulation resulted in a binary where a legitimate assembly instruction, CPUID, was replaced by a function call to get_CPU_ID. Such a change, particularly when introduced through an obfuscated build process, is incredibly difficult to detect through traditional source code review or even simple binary diffing tools, as the source code might appear clean.

VeriBin's binary-level analysis proved highly effective in this scenario. It easily detected the replacement of the CPUID instruction with the get_CPU_ID function call. Because this modification fundamentally altered the program's execution flow and potentially its behavior (depending on what get_CPU_ID actually did), VeriBin correctly determined that this patch was not safe to apply.

This case study is particularly significant as it underscores a crucial point: the need for robust binary-level verification, even when the source code is ostensibly available. Malicious actors can bypass source code scrutiny by injecting backdoors at the compilation or linking stage, making tools like VeriBin indispensable for ensuring the integrity of the final deployed binary. It serves as a powerful proof of concept for VeriBin's ability to uncover sophisticated, low-level threats that exploit weaknesses in the software supply chain.

Defensive Implications

▶ Watch: Evaluation results and case studies (9:00)

VeriBin offers significant defensive implications for various stakeholders involved in software development, deployment, and security:

• Enhanced Software Supply Chain Security: Organizations can integrate VeriBin into their software supply chain pipelines to formally verify binaries received from third-party vendors. This is particularly crucial for closed-source components, legacy systems, or when there's a lack of trust in the build process. By verifying that patches don't introduce regressions or malicious changes, VeriBin helps to mitigate risks from compromised suppliers or obfuscated build environments.
• Improved Patch Validation for Critical Infrastructure: In highly regulated and safety-critical domains like automotive, aerospace, and medical devices, where reliability is paramount, VeriBin provides a formal method to ensure that security patches preserve original functionality. This reduces the risk of deploying patches that inadvertently break essential systems or introduce new vulnerabilities.
• Detection of Sophisticated Binary-Level Attacks: As demonstrated by the exitus backdoor case study, VeriBin is capable of detecting subtle, malicious modifications injected at the assembly or compilation level that might bypass source code review. Defenders can use VeriBin to scrutinize critical binaries for such stealthy alterations, even when the source code appears clean.
• Reduced Manual Effort and Error: By automating the verification of functionality-preserving properties, VeriBin significantly reduces the extensive human effort and propensity for error associated with manual binary diffing or decompiled code comparison. This frees up security analysts to focus on more complex, high-level threat analysis.
• Informed Decision-Making for Patch Deployment: VeriBin provides clear, actionable insights into whether a patch is "safe to apply." This allows security teams and product managers to make informed decisions about patch deployment, balancing security improvements with the risk of introducing regressions. The adaptive nature of VeriBin further allows human experts to inject their domain knowledge, avoiding false positives that might arise from purely automated, rigid comparisons.
• Proactive Vulnerability Management: By establishing a robust binary-level verification process, organizations can become more proactive in their vulnerability management strategies. They can confidently apply patches faster, knowing that the integrity and functionality of their systems will be preserved, thereby reducing the window of exposure to known vulnerabilities.

Key Takeaways

• Binary-Level Verification is Essential: Traditional source-code-dependent patch verification tools are insufficient for scenarios lacking source code or facing untrusted build chains. VeriBin fills this critical gap by enabling formal verification directly on binaries.
• Addresses Core Binary Analysis Challenges: VeriBin effectively tackles complexities like compiler-introduced offset changes using heuristic-based detection and simplifies symbolic comparisons with matching path pairs, making binary-level analysis practical and accurate.
• Adaptive and Accurate: The system incorporates human analyst feedback to refine its verification process, allowing it to handle semantic equivalences (e.g., swapping encryption algorithms) and achieve high accuracy with "no false positives" in identifying unsafe patches.
• Proven Efficacy in Real-World Scenarios: Case studies, including the correct validation of a tidy security patch and the detection of the exitus backdoor, demonstrate VeriBin's ability to identify both benign and malicious changes at the binary level.
• Significant Defensive Implications: VeriBin enhances software supply chain security, aids in validating patches for critical infrastructure, and provides a robust mechanism to detect sophisticated low-level attacks that bypass source code scrutiny.
• Open-Sourced for Community Benefit: The tool's availability as open-source fosters further research and development in binary-level security analysis, contributing to the broader cybersecurity community.

About the Speaker(s)

Hongwei Wu is the presenter of this work, "VeriBin: Adaptive Verification of Patches at the Binary Level." The research represents a joint effort between Purdue University and Simon Fraser University, indicating his affiliation with these academic institutions. Based on the presentation, Hongwei Wu is actively involved in cutting-edge research in the field of binary analysis and security, focusing on formal methods for software integrity and vulnerability maintenance.