GAMBA

GAMBA هي أداة لتبسيط التعبيرات المختلطة البوليانية-الحسابية (MBAs). GAMBA اختصار لـ General Advanced Mixed Boolean Arithmetic simplifier. تستخدم المبسط الجبري الخطي SiMBA لتبسيط التعابير الفرعية الخطية بشكل تكراري لمُدخل MBA قد يكون غير خطي. بشكل عام، مكوناتها الأساسية هي التالية:

• استخدام أشجار البنية المجردة (ASTs)
• عزل التعابير الفرعية الخطية عبر تطبيق تحويلات (بسيطة وأكثر تطورًا)
• إعادة هيكلة من أجل زيادة فرصة بناء تعابير فرعية خطية يمكن تبسيطها
• تبسيط التعابير الفرعية الخطية باستخدام 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 لتبسيط MBAs العامة
• simplify.py لتبسيط MBAs الخطية

بالإضافة إلى ذلك، يتم توفير سكربت اختبار لإعادة إنتاج النتائج المذكورة في الورقة البحثية.

الاستخدام

تبسيط التعابير العامة المفردة

من أجل تبسيط تعبير واحد 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، يتم تفعيل الاختزال المعياري (modulo) للثوابت:

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 فقط على MBAs ذات الحقائق الأساسية الخطية:

python3 experiments/tests.py --linear

يمكن تفعيل الفحوصات العددية أو الفحوصات باستخدام Z3 عبر الخيارين --check (-c) أو --z3 (-z) على التوالي.

يتم تصنيف التعابير اعتمادًا على نجاح التبسيط أو التحقق:

• ok: التعابير التي يتم تبسيطها إلى نفس النتيجة تمامًا مثل الحقائق الأساسية المقابلة
• okz: التعابير التي يمكن التحقق من تكافؤها مع الحقائق الأساسية باستخدام الخوارزمية (عن طريق تبسيط التعبير مطروحًا منه تعبير الحقيقة الأساسية إلى 0)
• z3: التعابير التي يمكن التحقق من تكافؤها مع الحقائق الأساسية باستخدام Z3
• to: التعابير التي واجهت الخوارزمية فيها مهلة زمنية (timeout)
• 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

صيغة MBAs

عدد المتغيرات غير محدود من الناحية النظرية، ولكن بالطبع يزداد وقت التشغيل مع عدد المتغيرات. لا يوجد قيد صارم على تدوين المتغيرات. يجب أن تبدأ بحرف ويمكن أن تحتوي على أحرف وأرقام وشرطات سفلية. على سبيل المثال، جميع أسماء المتغيرات التالية ستكون مقبولة:

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

عوامل التشغيل التالية مدعومة، مرتبة حسب أسبقيتها في بايثون:

• $**$: الأس
• $\mathord{\sim}$, $-$: النفي البتي والسالب الأحادي
• $*$: الضرب
• $+$, $-$: الجمع والطرح
• <<: الإزاحة لليسار
• &: الاقتران (AND)
• $\mathbin{^\wedge}$: الانفصال الحصري (XOR)
• $|$: الانفصال الشامل (OR)

يمكن استخدام المسافات البيضاء في تعابير الإدخال. على سبيل المثال، يمكن كتابة التعبير "x+y" بدلاً من ذلك كـ "x + y".

يرجى احترام أسبقية العوامل واستخدام الأقواس عند الضرورة! على سبيل المثال، التعبيران $1 + (x|y)$ و $1 + x|y$ ليسا متكافئين لأن $+$ له أسبقية أعلى من $|$. لاحظ أن الأخير ليس حتى MBA خطيًا.

التبعيات

Z3

أداة حل SMT Z3 مطلوبة من قبل simplify_general.py و simplify.py إذا تم استخدام التحقق الاختياري من التعابير المبسطة. إذا لم يتم استخدام هذا الخيار، فلن يتم إلقاء أي خطأ حتى إذا لم يتم تثبيت Z3.

تثبيت Z3:

• من مستودع جيثب: https://github.com/Z3Prover/z3
• على دبيان: sudo apt-get install python3-z3

NumPy

حزمة الحوسبة العلمية NumPy مطلوبة بسبب الكسل، ولكنها ليست ضرورية حقًا للتشغيل. ملاحظة: مطلوب الإصدار 1.15.0 على الأقل لـ numpy.quantile

تثبيت NumPy:

• من مستودع جيثب: https://github.com/numpy/numpy.git
• على دبيان: sudo apt-get install python3-numpy

الترخيص

حقوق النشر (c) 2023 Denuvo GmbH، صدر بموجب GPLv3.

الاتصال

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