denuvosoftwaresolutions/simbaفكّ التعتيم الفعّال للتعبيرات المنطقية-الحسابية المختلطة الخطية
SiMBA هي أداة لتبسيط التعبيرات الحسابية-المنطقية المختلطة الخطية (MBAs). مثل MBA-Blast وMBA-Solver، تستخدم نهجًا جبريًا بالكامل يعتمد على فكرة أن تعبير MBA الخطي محدد بالكامل بقيمه على مجموعة الأصفار والآحاد، ولكنها تستفيد من الرؤى الجديدة التي تفيد بأن التحويل إلى فضاء البت الواحد (1-bit-space) ليس ضروريًا لتحقيق ذلك.
تستند إلى الورقة البحثية التالية:
@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 إمكانية ترميز مخرجات جميع التعبيرات بواسطة دوال تآلفية $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$، يتم توفير مجموعات بيانات إضافية لـ $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
عدد المتغيرات غير محدود من الناحية النظرية، لكن زمن التشغيل يزداد بالطبع مع زيادة عدد المتغيرات. لا يوجد قيد صارم على ترميز المتغيرات. يجب أن تبدأ بحرف ويمكن أن تحتوي على أحرف وأرقام وشرطات سفلية. على سبيل المثال، جميع أسماء المتغيرات التالية مقبولة:
يتم دعم العوامل التالية، مرتبة حسب أسبقيتها في بايثون:
يمكن استخدام المسافات البيضاء في تعبيرات الإدخال. على سبيل المثال، يمكن كتابة التعبير "x+y" بدلاً من ذلك كـ "x + y".
يرجى احترام أسبقية العوامل واستخدام الأقواس عند الضرورة! على سبيل المثال، التعبيران $1 + (x|y)$ و$1 + x|y$ غير متكافئين لأن $+$ له أسبقية أعلى من $|$. لاحظ أن الأخير ليس حتى تعبير MBA خطيًا.
محلل SMT Z3 مطلوب
تثبيت Z3:
sudo apt-get install python3-z3حقوق النشر (c) 2022 Denuvo GmbH، مُصدرة بموجب GPLv3.