GAMBA

GAMBA — это инструмент для упрощения смешанных булево-арифметических выражений (MBA). GAMBA расшифровывается как General Advanced Mixed Boolean Arithmetic simplifier (универсальный продвинутый упроститель смешанных булево-арифметических выражений). Он использует алгебраический линейный упроститель SiMBA для итеративного упрощения линейных подвыражений потенциально нелинейного входного MBA. Основные компоненты GAMBA:

• Использование абстрактных синтаксических деревьев (AST)
• Выделение линейных подвыражений с помощью (тривиальных и более сложных) преобразований
• Рефакторинг для увеличения вероятности построения линейных подвыражений, которые можно упростить
• Упрощение линейных подвыражений с помощью SiMBA
• Подстановочная логика для временного избавления от нетривиальных констант и арифметических операций внутри побитовых операций

GAMBA основан на следующей статье, см. также слайды, использованные для презентации:

@inproceedings{gamba2023,
    author = {Reichenwallner, Benjamin; Meerwald-Stadler, Peter},
    title = {Simplification of General Mixed Boolean-Arithmetic Expressions: {GAMBA}},
    address = {Delft, The Netherlands},
    year = {2023},
    month = jul,
    publisher = {IEEE},
    pages = {427--438},
    doi = {10.1109/EuroSPW59978.2023.00053},
    howpublished = {https://arxiv.org/abs/2305.06763},
    booktitle = {Proceedings of the 2nd Workshop on Robust Malware Analysis, WORMA'23, 
                 co-located with the 8th IEEE European Symposium on Security and Privacy}
}

Содержание

Предоставляются две основные программы:

• simplify_general.py для упрощения общих MBA
• simplify.py для упрощения линейных MBA

Кроме того, предоставляется тестовый скрипт для воспроизведения результатов, указанных в статье.

Использование

Упрощение отдельных общих выражений

Для упрощения одного выражения expr используйте:

python3 src/simplify_general.py "expr"

Также можно упростить несколько выражений одновременно, например:

python3 src/simplify_general.py "x+x" "y*y" "a&a"

Фактически, каждый аргумент командной строки, не являющийся опцией, считается выражением для упрощения. Обратите внимание, что опускание кавычек может привести к нежелательному поведению. Результаты упрощения выводятся в командную строку, как показано ниже:

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

Если используется опция -z, результаты упрощения в конечном итоге проверяются на семантическую эквивалентность исходным выражениям с помощью Z3. Это не влияет на вывод командной строки, пока алгоритм работает корректно:

python3 src/simplify_general.py "x+x" -z

Если алгоритм выдаст неверный результат, будет вызвана следующая ошибка:

*** Expression x+x
Error in simplification! Simplified expression is not equivalent to original one!

Кроме того, можно выполнить числовую проверку результатов для всех возможных входных данных до определённого количества бит. Это включается опцией -v, за которой следует максимальное количество бит используемых входных данных:

python3 src/simplify_general.py "x+x" -v 3

В случае неверного результат вывод может выглядеть следующим образом:

*** Expression x+x
*** ... verify via evaluation ... [                    ] 0%
*** ... verification failed for input [1, 0]: orig 1, output 2

Константы, встречающиеся в выходных выражениях GAMBA, могут зависеть от количества бит, используемых для констант, а также переменных. По умолчанию это число равно $64$ и может быть установлено с помощью опции -b:

python3 src/simplify_general.py "-x" -b 32

По умолчанию константы, встречающиеся в выходных данных, выводятся в представлении, максимально близком к нулю. То есть в приведённом выше случае число -1 останется:

*** Expression -x
*** ... simplified to -x

Это поведение можно изменить: с помощью опции -m включается модульное сокращение констант:

python3 src/simplify_general.py "-x" -b 32 -m

Тогда для числа бит $b$ константы всегда лежат между $0$ и $2^b-1$. Следовательно, приведённый выше вызов приведет к следующему выводу:

*** Expression -x
*** ... simplified to 4294967295*x

Упрощение отдельных линейных выражений

Файл src/simplify.py предназначен для использования src/simplify_general.py, но может выполняться и отдельно. Используйте опцию командной строки -h, чтобы увидеть доступные настройки.

Воспроизведение экспериментов

Файл experiments/tests.py можно использовать для воспроизведения экспериментов, описанных в статье. По умолчанию он запускает GAMBA на 6 наборах данных:

python3 experiments/tests.py

Также можно указать запуск SiMBA с помощью опции --linear или -l. В этом случае SiMBA запускается только на MBA с линейными эталонными выражениями:

python3 experiments/tests.py --linear

Числовые проверки или проверки с помощью Z3 включаются опциями --check (-c) или --z3 (-z) соответственно.

Выражения классифицируются в зависимости от успеха упрощения или проверки:

• ok: выражения, упрощённые до точно такого же результата, как соответствующие эталонные выражения
• okz: выражения, эквивалентность которых эталонным выражениям может быть проверена с помощью алгоритма (путём упрощения выражения минус эталонное выражение до 0)
• z3: выражения, эквивалентность которых эталонным выражениям может быть проверена с помощью Z3
• to: выражения, для которых алгоритм превысил тайм-аут
• ng: выражения, для которых упрощение и проверка не увенчались успехом
• nc: выражения, для которых алгоритм (в случае использования SiMBA) не запускался, поскольку эталонные выражения не являются линейными
• err: выражения, для которых произошла ошибка

Наборы данных

Наборы данных для использования с experiments/tests.py находятся в каталоге experiments/datasets/.

• neureduce.txt: Используйте опцию -d 0; взято с https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv (с некоторыми исправлениями)
• mba_obf_linear.txt: Используйте опцию -d 1; взято с https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt (1000 линейных выражений)
• mba_obf_nonlinear.txt: Используйте опцию -d 2; взято с https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt и https://github.com/nhpcc502/MBA-Obfuscator/tree/master/samples/ground.linear.nonpoly.txt (по 500 выражений; с некоторыми исправлениями для неполиномиальных выражений)
• syntia.txt: Используйте опцию -d 3; взято с MBA-Flatten, dataset/dataset_syntia.txt
• mba_flatten.txt: Используйте опцию -d 4; взято с MBA-Flatten, первые 1000 выражений из dataset/pldi_dataset_linear_MBA.txt, dataset/pldi_dataset_poly_MBA.txt, dataset/pldi_dataset_nonpoly_MBA.txt
• qsynth_ea.txt: Используйте опцию -d 5; взято с https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json

Кроме того, в каталоге experiments/datasets/bonus/ предоставляются следующие дополнительные наборы данных (не рассматриваемые в публикации):

• loki_tiny.txt: Используйте опцию -d 6; взято с https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data, 25000 MBA, сгенерированных для статьи LOKI для простых эталонных выражений ($x+y$, $x-y$, $x\&y$, $x|y$, $x^y$), глубиной до 5

Формат MBA

Количество переменных теоретически неограниченно, но, конечно, время выполнения увеличивается с увеличением количества переменных. Строгих ограничений на обозначение переменных нет. Они должны начинаться с буквы и могут содержать буквы, цифры и символы подчёркивания. Например, следующие имена переменных будут корректными:

• $a$, $b$, $c$, ..., $x$, $y$, $z$, ...
• $v0$, $v1$, $v2$, ...
• $v_0$, $v_1$, $v_2$, ...
• $X0$, $X1$, $X2$, ...
• $var0$, $var1$, $var2$, ...
• $var1a$, $var1b$, $var1c$, ...
• ...

Поддерживаются следующие операторы, упорядоченные по приоритету в Python:

• $**$: возведение в степень
• $\mathord{\sim}$, $-$: побитовое отрицание и унарный минус
• $*$: умножение
• $+$, $-$: сумма и разность
• <<: сдвиг влево
• &: конъюнкция
• $\mathbin{^\wedge}$: исключающая дизъюнкция
• $|$: включающая дизъюнкция

Во входных выражениях можно использовать пробелы. Например, выражение "x+y" можно также записать как "x + y".

Учитывайте приоритет операторов и используйте скобки при необходимости! Например, выражения $1 + (x|y)$ и $1 + x|y$ не эквивалентны, поскольку $+$ имеет более высокий приоритет, чем $|$. Обратите внимание, что последнее даже не является линейным MBA.

Зависимости

Z3

SMT-решатель Z3 требуется для simplify_general.py и simplify.py, если используется необязательная проверка упрощённых выражений. Если эта опция не используется, ошибки не возникает, даже если Z3 не установлен.

Установка Z3:

• из репозитория Github: https://github.com/Z3Prover/z3
• в Debian: sudo apt-get install python3-z3

NumPy

Пакет для научных вычислений NumPy требуется из-за лени, но на самом деле не является обязательным для работы. Примечание: требуется версия не ниже 1.15.0 для numpy.quantile.

Установка NumPy:

• из репозитория Github: https://github.com/numpy/numpy.git
• в Debian: sudo apt-get install python3-numpy

Лицензия

Copyright (c) 2023 Denuvo GmbH, выпущено под лицензией GPLv3.

Контакты

• Benjamin Reichenwallner: benjamin(dot)reichenwallner(at)denuvo(dot)com
• Peter Meerwald-Stadler: peter(dot)meerwald(at)denuvo(dot)com