SiMBA

SiMBA — это инструмент для упрощения линейных смешанных булево-арифметических выражений (MBA). Как и MBA-Blast и MBA-Solver, он использует полностью алгебраический подход, основанный на идее, что линейное MBA полностью определяется своими значениями на множестве нулей и единиц, но использует новые наблюдения, согласно которым для этого не требуется преобразование в 1-битовое пространство.

Он основан на следующей статье:

@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}}
}

С презентацией можно ознакомиться по слайдам и видеозаписи. Также доступна через ACM.

Содержимое

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

simplify.py для упрощения отдельных линейных MBA
simplify_dataset.py для упрощения набора линейных MBA, содержащихся в файле, и их проверки путём сравнения с соответствующими более простыми выражениями, также содержащимися в этом файле

Кроме того, программа check_linear_mba.py может использоваться для проверки того, являются ли выражения линейными MBA.

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

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

Чтобы упростить отдельное выражение expr, используйте

python3 src/simplify.py "expr"

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

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

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

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

По умолчанию проверка того, является ли входное выражение линейным MBA, не выполняется. Эту проверку можно дополнительно включить с помощью опции -l:

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

Поскольку $x*x$ не является линейным MBA, в этом случае появится следующий вывод:

*** Expression x*x
Error: Input expression may be no linear MBA: x*x

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

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

Это приведёт к следующей ошибке:

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

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

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

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

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

Упрощение и проверка выражений из файла

Чтобы упростить выражения, сохранённые в файле с путём path_to_file, используйте

python3 src/simplify_dataset.py -f path_to_file

То есть файл должен быть указан с помощью опции -f. Каждая строка файла должна содержать сложное выражение и эквивалентное ему более простое, разделённые запятой, например:

example-expressions.txt:

(x&y)+(x|y), x+y
(x|y)-(~x&y)-(x&~y), x&y
-(a|~b)+(~b)+(a&~b)+b, a^b
2*(s&~t)+2*(s^t)-(s|t)+2*~(s^t)-~t-~(s&t), s

Для каждой строки упрощаются как сложное, так и простое выражение, после чего они сравниваются. Причина упрощения последнего — сделать результаты проверки независимыми от пробелов, порядка множителей или слагаемых и т. д.

Как и в simplify.py, проверку линейности и проверку корректности упрощения можно включить с помощью опций -l и -z соответственно, а количество битов можно задать с помощью опции -b. Если требуется запустить SiMBA только на определённом максимальном числе выражений из указанного файла, это максимальное число можно задать через опцию -r:

python3 src/simplify_dataset.py -f some_file.txt -r 2

Если бы some_file.txt содержал выражения, перечисленные выше, были бы упрощены только первые два из них:

Simplify expressions from data/some_file.txt ...
  * total count: 2
  * verified: 2
  * equal: 2
  * average duration: 0.00014788552653044462

В любом случае вывод содержит информацию о

общем количестве выражений во входных данных,
количестве выражений, которые после упрощения удалось проверить с помощью Z3 на эквивалентность соответствующему более простому выражению (если только результат упрощения уже не имеет точно такого же строкового представления),
количестве выражений, которые упрощаются до того же самого выражения, что и соответствующее простое выражение, и
среднем времени выполнения в секундах.

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

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

python3 src/simplify_dataset.py -f some_file.txt -v

В этом случае будет показан следующий вывод:

Simplify expressions from data/some_file.txt ...

    *** 1 groundtruth x+y, simplified x+y => equal: True, verified: True
    *** 2 groundtruth x&y, simplified x&y => equal: True, verified: True
    *** 3 groundtruth a^b, simplified a^b => equal: True, verified: True
    *** 4 groundtruth s, simplified s => equal: True, verified: True

  * total count: 4
  * verified: 4
  * equal: 4
  * average duration: 0.00016793253598734736

Другая опция -e даёт возможность закодировать выходные значения всех выражений аффинными функциями $f(x) = ax+b$ со случайными целыми числами $a,b$ в диапазоне от $1$ до $2^b-1$, где $b$ — количество битов:

python3 src/simplify_dataset.py -f some_file.txt -v -e

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

Simplify expressions from data/some_file.txt ...

    *** 1 groundtruth 10623056950310032687+5038261596809828791*x+5038261596809828791*y, simplified 10623056950310032687+5038261596809828791*x+5038261596809828791*y => equal: True, verified: True
    *** 2 groundtruth 15181401701264988765+3962868592131193124*(x&y), simplified 15181401701264988765+3962868592131193124*(x&y) => equal: True, verified: True
    *** 3 groundtruth 6812440940417974076+11894131080657788315*(a^b), simplified 6812440940417974076+11894131080657788315*(a^b) => equal: True, verified: True
    *** 4 groundtruth 4558303267887122851+10271005790757592209*s, simplified 4558303267887122851+10271005790757592209*s => equal: True, verified: True

  * total count: 4
  * verified: 4
  * equal: 4
  * average duration: 0.00019435951253399253

Воспроизводимость

Для воспроизведения части экспериментов, описанных в статье, можно использовать любой из файлов наборов данных, содержащихся в каталоге data/. Для каждой из следующих функций $e_1,\ldots, e_5$ предоставлены наборы данных из $1,000$ эквивалентных линейных MBA, использующих $2$, $3$ или $4$ переменных:

$e_1(x,y) = x+y$
$e_2 = 49,374$
$e_3(x) = 3,735,936,685, x + 49,374$
$e_4(x,y) = 3,735,936,685, (x\mathbin{^\wedge}y) + 49,374$
$e_5(x) = 3,735,936,685\cdot \mathord{\sim} x$

Для $e_1$ предоставлены дополнительные наборы данных для $5$–$7$ переменных. Эти MBA были сгенерированы с помощью алгоритма, основанного на методе, описанном Чжоу и др. в 2007 году и описанном в статье.

Обратите внимание, что эти наборы данных были сгенерированы для $b=64$ бит. Для других количеств битов их эквивалентность $e_i$ не может быть гарантирована.

Для воспроизведения дальнейших экспериментов мы отсылаем к наборам данных, предоставленным репозиторием MBA-Solver и репозиторием NeuReduce, соответственно.

Проверка линейности

Файл check_linear_mba.py используется упростителем, но также предоставляет собственный интерфейс, например:

python3 src/check_linear_mba.py "x+x" "x*x"

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

*** Expression x+x
*** +++ valid
*** Expression x*x
*** --- not valid

Формат 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.

Зависимости

Требуется SMT-решатель Z3

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

Установка Z3:

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

Лицензия

Контакты

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

SiMBA

Популярное

SiMBA

Содержимое

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

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

Упрощение и проверка выражений из файла

Воспроизводимость

Проверка линейности

Формат MBA

Зависимости

Лицензия

Контакты