CoBRA

Coefficient-Based Reconstruction of Arithmetic — a Mixed Boolean-Arithmetic expression simplifier.

CoBRA deobfuscates expressions that interleave arithmetic (+, -, *) with bitwise (&, |, ^, ~) and shift (<<, >>) operators — a technique commonly used in software obfuscation.

$ cobra-cli --mba "(x&y)+(x|y)"
x + y

$ cobra-cli --mba "((a^b)|(a^c)) + 65469 * ~((a&(b&c))) + 65470 * (a&(b&c))" --bitwidth 16
67 + (a | b | c)

$ cobra-cli --mba "((a^b)&c) | ((a&b)^c)"
c ^ a & b

$ cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16
x

$ cobra-cli --mba "(x ^ 0x10) + 2 * (x & 0x10)"
16 + x

$ cobra-cli --mba "x << 3"
8 * x

$ cobra-cli --mba "~x"
~x

$ cobra-cli --mba "(x^y)*(x&y) + 3*(x|y)"
(x ^ y) * (x & y) + 3 * (x | y)

$ cobra-cli --mba '-357*(x&~y)*(x&y)+102*(x&~y)*(x&~y)+374*(x&~y)*~(x^y)
  -306*(x&~y)*~(x|y)-17*(x&~y)*~(x|~y)-105*~(x|~y)*(x&y)+30*~(x|~y)*(x&~y)
  +110*~(x|~y)*~(x^y)-90*~(x|~y)*~(x|y)-5*~(x|~y)*~(x|~y)+34*(x&~y)*~x
  -85*(x&~y)*~y+10*~(x|~y)*~x-25*~(x|~y)*~y'
22 * (x & y) + -17 * x + -5 * y

How It Works

CoBRA uses a worklist-based orchestrator to simplify expressions. Each input enters the worklist as a work item tagged with a state kind. A scheduler selects the next pass to run based on the item's state, prerequisite dependencies, and an attempt cache that prevents redundant work.

36 discrete passes are organized into families: AST processing, signature-based techniques, semilinear techniques, decomposition, and lifting. Some passes fork local alternatives or child solves that are resolved by competition groups; outside those groups, the worklist returns the first fully verified top-level candidate. All results are verified by spot-checking random inputs (default) or Z3 equivalence proof (--verify).

Input Expression
       |
  [Worklist Scheduler]
       |
  Work items flow through state kinds:
       |
  kFoldedAst ──> AST processing passes
       |         (classify, lower, rewrite)
       |
       +──> kSignatureState ──> Signature techniques
       |    (pattern match, CoB, ANF, polynomial recovery)
       |
       +──> kSemilinearNormalizedIr ──> Semilinear techniques
       |    (normalize, recover structure, refine, reconstruct)
       |
       +──> kCoreCandidate / kRemainderState ──> Decomposition
       |    (extract core, classify residual, solve)
       |
       +──> kLiftedSkeleton ──> Lifting
       |    (virtual variable substitution, outer solve)
       |
       +──> kCandidateExpr ──> Verification
            (spot-check or Z3 proof)
       |
  Simplified Expression

Signature-based techniques evaluate the expression on all Boolean inputs to get a signature vector. A CoB butterfly transform recovers AND-product basis coefficients. Pattern matching, ANF, and polynomial recovery handle different complexity levels.

Semilinear techniques handle expressions with constant masks (e.g., x & 0xFF). The expression is decomposed into weighted bitwise atoms, then structure recovery and term refinement simplify the intermediate representation, and bit-partitioned OR-assembly reconstructs the final result.

Decomposition targets mixed expressions with products of bitwise subexpressions. A polynomial core is extracted, then residuals are classified and solved (polynomial, boolean-null/ghost, or template fallback).

Lifting replaces complex subexpressions with virtual variables, solves the simplified outer skeleton, then substitutes back.

Features

• Linear MBA simplification — weighted sums of bitwise atoms via signature vector and CoB transform
• Scaled pattern matching — k * f(vars) + c with Shannon decomposition for 4-5 variable Boolean expressions
• Semilinear support — constant-masked atoms with XOR/OR/NOT-AND constant lowering, structure recovery, term refinement, bit-partitioned reconstruction
• Polynomial recovery — multilinear terms and singleton powers via coefficient splitting and finite differences
• Mixed product handling — decomposition engine with core extraction, residual solving, and ghost residual classification
• Subexpression lifting — replace complex subtrees with virtual variables to reduce problem dimension
• Worklist orchestrator — DAG-aware pass scheduling with deduplication and bounded search
• Competition groups — local alternative branches and child solves use cost-based winner selection with continuations
• Constant shifts — << desugars to multiplication, >> simplifies via semilinear techniques
• ANF cleanup — absorption, common-cube factoring, and OR recognition
• Configurable bitwidth — 1-bit to 64-bit modular arithmetic
• Auxiliary variable elimination — reduces variable count when terms cancel
• Z3 verification — optional equivalence checking of simplified output
• Spot-check self-test — lightweight random-input validation when Z3 is unavailable
• LLVM pass plugin — integrate directly into compiler pipelines (requires LLVM 19-22)

Building

See BUILD.md for full details including optional dependencies (LLVM, Z3).

# Build dependencies (Abseil, Highway; optionally GoogleTest, LLVM, Z3)
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release
cmake --build build-deps

# Build CoBRA
cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCMAKE_BUILD_TYPE=Release
cmake --build build

# (Optional) Build and run tests
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release -DCOBRA_BUILD_TESTS=ON
cmake --build build-deps
cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCMAKE_BUILD_TYPE=Release \
  -DCOBRA_BUILD_TESTS=ON
cmake --build build
ctest --test-dir build --output-on-failure

With LLVM Pass Plugin

cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCOBRA_BUILD_LLVM_PASS=ON \
  -DCMAKE_BUILD_TYPE=Release
cmake --build build

Usage

# Basic simplification
cobra-cli --mba "(x&y)+(x|y)"

# Specify bitwidth
cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16

# Enable Z3 equivalence verification
cobra-cli --mba "(a^b)+(a&b)+(a&b)" --verify

# Verbose output (show intermediate pipeline steps)
cobra-cli --mba "(x&y)+(x|y)" --verbose

Options

Project Structure