CoBRA

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

So funktioniert es

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.

Funktionen

• Lineare MBA-Vereinfachung — gewichtete Summen bitweiser Atome mittels Signaturvektor und CoB-Transformation
• Skalierter Musterabgleich — k * f(vars) + c mit Shannon-Zerlegung für Boolesche Ausdrücke mit 4–5 Variablen
• Semilineare Unterstützung — Atome mit konstanten Masken inklusive XOR/OR/NOT-AND-Konstanten-Absenkung, Struktur-Rekonstruktion, Term-Verfeinerung und bitpartitionierter Rekonstruktion
• Polynom-Rekonstruktion — multilineare Terme und Einzelpotenzen mittels Koeffizienten-Splitting und finiter Differenzen
• Verarbeitung gemischter Produkte — Zerlegungs-Engine mit Kern-Extraktion, Restterm-Lösung und Klassifizierung von Ghost-Resttermen
• Lifting von Teilausdrücken — ersetzt komplexe Teilbäume durch virtuelle Variablen, um die Problemdimension zu reduzieren
• Worklist-Orchestrator — DAG-bewusste Pass-Planung mit Deduplizierung und begrenzter Suche
• Wettbewerbsgruppen — lokale Alternativ-Zweige und Teil-Lösungen verwenden eine kostenbasierte Gewinnerauswahl mit Continuations
• Konstante Verschiebungen — << wird zu Multiplikation desugart, >> wird über semilineare Techniken vereinfacht
• ANF-Bereinigung — Absorption, Herausfaktorisieren gemeinsamer Würfel und OR-Erkennung
• Konfigurierbare Bitbreite — modulare Arithmetik von 1 bis 64 Bit
• Eliminierung von Hilfsvariablen — reduziert die Variablenanzahl, wenn Terme sich aufheben
• Z3-Verifizierung — optionale Äquivalenzprüfung der vereinfachten Ausgabe
• Stichproben-Selbsttest — leichtgewichtige Validierung mit zufälligen Eingaben, wenn Z3 nicht verfügbar ist
• LLVM-Pass-Plugin — direkte Integration in Compiler-Pipelines (erfordert LLVM 19–22)

Kompilieren

Siehe 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

Mit 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

Verwendung

# 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

Optionen

Projektstruktur