trailofbits/cobraCoefficient-Based Reconstruction of Arithmetic — un simplificateur d'expressions Mixed Boolean-Arithmetic (MBA) pour la désobfuscation
Coefficient-Based Reconstruction of Arithmetic — un simplificateur d'expressions mixtes booléennes-arithmétiques.
CoBRA désobfusque les expressions qui entrelacent des opérateurs arithmétiques (+, -, *) avec des opérateurs binaires (&, |, ^, ~) et de décalage (<<, ) — une technique couramment utilisée dans l'obfuscation logicielle.
>>$ 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 utilise un orchestrateur basé sur une liste de travail (worklist) pour simplifier les expressions. Chaque entrée arrive dans la liste de travail comme un élément de travail étiqueté avec un type d'état. Un ordonnanceur sélectionne la passe suivante à exécuter en fonction de l'état de l'élément, des dépendances prérequises et d'un cache de tentatives qui évite les travaux redondants.
36 passes distinctes sont organisées en familles : traitement de l'AST, techniques basées sur la signature, techniques semilinéaires, décomposition et élévation (lifting). Certaines passes génèrent des alternatives locales ou des sous-résolutions résolues par des groupes de compétition ; en dehors de ces groupes, la liste de travail renvoie le premier candidat de niveau supérieur entièrement vérifié. Tous les résultats sont vérifiés par sondage aléatoire des entrées (par défaut) ou par preuve d'équivalence 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
Les techniques basées sur la signature évaluent l'expression sur toutes les entrées booléennes pour obtenir un vecteur de signature. Une transformée papillon CoB récupère les coefficients de la base de produits ET. Le filtrage de motifs, la forme normale algébrique (ANF) et la récupération polynomiale gèrent différents niveaux de complexité.
Les techniques semilinéaires traitent les expressions avec des masques constants (par exemple x & 0xFF). L'expression est décomposée en atomes binaires pondérés, puis la récupération de structure et l'affinage des termes simplifient la représentation intermédiaire, et un assemblage OU partitionné par bits reconstruit le résultat final.
La décomposition cible les expressions mixtes avec des produits de sous-expressions binaires. Un noyau polynomial est extrait, puis les résidus sont classés et résolus (polynomiaux, nuls booléens/fantômes, ou repli par modèle).
L'élévation (lifting) remplace les sous-expressions complexes par des variables virtuelles, résout le squelette externe simplifié, puis effectue la substitution inverse.
k * f(vars) + c avec décomposition de Shannon pour les expressions booléennes à 4-5 variables<< est désucré en multiplication, >> est simplifié via les techniques semilinéairesVoir BUILD.md pour tous les détails, y compris les dépendances optionnelles (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
| Option | Défaut | Description |
|---|---|---|
--mba <expr> | Expression à simplifier | |
--bitwidth <n> | 64 | Largeur de l'arithmétique modulaire (1-64) |
--max-vars <n> | 16 | Nombre maximal de variables |
--verify | off | Vérification d'équivalence Z3 |
--verbose | off | Afficher les détails internes du pipeline |
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 dispose de 1195 tests couvrant des benchmarks unitaires, d'intégration et de jeux de données :
# 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
Les benchmarks de jeux de données valident sur des expressions obfusquées réelles provenant de multiples sources indépendantes. Voir DATASETS.md pour le rapport complet — 75 126 expressions réparties dans 35 fichiers de jeux de données provenant de 7 sources indépendantes.
{0,1} mais incorrects à pleine largeur (base de produits ET vs multiplication arithmétique). Ceux-ci sont détectés et correctement signalés comme échecs de vérification.Merci à Bas Zweers et à l'équipe Back Engineering pour l'inspiration et les conseils qui ont contribué à façonner ce projet. À voir : leur présentation re//verse 2026 Deobfuscation of a Real World Binary Obfuscator.
Merci également à Jack Royer, Matteo Favaro, Arnau Gàmez et aux autres contributeurs anonymes pour la revue et les tests continus.
Apache-2.0. Les jeux de données de test dans test/datasets/ sont redistribués à partir de projets de recherche tiers sous leurs licences d'origine (principalement GPL-3.0). Voir THIRD_PARTY_LICENSES pour plus de détails.