CoBRA

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

Comment ça marche

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.

Fonctionnalités

• Simplification MBA linéaire — sommes pondérées d'atomes binaires via vecteur de signature et transformée CoB
• Filtrage de motifs à l'échelle — k * f(vars) + c avec décomposition de Shannon pour les expressions booléennes à 4-5 variables
• Support semilinéaire — atomes à masque constant avec abaissement de constantes XOR/OU/NON-ET, récupération de structure, affinage des termes, reconstruction partitionnée par bits
• Récupération polynomiale — termes multilinéaires et puissances singletons via scission de coefficients et différences finies
• Gestion de produits mixtes — moteur de décomposition avec extraction du noyau, résolution des résidus et classification des résidus fantômes
• Élévation de sous-expressions — remplace les sous-arbres complexes par des variables virtuelles pour réduire la dimension du problème
• Orchestrateur à liste de travail — ordonnancement de passes tenant compte des DAG, déduplication et recherche bornée
• Groupes de compétition — les branches alternatives locales et les sous-résolutions utilisent une sélection du vainqueur basée sur le coût avec continuations
• Décalages constants — << est désucré en multiplication, >> est simplifié via les techniques semilinéaires
• Nettoyage FNA (ANF) — absorption, factorisation de cubes communs et reconnaissance de OU
• Largeur de bits configurable — arithmétique modulaire de 1 à 64 bits
• Élimination de variables auxiliaires — réduit le nombre de variables lorsque des termes s'annulent
• Vérification Z3 — vérification optionnelle d'équivalence de la sortie simplifiée
• Auto-test par sondage — validation légère par entrées aléatoires lorsque Z3 n'est pas disponible
• Plugin de passe LLVM — intégration directe dans les pipelines de compilation (nécessite LLVM 19-22)

Compilation

Voir 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

Avec le plugin de passe LLVM

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

Utilisation

# 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

Options

Structure du projet