Skip to content
Reverse Engineering
Obfuscationadvanced

Mixed Boolean Arithmetic (MBA)

Des opérations simples sont remplacées par des mélanges sémantiquement équivalents d'opérateurs arithmétiques et booléens, déjouant la reconnaissance de motifs et la simplification du décompilateur tout en préservant le résultat.

L'obfuscation par Mixed Boolean Arithmetic (MBA) réécrit une opération simple sous la forme d'une expression équivalente qui mélange opérateurs arithmétiques (+, -, *) et bit à bit (^, &, |, ~). Les deux formes calculent la même valeur pour toutes les entrées, mais la forme obfusquée est volumineuse, peu familière et hors des règles de réécriture que connaissent les décompilateurs et les moteurs de reconnaissance de motifs — l'intention d'origine est ainsi cachée à la vue de tous.

Fonctionnement

La technique repose sur des identités vraies sur les entiers machine. Une addition ou un XOR peut être développé en un enchevêtrement de termes booléens et arithmétiques ; imbriquer ces identités produit des expressions arbitrairement complexes mais qui préservent la valeur.

c
// before
z = x + y;
w = x ^ y;

// after (semantically identical for all x, y)
z = (x ^ y) + 2 * (x & y);
w = (x | y) - (x & y);

// nested deeper, a single XOR can become:
w = ((x | y) - (x & y)) + ((~x & y) - (x & ~y)) - ((~x & y) - (x & ~y));

Détection & contournement

  • Statique — Dans IDA/Ghidra, une ligne de source triviale se décompile en une longue chaîne de and/or/xor/not/add/sub sans objectif apparent, réutilisant souvent les deux mêmes variables. Une MBA linéaire apparaît comme une somme pondérée de termes bit à bit sur un petit ensemble d'entrées — cette forme est la signature.
  • Dynamique — Traitez l'expression comme une fonction boîte noire de ses entrées et récupérez-la par synthèse de programme ou recherche guidée par oracle (msynth, l'approche de type gooMBA), ou échantillonnez des couples entrée/sortie pour ajuster une combinaison linéaire plus simple.
  • Patch / simplification — Prouvez l'équivalence entre l'expression obfusquée et une forme simple candidate par bit-blasting et un solveur SMT (Z3), puis substituez la forme simple dans la décompilation. Des simplifieurs spécialisés traitent directement le cas linéaire courant.
  • Outils — SiMBA et MBA-Blast pour les MBA linéaires, GAMBA pour les cas non linéaires, Arybo et msynth pour la manipulation/synthèse symbolique, et Z3 pour vérifier l'équivalence avant de patcher.
Votes

Commentaires(0)