
Koeffizientenbasierte Rekonstruktion von Arithmetik — ein Vereinfacher für Mixed-Boolean-Arithmetic-Ausdrücke (MBA) zur Deobfuskation
Coefficient-Based Reconstruction of Arithmetic — ein Vereinfacher für Mixed-Boolean-Arithmetic-Ausdrücke.
CoBRA deobfuskiert Ausdrücke, die Arithmetik (+, -, *) mit bitweisen Operatoren (&, |, ^, ~) und Schiebeoperatoren (<<, ) verschachteln — eine Technik, die häufig bei der Software-Obfuskation eingesetzt wird.
>>$ 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
CoBRA verwendet einen worklist-basierten Orchestrator zur Vereinfachung von Ausdrücken. Jede Eingabe gelangt als Arbeitselement mit einer Statusart in die Worklist. Ein Scheduler wählt den nächsten auszuführenden Pass basierend auf dem Status des Elements, den Voraussetzungsabhängigkeiten und einem Attempt-Cache aus, der redundante Arbeit verhindert.
36 einzelne Pässe sind in Familien organisiert: AST-Verarbeitung, signaturbasierte Techniken, semilineare Techniken, Zerlegung und Lifting. Einige Pässe verzweigen lokale Alternativen oder Teil-Lösungen, die von Wettbewerbsgruppen aufgelöst werden; außerhalb dieser Gruppen gibt die Worklist den ersten vollständig verifizierten Top-Level-Kandidaten zurück. Alle Ergebnisse werden durch Stichprobenprüfung mit zufälligen Eingaben (Standard) oder durch Z3-Äquivalenzbeweis (--verify) verifiziert.
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
Signaturbasierte Techniken werten den Ausdruck mit allen Booleschen Eingaben aus, um einen Signaturvektor zu erhalten. Eine CoB-Schmetterlingstransformation gewinnt die Koeffizienten der AND-Produkt-Basis zurück. Musterabgleich, ANF und Polynom-Rekonstruktion bewältigen unterschiedliche Komplexitätsstufen.
Semilineare Techniken behandeln Ausdrücke mit konstanten Masken (z. B. x & 0xFF). Der Ausdruck wird in gewichtete bitweise Atome zerlegt; anschließend vereinfachen Struktur-Rekonstruktion und Term-Verfeinerung die Zwischendarstellung, und eine bitpartitionierte OR-Rekonstruktion setzt das Endergebnis wieder zusammen.
Zerlegung zielt auf gemischte Ausdrücke mit Produkten bitweiser Teilausdrücke ab. Ein polynomialer Kern wird extrahiert; danach werden Restterme klassifiziert und gelöst (polynomial, boolesch-null/Ghost oder Template-Fallback).
Lifting ersetzt komplexe Teilausdrücke durch virtuelle Variablen, löst das vereinfachte äußere Gerüst und substituiert anschließend zurück.
k * f(vars) + c mit Shannon-Zerlegung für Boolesche Ausdrücke mit 4–5 Variablen<< wird zu Multiplikation desugart, >> wird über semilineare Techniken vereinfachtSiehe BUILD.md für vollständige Details einschließlich optionaler Abhängigkeiten (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
cmake -S . -B build \
-DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
-DCOBRA_BUILD_LLVM_PASS=ON \
-DCMAKE_BUILD_TYPE=Release
cmake --build build
# 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
| Flag | Standard | Beschreibung |
|---|---|---|
--mba <expr> | Zu vereinfachender Ausdruck | |
--bitwidth <n> | 64 | Breite der modularen Arithmetik (1–64) |
--max-vars <n> | 16 | Maximale Variablenanzahl |
--verify | aus | Z3-Äquivalenzprüfung |
--verbose | aus | Pipeline-Interna ausgeben |
lib/core/ Core simplification engine (~50 source files)
Orchestrator Worklist scheduler, state machine, main simplification loop
OrchestratorPasses 39-pass registry with DAG-aware scheduling
CompetitionGroup Multi-technique racing and winner selection
ContinuationTypes Deferred recombination data for pass composition
JoinState Multi-operand join tracking for structural rewrites
SignatureSimplifier Signature-based techniques (CoB, pattern matching, ANF)
SignatureVector Evaluate expression on {0,1}^n inputs
AuxVarEliminator Reduce variable count by detecting cancellations
PatternMatcher Recognize bitwise patterns (2-var/3-var tables, scaled)
CoeffInterpolator Butterfly interpolation for coefficient recovery
CoBExprBuilder Reconstruct expressions from CoB coefficients
AnfTransform Algebraic Normal Form conversion
AnfCleanup Absorption, factoring, OR recognition
CoefficientSplitter Separate bitwise vs. arithmetic contributions
ArithmeticLowering Lower arithmetic fragment to polynomial IR
PolyNormalizer Canonical form for polynomial expressions
SingletonPowerRecovery Detect x^k terms via finite differences
DecompositionEngine Extract-solve loop: polynomial core + residual solving
GhostBasis Ghost primitive library (mul_sub_and, mul3_sub_and3)
GhostResidualSolver Boolean-null classification and ghost residual solving
WeightedPolyFit 2-adic weighted linear solve for polynomial quotients
MixedProductRewriter Expand bitwise products into linear sums
TemplateDecomposer Bounded template matching for mixed expressions
ProductIdentityRecoverer Recover product-of-sums identities
SemilinearNormalizer Decompose into weighted bitwise atoms
SemilinearSignature Per-bit signature evaluation and linear shortcut
StructureRecovery XOR recovery, mask elimination, term coalescing
TermRefiner Dead-bit mask reduction, same-coefficient merge
BitPartitioner Group bit positions by semantic profile
MaskedAtomReconstructor Reassemble with OR-rewrite for disjoint masks
Evaluator Compiled expression evaluator
lib/llvm/ LLVM pass plugin (CobraPass, MBADetector, IRReconstructor)
lib/verify/ Z3-based equivalence verification
include/cobra/ Public headers
tools/cobra-cli/ CLI frontend and expression parser
test/ 1195 tests across ~63 test files
CoBRA hat 1195 Tests, die Unit-, Integrations- und Datensatz-Benchmarks abdecken:
# Run all tests
ctest --test-dir build --output-on-failure
# Run a specific test suite
ctest --test-dir build -R test_simplifier --output-on-failure
# Run with verbose output
ctest --test-dir build -V
Datensatz-Benchmarks validieren anhand realer obfuskierter Ausdrücke aus mehreren unabhängigen Quellen. Siehe DATASETS.md für den vollständigen Benchmark-Bericht — 75.126 Ausdrücke in 35 Datensatzdateien aus 7 unabhängigen Quellen.
{0,1}-Eingaben korrekt, bei voller Bitbreite jedoch falsch sind (AND-Produkt-Basis vs. arithmetische Multiplikation). Diese werden erkannt und korrekt als „Verifizierung fehlgeschlagen“ gemeldetDank an Bas Zweers und das Back Engineering-Team für die Inspiration und Anleitung, die zur Gestaltung dieses Projekts beigetragen haben. Empfohlener Vortrag: ihr re//verse-2026-Talk Deobfuscation of a Real World Binary Obfuscator.
Zusätzlicher Dank an Jack Royer, Matteo Favaro, Arnau Gàmez und andere anonyme Mitwirkende für das kontinuierliche Review und Testen.
Apache-2.0. Testdatensätze in test/datasets/ werden aus Forschungsprojekten Dritter unter deren ursprünglichen Lizenzen (hauptsächlich GPL-3.0) weiterverteilt. Siehe THIRD_PARTY_LICENSES für Details.