trailofbits/cobraCoefficient-Based Reconstruction of Arithmetic — un semplificatore di espressioni Mixed Boolean-Arithmetic (MBA) per la deoffuscazione
# CoBRA
**Co**efficient-**B**ased **R**econstruction of **A**rithmetic — un semplificatore di espressioni Mixed Boolean-Arithmetic.
[](LICENSE)
[](https://en.cppreference.com/w/cpp/23)
[](#testing)
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
```
<details>
<summary>Altri esempi</summary>
```
$ 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
```
</details>
## 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](https://github.com/trailofbits/cobra/blob/master/BUILD.md) per tutti i dettagli, incluse le dipendenze opzionali (LLVM, Z3).
```bash
# 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
```bash
cmake -S . -B build \
-DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
-DCOBRA_BUILD_LLVM_PASS=ON \
-DCMAKE_BUILD_TYPE=Release
cmake --build build
```
## Utilizzo
```bash
# 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
| Flag | Default | Descrizione |
|------|---------|-------------|
| `--mba <expr>` | | Espressione da semplificare |
| `--bitwidth <n>` | 64 | Larghezza dell'aritmetica modulare (1-64) |
| `--max-vars <n>` | 16 | Numero massimo di variabili |
| `--verify` | off | Verifica di equivalenza con Z3 |
| `--verbose` | off | Mostra i dettagli interni della pipeline |
## Struttura del Progetto
```
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
```
## Test
CoBRA ha 1195 test che coprono benchmark unitari, di integrazione e su dataset:
```bash
# 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
```
I benchmark su dataset vengono validati su espressioni offuscate reali provenienti da più fonti indipendenti. Vedi [DATASETS.md](https://github.com/trailofbits/cobra/blob/master/DATASETS.md) per il report completo dei benchmark: 75.126 espressioni in 35 file di dataset da 7 fonti indipendenti.
## Limitazioni Note
- **MBA misti-polinomiali profondamente intervallati** — le espressioni non supportate rimanenti sono prevalentemente AST grandi e fortemente duplicati con operatori aritmetici e bitwise intervallati. Il lifting delle sottoespressioni classificato per impatto recupera molti di questi casi, ma le espressioni che esauriscono il budget della worklist dopo il lifting rimangono non supportate
- **Divergenza di ricostruzione nel dominio booleano** — un piccolo numero di espressioni produce candidati CoB corretti su input `{0,1}` ma errati a piena larghezza (base AND-product vs. moltiplicazione aritmetica). Questi vengono rilevati e correttamente segnalati come verify-failed
- **Nessuna minimizzazione logica generale** — CoBRA usa riscritture algebriche greedy, non Quine-McCluskey/Espresso/BDD
## Ringraziamenti
Grazie a [Bas Zweers](https://github.com/AnalogCyberNuke) e al team di [Back Engineering](https://github.com/backengineering) per l'ispirazione e la guida che hanno contribuito a dare forma a questo progetto. Consigliata la visione del loro talk re//verse 2026 [Deobfuscation of a Real World Binary Obfuscator](https://www.youtube.com/watch?v=3LtwqJM3Qjg).
Un ulteriore ringraziamento a [Jack Royer](https://github.com/Garfield1002), [Matteo Favaro](https://github.com/fvrmatteo), [Arnau Gàmez](https://github.com/arnaugamez) e agli altri contributori anonimi per la revisione e i test continui.
## Licenza
[Apache-2.0](https://github.com/trailofbits/cobra/blob/master/LICENSE). I dataset di test in `test/datasets/` sono ridistribuiti da progetti di ricerca di terze parti secondo le loro licenze originali (principalmente GPL-3.0). Vedi [THIRD_PARTY_LICENSES](https://github.com/trailofbits/cobra/blob/master/THIRD_PARTY_LICENSES) per i dettagli.