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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Числовые проверки или проверки с помощью 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