SiMBA is a tool for the simplification of linear mixed Boolean-arithmetic expressions (MBAs). Like MBA-Blast and MBA-Solver, it uses a fully algebraic approach based on the idea that a linear MBA is fully determined by its values on the set of zeros and ones, but leveraging the new insights that a transformation to the 1-bit-space is not necessary for this.

It is based on the following paper:

@inproceedings{simba2022,
    author = {Reichenwallner, Benjamin and Meerwald-Stadler, Peter},
    title = {Efficient deobfuscation of linear mixed Boolean-arithmetic expressions},
    year = {2022},
    month = nov,
    address = {Los Angeles, CA, USA},
    date = {November 7 - 11, 2022},
    booktitle = {Proceedings of the CheckMATE 2022 workshop, co-located with the ACM Conference on Computer and Communication Security, CCS'22},
    pages = {19--28},
    doi = {10.1145/3560831.3564256},
    publisher = {ACM},
    howpublished = {\url{https://arxiv.org/abs/2209.06335}}
}

Find slides and a video recording of the presentation. Also available via ACM.

Content

Two main programs (Python 3) are provided:

• simplify.py for the simplification of single linear MBAs
• simplify_dataset.py for the simplification of a set of linear MBAs contained in a file and their verification via a comparison with corresponding simpler expressions also contained in this file

Additionally, the program check_linear_mba.py can be used for checking whether expressions represent linear MBAs.

Usage

Simplifying single expressions

In order to simplify a single expression expr, use

python3 src/simplify.py "expr"

Alternatively, multiple expressions can be simplified at once, e.g.:

python3 src/simplify.py "x+x" "a&a"

In fact, each command line argument which is not an option is considered as an expression to be simplified. Note that omitting the quotation marks may imply undesired behavior. The simplification results are printed to the command line as shown in the following:

*** Expression x+x
*** ... simplified to 2*x
*** Expression a
*** ... simplified to a

Per default no check whether the input expression is a linear MBA is performed. This check can optionally be enabled via the option -l:

python3 src/simplify.py "x*x" -l

Since