GAMBA

GAMBA는 혼합 부울-산술 표현식(MBA)을 단순화하기 위한 도구입니다. GAMBA는 General Advanced Mixed Boolean Arithmetic simplifier의 약자입니다. 선형 대수 단순화 도구 SiMBA를 반복적으로 사용하여 잠재적으로 비선형 입력 MBA의 선형 하위 표현식을 단순화합니다. 전반적으로 핵심 구성 요소는 다음과 같습니다:

추상 구문 트리(AST) 사용
(간단하고 정교한) 변환을 적용하여 선형 하위 표현식 분리
단순화할 수 있는 선형 하위 표현식을 구성할 가능성을 높이기 위한 리팩토링
SiMBA를 사용한 선형 하위 표현식 단순화
비트 연산 내에서 중요하지 않은 상수 및 산술 연산을 일시적으로 제거하기 위한 대체 로직

GAMBA는 다음 논문을 기반으로 하며, 발표에 사용된 슬라이드도 참조하십시오:

@inproceedings{gamba2023,
    author = {Reichenwallner, Benjamin and 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

기본적으로 출력에 나타나는 상수는 0에 가능한 한 가까운 표현으로 보고됩니다. 즉, 위의 경우 -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 파일을 사용하여 논문에 명시된 실험을 재현할 수 있습니다. 기본적으로 6개의 데이터셋에서 GAMBA를 실행합니다:

python3 experiments/tests.py

또는 --linear 또는 -l 옵션을 사용하여 대신 SiMBA를 실행하도록 지시할 수 있습니다. 이 경우 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, dataset/pldi_dataset_linear_MBA.txt, dataset/pldi_dataset_poly_MBA.txt, dataset/pldi_dataset_nonpoly_MBA.txt에서 처음 1000개 표현식
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, LOKI 논문에서 생성된 간단한 참조 진리 표현식($x+y$, $x-y$, $x\&y$, $x|y$, $x^y$)에 대한 MBA 25000개, 깊이 최대 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는 편의상 필요하지만, 작동에 필수적이지는 않습니다. 참고: numpy.quantile을 사용하려면 최소 버전 1.15.0이 필요합니다.

NumPy 설치:

Github 저장소에서: https://github.com/numpy/numpy.git
Debian에서: sudo apt-get install python3-numpy

라이선스

연락처

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

GAMBA

인기

GAMBA

내용

사용법

단일 일반 표현식 단순화

단일 선형 표현식 단순화

실험 재현

데이터셋

MBA 형식

의존성

Z3

NumPy

라이선스

연락처