Breaking Mixed Boolean-Arithmetic Obfuscation in Real-World Applications

Breaking Mixed Boolean-Arithmetic Obfuscation in Real-World Applications

Speakers: Tim Blazytko, emproof; Nicolò Altamura

Conference: REcon 2025

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

Overview

Mixed Boolean-Arithmetic (MBA) obfuscation is one of the most mathematically sophisticated code-protection techniques in use today — turning a trivial expression like X + Y into a sprawling tangle of bitwise and arithmetic operations that defeats casual inspection, symbolic execution, and even many automated tools. At REcon 2025, Tim Blazytko (emproof) and Nicolò Altamura delivered a thorough treatment of the state of MBA obfuscation: how it is constructed, what attacks exist to break it, where current binary analysis tooling falls short, and how a new Binary Ninja plugin integrates the best available simplification engines into a practical reverse engineering workflow.

The talk positioned itself at the intersection of academic theory and real-world practice — a space where well-understood algebraic attacks remain largely unimplemented in production tools and where the gap between what researchers know how to do and what practitioners can actually do remains uncomfortably wide.

Background

▶ Watch: Introduction: mixed Boolean-arithmetic (MBA) obfuscation (0:18)

Mixed Boolean-Arithmetic expressions arise from combining two algebraic structures: standard arithmetic operations (addition, subtraction, multiplication) and Boolean operations (AND, OR, XOR, NOT), all computed modulo 2ⁿ for some bit width n. The key insight that makes MBAs useful as an obfuscation primitive is that these two algebras interact in non-trivial ways, making simplification a genuinely hard problem — one that neither human inspection nor automated tools can always solve.

MBAs appear in three main deployment contexts:

• Gaming anti-cheat systems: Protecting game logic, license checks, and memory integrity validation from circumvention.
• Digital Rights Management (DRM): Hiding decryption keys, license validation routines, and content access logic behind layers of transformation.
• Malware: Concealing payload logic, command-and-control communication, and evasion primitives from both static analysis and sandboxed execution.

The speakers demonstrated the core idea with a simple example: the expression X ⊕ (X | Y) + 2 * (X & Y) is in fact equivalent to X + Y. To a human analyst, or to a decompiler that doesn't specifically know to look for MBA patterns, this expression is opaque. With enough nesting and recursive rewriting, even multi-variable additions become essentially unreadable.

Key Findings

▶ Watch: MBA simplification technique: expression rewriting approach (7:30)

Two Classes of MBA Expressions

The speakers drew a sharp distinction between linear MBAs and polynomial MBAs:

• Linear MBAs consist of additions of terms like X, (X & Y), (X ⊕ Y), etc., without any variable-to-variable multiplication. They are complex-looking but mathematically tractable.
• Polynomial MBAs include products of variables, such as (X & Y) * (X ⊕ Z). These multiplication terms make simplification substantially harder and defeat methods that work well on linear forms.

The algebraic research from Lenovo's security team (presented at academic venues) showed that linear MBAs are effectively broken — there exist algebraic attacks that can always simplify them. However, these attacks have not been incorporated into mainstream binary analysis tools. Polynomial MBAs remain a harder open problem.

Construction Techniques

Two construction mechanisms were described in detail:

1. Recursive Rewriting: Starting with a lookup table of nearly a million arithmetic identities, a protector picks a sub-expression, replaces it with an equivalent expression from the database, then feeds the result back as a new input and repeats. After enough iterations, even a simple two-variable sum becomes a multi-line wall of operations.

1. Permutation Polynomials: An invertible function H with its inverse H⁻¹ is applied around a target expression: H⁻¹(H(expr)) equals expr, but the intermediate form is obfuscated. Academic papers on binary permutation polynomials (over modular rings) provide systematic ways to generate these functions.

Both techniques can be combined and applied recursively, creating expressions whose complexity scales with the desired protection strength.

Attacks: State of the Art and Shortcomings

The speakers surveyed the landscape of MBA simplification techniques:

• Algebraic attacks: Exploit mathematical structure directly. The Lenovo-originated work provides powerful tools for linear MBAs, and follow-up research extends coverage to some polynomial forms by first linearizing them. However, none of this is yet available in any usable binary analysis plugin.
• Compiler optimization-based attacks: Running MBA expressions through LLVM or GCC optimization passes has some effect, but is limited. Compilers were not designed to simplify MBA expressions and lack the necessary algebraic rules.
• Symbolic execution: Produces symbolic forms of MBA expressions but does not simplify them. Useful as a precursor to synthesis-based attacks but not as a standalone simplifier.
• Synthesis-based attacks (QSynthesis / msynth): The most powerful practical approach. The core idea is to treat the obfuscated expression as a black box, sample input-output pairs, and use those pairs to look up a precomputed table that maps I/O behavior to the shortest known equivalent expression. Robin David's QSynthesis work (also presented at REcon 2025) formalized this approach. The tool msynth is an open-source Python implementation of this concept built on the MIASM intermediate representation.
• Goomba (Hex-Rays/IDA Pro plugin): A recent synthesis-based IDA decompiler plugin that works well out-of-the-box for linear MBAs. Performance degrades for polynomial and more complex expressions, making it unreliable for hard cases.

The honest summary delivered by the speakers: no single tool handles all MBA forms reliably. msynth requires manual scripting and IR translation. Goomba is convenient but unstable for hard cases. Algebraic attacks that could crack the hard cases haven't been ported to binary tools.

Technical Deep Dive

▶ Watch: Compiler optimizations against MBA: effectiveness analysis (10:00)

QSynthesis: Divide and Conquer Simplification

The synthesis approach used by QSynthesis and msynth operates on the expression's abstract syntax tree:

1. Start at the root of the tree. Sample input-output pairs and query the precomputed lookup table. If a match exists, done.
2. If not, recurse into the left subtree. Find the simplest expression matching that subtree's I/O behavior, name it R0, and substitute.
3. Recurse into the right subtree. Find the simplest match, name it R1, and substitute.
4. Re-attempt the root query with the simplified subtrees. Repeat until the whole tree collapses to a single node.

This divide-and-conquer strategy makes QSynthesis far more flexible than approaches that try to match the entire expression at once.

Binary Analysis Challenges

At the binary level, MBA simplification faces challenges beyond the math itself:

• Extraction: How do you identify which instructions constitute an MBA expression? Symbolic execution can be used, but decompiler output is often more convenient.
• Boundary selection: MBAs can span multiple functions, with parts of the expression computed in one function and consumed two calls down the graph. Identifying where an MBA starts and ends is an unsolved problem for non-local (interprocedural) cases.
• Typecasting: Binary code introduces implicit casts that must be handled explicitly when translating to an algebraic framework.
• Memory operands: The "inputs" to an MBA expression are register values or memory cell contents. Choosing the right abstraction level (RAX vs. the memory address it holds) matters for correctness.

The Binary Ninja Plugin: Obfuscation Analysis

Nicolò Altamura's contribution was a practical integration layer that makes MBA simplification usable inside Binary Ninja. The workflow:

1. Static Single Assignment (SSA): Binary Ninja's built-in SSA form renames every definition site with a unique name, making data flow unambiguous.
2. Backward Slicing: Starting from the target assignment, the plugin recursively replaces each variable reference with its definition, unfolding the expression tree until all leaves are known inputs.
3. IL Translation: The unfolded expression (expressed in Binary Ninja's BNIL) is translated into MIASM's intermediate representation so that msynth can process it.
4. Simplification: The translated expression is submitted to msynth's synthesis engine. The simplified result is substituted back into the Binary Ninja decompiler view.

The plugin — published as the obfuscation-analysis Binary Ninja plugin — supports any architecture that Binary Ninja can lift (x86, x86-64, ARM, MIPS, etc.) because simplification happens at the IR level. It uses msynth as the backend simplification engine.

The plugin demonstrated two real-world results:

• Opaque predicates based on MBA: An MBA expression that always evaluates to zero was correctly identified, immediately revealing that the conditional branch it protected was a dead code path.
• Control flow flattening: In a DRM system using a while(true) / switch dispatcher pattern, the MBA expression computing the initial state was simplified to a constant, revealing the first dispatch target.

Known Limitations of the Plugin

• Backward slicing is limited to intra-basic-block scope. Cross-block slicing introduces soundness issues because of control-flow-dependent definitions.
• MIASM does not support floating-point operations, Intel intrinsics, or control flow constructs within expressions. These cases fail gracefully but cannot be simplified.
• Interprocedural MBA patterns — where the obfuscated expression spans multiple function calls — are not handled.

Demo / Proof of Concept

▶ Watch: SMT/Boolean arithmetic solvers applied to real MBA expressions (17:52)

The demo section showed Binary Ninja screenshots with before-and-after views of the simplification plugin in action:

• A highlighted instruction containing a multi-term MBA expression, shown in its raw BNIL form, was submitted to the plugin. The plugin performed the backward slice to recover the full unfolded expression, translated it to MIASM IR, and returned a simplified form. The simplified expression was then annotated directly in the decompiler view.
• For the opaque predicate case, the result was 0 == 0 (always true or always false), immediately flagging the dead branch.
• For the DRM control-flow-flattening case, simplifying the switch variable produced a known constant representing the first state.

The plugin's GitHub repository (linked in the talk) includes example scripts and documentation for extending the workflow.

Defensive Implications

▶ Watch: Results: successfully simplified real-world MBA expressions (21:02)

From a protection design perspective, the talk highlighted several actionable insights:

• Polynomial MBAs remain more resilient than linear MBAs. Protectors aiming for robustness should prefer polynomial constructions and avoid purely linear ones, which are now algebraically broken.
• Non-local MBAs (where simplification requires interprocedural analysis) impose a significantly higher cost on attackers. Current tools simply cannot handle them.
• Combining obfuscation primitives (MBAs for constants, opaque predicates for control flow, virtualization for critical logic) creates compounding difficulty that no single simplification attack can address.

From a defender/analyst perspective:

• msynth and Goomba are the practical tools available today. Use Goomba first for linear cases; fall back to msynth for harder expressions.
• Binary Ninja's obfuscation-analysis plugin lowers the barrier to applying msynth without manual scripting. For any Binary Ninja user encountering DRM or malware with MBA-heavy code sections, this plugin is the fastest available starting point.
• Algebraic attacks from academia represent the next generation of tooling that binary analysis platforms have not yet absorbed. Following the academic literature (particularly from Lenovo's research group) will indicate where the next practical tools will emerge.

Key Takeaways

1. Linear MBAs are algebraically solved — the math to simplify them completely exists — but the implementations have not reached production binary analysis tools yet.
2. Polynomial MBAs with variable-variable multiplications remain a genuinely hard problem and a sound choice for software protectors.
3. Synthesis-based attacks (QSynthesis, msynth) are the best practical all-rounder today, but require careful setup and fail when the simplest representation of the underlying expression is itself complex.
4. Goomba (IDA) is convenient but unstable for hard cases; msynth is powerful but requires scripting effort.
5. The new Binary Ninja obfuscation-analysis plugin bridges the gap by automating extraction, backward slicing, IR translation, and msynth submission — making synthesis-based simplification accessible without manual effort.
6. Interprocedural MBA (across function boundaries) is an open problem and a practical defense against all current tools.
7. Equality saturation — a compiler optimization technique — is an emerging approach for MBA simplification that may produce future breakthroughs.

About the Speaker(s)

▶ Watch: Conclusions: MBA obfuscation is tractable with right approach (25:23)

Tim Blazytko is a security researcher and co-founder of emproof, a company specializing in software protection for embedded devices. He has given multiple talks at REcon on software obfuscation, binary analysis, and de-obfuscation, and offers training in these disciplines. His work spans both constructive (building protections) and destructive (defeating protections) perspectives on software security.

Nicolò Altamura is a security researcher who collaborated with Tim on the Binary Ninja plugin and the practical tooling integration described in this talk. His contribution focused on the engineering challenges of translating binary analysis IR to MIASM and integrating the msynth simplification engine into a production-grade decompiler plugin.