denuvosoftwaresolutions/simba선형 혼합 부울-산술 표현식의 효율적인 난독화 해제
SiMBA는 선형 혼합 부울-산술 표현식(MBA)의 단순화를 위한 도구입니다. MBA-Blast 및 MBA-Solver와 마찬가지로, 선형 MBA가 0과 1의 집합에 대한 값에 의해 완전히 결정된다는 아이디어에 기반한 완전 대수적 접근 방식을 사용하지만, 이를 위해 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 옵션을 사용하여 지정해야 합니다. 파일의 각 줄에는 복잡한 표현식과 이에 상응하는 더 단순한 표현식이 쉼표로 구분되어 포함되어야 합니다. 예:
(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를 사용한 올바른 단순화의 선택적 검증은 런타임에 영향을 주지만, 복잡한 표현식과 더 단순한 표현식으로 구성된 쌍의 단순화 결과 비교는 그렇지 않다는 점에 유의하십시오.
기본적으로 단순화 결과는 출력되지 않고 이러한 통계만 표시됩니다. 전자에 대한 정보가 필요하면 -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는 $b$가 비트 수일 때 $1$과 $2^b-1$ 사이의 무작위 정수 $a,b$를 사용하여 모든 표현식의 출력을 아핀 함수 $f(x) = ax+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$ 각각에 대해 $2$, $3$ 또는 $4$개의 변수를 사용하는 $1,000$개의 동등한 선형 MBA 데이터셋이 제공됩니다:
$e_1$의 경우 $5$~$7$개 변수에 대한 추가 데이터셋이 제공됩니다. 이러한 MBA는 Zhou et al.이 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
변수의 수는 이론상 무제한이지만 당연히 런타임은 변수 수에 따라 증가합니다. 변수 표기법에는 엄격한 제한이 없습니다. 변수는 문자로 시작해야 하며 문자, 숫자, 밑줄을 포함할 수 있습니다. 예를 들어, 다음 변수 이름은 모두 괜찮습니다:
다음 연산자는 Python에서의 우선순위 순서대로 지원됩니다:
입력 표현식에는 공백을 사용할 수 있습니다. 예를 들어, "x+y" 표현식은 "x + y"로 대신 쓸 수도 있습니다.
연산자의 우선순위를 존중하고 필요한 경우 괄호를 사용하십시오! 예를 들어, $+$가 $|$보다 우선순위가 높기 때문에 $1 + (x|y)$와 $1 + x|y$는 동등하지 않습니다. 후자는 선형 MBA조차 아니라는 점에 유의하십시오.
SMT 솔버 Z3가 필요합니다:
Z3 설치:
sudo apt-get install python3-z3Copyright (c) 2022 Denuvo GmbH, GPLv3에 따라 배포됩니다.