CoBRA

Coefficient-Based Reconstruction of Arithmetic — un semplificatore di espressioni Mixed Boolean-Arithmetic.

CoBRA deoffusca espressioni che intervallano operatori aritmetici (+, -, *) con operatori bitwise (&, |, ^, ~) e di shift (<<, >>) — una tecnica comunemente utilizzata nell'offuscamento del software.

$ 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

Come Funziona

CoBRA utilizza un orchestratore basato su worklist per semplificare le espressioni. Ogni input entra nella worklist come elemento di lavoro etichettato con un tipo di stato. Uno scheduler seleziona il pass successivo da eseguire in base allo stato dell'elemento, alle dipendenze prerequisito e a una cache dei tentativi che previene il lavoro ridondante.

36 pass distinti sono organizzati in famiglie: elaborazione AST, tecniche basate su firma, tecniche semilineari, decomposizione e lifting. Alcuni pass generano alternative locali o child solves che vengono risolte da gruppi di competizione; al di fuori di questi gruppi, la worklist restituisce il primo candidato di primo livello completamente verificato. Tutti i risultati vengono verificati tramite spot-check su input casuali (default) o prova di equivalenza con Z3 (--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

Le tecniche basate su firma valutano l'espressione su tutti gli input booleani per ottenere un vettore di firma. Una trasformata butterfly CoB recupera i coefficienti della base AND-product. Il pattern matching, l'ANF e il recupero polinomiale gestiscono diversi livelli di complessità.

Le tecniche semilineari gestiscono espressioni con maschere costanti (es. x & 0xFF). L'espressione viene scomposta in atomi bitwise pesati; quindi il recupero della struttura e il raffinamento dei termini semplificano la rappresentazione intermedia, e l'OR-assembly partizionato per bit ricostruisce il risultato finale.

La decomposizione mira a espressioni miste con prodotti di sottoespressioni bitwise. Viene estratto un nucleo polinomiale, quindi i residui vengono classificati e risolti (polinomiale, boolean-null/ghost o fallback basato su template).

Il lifting sostituisce sottoespressioni complesse con variabili virtuali, risolve lo scheletro esterno semplificato e quindi sostituisce all'indietro.

Caratteristiche

• Semplificazione MBA lineare — somme pesate di atomi bitwise tramite vettore di firma e trasformata CoB
• Pattern matching scalato — k * f(vars) + c con decomposizione di Shannon per espressioni booleane a 4-5 variabili
• Supporto semilineare — atomi con maschera costante con lowering costante XOR/OR/NOT-AND, recupero della struttura, raffinamento dei termini, ricostruzione partizionata per bit
• Recupero polinomiale — termini multilineari e potenze singole tramite divisione dei coefficienti e differenze finite
• Gestione di prodotti misti — motore di decomposizione con estrazione del core, risoluzione dei residui e classificazione dei residui ghost
• Lifting di sottoespressioni — sostituisce sottoalberi complessi con variabili virtuali per ridurre la dimensione del problema
• Orchestratore worklist — schedulazione dei pass DAG-aware con deduplicazione e ricerca limitata
• Gruppi di competizione — rami alternativi locali e child solves usano selezione del vincitore basata sui costi con continuazioni
• Shift costanti — << viene desugared in moltiplicazione, >> semplificato tramite tecniche semilineari
• Pulizia ANF — assorbimento, fattorizzazione del cubo comune e riconoscimento OR
• Bitwidth configurabile — aritmetica modulare da 1 a 64 bit
• Eliminazione di variabili ausiliarie — riduce il numero di variabili quando i termini si cancellano
• Verifica Z3 — controllo opzionale di equivalenza dell'output semplificato
• Self-test spot-check — validazione leggera su input casuali quando Z3 non è disponibile
• Plugin pass LLVM — integrazione diretta nelle pipeline del compilatore (richiede LLVM 19-22)

Compilazione

Vedi BUILD.md per tutti i dettagli, incluse le dipendenze opzionali (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

Con il plugin pass LLVM

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

Utilizzo

# 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

Opzioni

Struttura del Progetto