AwesomeREA.org

Tool

SiMBA

Research tool from Denuvo that simplifies linear mixed Boolean-arithmetic (MBA) expressions, which combine bitwise and integer operations and are used in code obfuscation. Like MBA-Blast and MBA-Solver it works algebraically, using the fact that a linear MBA is fully determined by its values on inputs of zeros and ones: it evaluates the expression on every such combination and rewrites it as a linear combination of basic bitwise expressions, without first translating it to 1-bit space. Python scripts simplify single expressions or whole datasets, can check that an input is linear and can prove the result equivalent with Z3.

Targets
Binary
Category
Native analysis tools
Relationship
Foundation tool
Sources reviewed

Requirements & limits

  • Accompanies Benjamin Reichenwallner and Peter Meerwald-Stadler's paper at the CheckMATE 2022 workshop, co-located with ACM CCS 2022 (DOI 10.1145/3560831.3564256, arXiv 2209.06335); the repository also holds the paper PDF, slides and a talk video. The reviewed main commit dates from 2022-12-12, and there are no releases or packages: the scripts run directly from src/.
  • Needs Python 3; Z3's Python bindings are required by simplify_dataset.py and by the -z verification option of simplify.py. Input is expression text, or a file with one complex expression and its simpler equivalent per line, built from variables, constants and the operators ~, unary minus, *, +, -, &, ^ and |; the tool has no disassembler or decompiler integration. Output constants depend on the bit width, 64 by default and set with -b.
  • Only linear MBAs are handled: the optional -l check rejects nonlinear input such as products of variables, and the README warns that operator precedence follows Python, so parentheses are needed. Result refinement through lookup tables of bitwise expressions covers up to three variables; expressions with more variables keep the generic linear-combination form.
  • For reproducing part of the paper's experiments, data/ holds generated sets of 1,000 equivalent linear MBAs per target function with 2 to 4 variables, plus 5- and 6-variable sets for x+y; the README also mentions 7 variables, which are not in the tree. The datasets assume 64 bits, and simplify_dataset.py reports how many results Z3 verified or matched exactly and the average runtime. There is no test suite or CI, and no results were reproduced in this review.
  • GPL-3.0, copyright 2022 Denuvo GmbH. The reviewed sources establish no REA connection.

About this entry

The description was reviewed against primary sources. This does not establish runtime testing, security auditing or verified compatibility.

Report an outdated entry Suggest a translation fix

Primary sources

  1. README.md GitHub · DenuvoSoftwareSolutions/SiMBA · Revision 2281799
  2. src/simplify.py GitHub · DenuvoSoftwareSolutions/SiMBA · Revision 2281799
  3. src/simplify_dataset.py GitHub · DenuvoSoftwareSolutions/SiMBA · Revision 2281799
  4. src/check_linear_mba.py GitHub · DenuvoSoftwareSolutions/SiMBA · Revision 2281799
  5. data GitHub · DenuvoSoftwareSolutions/SiMBA · Revision 2281799
  6. paper/paper.pdf GitHub · DenuvoSoftwareSolutions/SiMBA · Revision 2281799
  7. LICENSE GitHub · DenuvoSoftwareSolutions/SiMBA · Revision 2281799
  8. https://arxiv.org/abs/2209.06335

More in Native binaries

All 129 entries in Native binaries