mrphrazer/msynthإطار عمل لفك تشويش الشيفرة لتبسيط تعبيرات الحساب المنطقي-الحسابي المختلط (MBA)
المؤلف: Tim Blazytko و Moritz Schloegel
msynth هو إطار عمل لإزالة تشويق الشيفرة (code deobfuscation) لتبسيط تعبيرات الحساب المختلط الثنائي (Mixed Boolean-Arithmetic, MBA). بالنظر إلى أوراكل تبسيط محسوب مسبقًا، فإنه يمر عبر تعبير معقد ممثل كشجرة بنية مجردة (AST) ويحاول تبسيط الأشجار الفرعية باستخدام تقنيات تبسيط جبرية ودلالية متنوعة. بدلاً من ذلك، يحاول تبسيط التعبيرات عبر تخليق البرامج العشوائي.
تم بناء msynth فوق Miasm ومستوحى من الأوراق البحثية
"QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation" بواسطة Robin David و Luigi Coniglio و Mariano Ceccato (NDSS, BAR 2020)،
"Syntia: Synthesizing the Semantics of Obfuscated Code" بواسطة Tim Blazytko و Moritz Contag و Cornelius Aschermann و Thorsten Holz (USENIX Security 2017) و
"Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate" بواسطة Grégoire Menguy و Sébastien Bardin و Richard Bonichon و Cauim de Souza de Lima (CCS 2021).
"Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation" بواسطة Vidal Attias و Nicolas Bellec و Grégoire Menguy و Sébastien Bardin و Jean-Yves Marion (CCS 2025).
"Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions" بواسطة Benjamin Reichenwallner و Peter Meerwald-Stadler (CheckMATE 2022) و
"Simplification of General Mixed Boolean-Arithmetic Expressions: GAMBA" بواسطة Benjamin Reichenwallner و Peter Meerwald-Stadler (WORMA 2023).
يمكن استخدامه بالاقتران مع محرك التنفيذ الرمزي الخاص بـ Miasm لتبسيط التعبيرات المعقدة في الشيفرة المشوشة أو كأداة مستقلة للتلاعب بتبسيط MBA.
original: {((((((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) ^ 0xFFFFFFFF) & RDX[0:32]) + ((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) & (RDX[0:32] ^ 0xFFFFFFFF)) + -(((((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) ^ 0xFFFFFFFF) & RDX[0:32]) + ((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) | (((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32])) + ({RDI[0:32] & ({RDI[0:32] & RSI[0:32] 0 32, 0x0 32 64} * 0x2 + {RDI[0:32] ^ RSI[0:32] 0 32, 0x0 32 64})[0:32] 0 32, 0x0 32 64} * 0x2 + {((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) & RSI[0:32]) + (((RDI + {(RDI[0:32] ^ 0xFFFFFFFF) | RDX[0:32] 0 32, 0x0 32 64} + 0x1)[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + (RDI[0:32] ^ ({RDI[0:32] & RSI[0:32] 0 32, 0x0 32 64} * 0x2 + {RDI[0:32] ^ RSI[0:32] 0 32, 0x0 32 64})[0:32]) + ((RDI[0:32] ^ 0xFFFFFFFF) | RDX[0:32]) + (RDI + RDX + 0x1)[0:32] 0 32, 0x0 32 64})[0:32]) * 0x2 0 32, 0x0 32 64}
simplified: {(-RDX[0:32] + ((RDI[0:32] + RDX[0:32] + RSI[0:32]) << 0x1)) * 0x2 0 32, 0x0 32 64}
لتثبيت msynth اتبع هذه الخطوات:
git clone https://github.com/mrphrazer/msynth.git
cd msynth
# optionally: use a virtual environment
python -m venv msynth-env
source msynth-env/bin/activate
# install dependencies
pip install -r requirements.txt
# install msynth
pip install .
# unzip database
unzip -d database -q database/3_variables_constants_7_nodes.txt.zip
عند تحديث بيئة موجودة، أعد تثبيت التبعيات لالتقاط إصدار Miasm المثبت. قد تُبلغ إصدارات Miasm المختلفة عن نفس إصدار الحزمة، لذا قد يترك التثبيت العادي الإصدار الأقدم مثبتًا:
python -m pip install --force-reinstall -r requirements.txt
لإنشاء أوراكل، نحتاج إلى جدول بحث للتبسيط (أو قاعدة بيانات) يحتوي على عدد كبير من التعبيرات. استخدمنا بحثًا تعداديًا لحساب التعبيرات مسبقًا بحجم بت 8 و16 و32 و64 وفقًا للمواصفات التالية:
حتى خمسة متغيرات p0 و p1 و p2 و p3 و p4
عوامل الاقتطاع (truncation) لخفض المتغيرات (إذا لزم الأمر) إلى 32 و16 و8 بت،
عمليات المتجهات البتية: الجمع والطرح والضرب والنفي (سالب أحادي) والعطف/الفصل/الاستبعاد/النفي البتي والإزاحة المنطقية لليسار،
وبالنسبة لبعض الجداول، الثوابت 0x0 و 0x1 و 0x2 و 0x80 و 0xff و 0x800 و 0xffff و 0x8000_0000 و 0xffff_ffff و 0x8000_0000_0000_0000 و 0xffff_ffff_ffff_ffff.
تحتوي قاعدة البيانات المثالية المضمنة في database على جميع التوليفات البالغ عددها 1,293,020 والتي تم إنشاؤها باستخدام ثلاثة متغيرات والثوابت 0x0 و 0x1 و 0x2 لما يصل إلى 7 عقد (على سبيل المثال، ((p0 + p1) * (p2 ^ 0x2)) أو ((p0 - p2) << (p1 + p2))). يمكن العثور على قواعد بيانات أكبر محسوبة مسبقًا هنا (~31GB غير مضغوطة). لاحظ أن الشيفرة الخاصة بحساب التعبيرات مسبقًا ليست جزءًا من هذا المستودع. نخطط لإصدارها في وقت ما في المستقبل.
كبديل لجداول البحث المحسوبة مسبقًا، يدعم msynth تبسيط التعبيرات عبر تخليق البرامج العشوائي. بالنسبة لتعبير حسابي معقد معين، يمكن لـ msynth تعلم تعبير أقصر يشترك في نفس سلوك المدخلات والمخرجات. في الوقت الحالي، يتم تنفيذه كمكون مستقل. ومع ذلك، نخطط لدمج كلا نهجي التبسيط في المستقبل.
يستخدم مسار التخليق أيضًا قواعد الاستدلال بالبحث المعياري (Search Modulo Inference Rules, Smir) بشكل افتراضي، وفقًا لورقة CCS 2025 المرتبطة أعلاه. يعزز Smir البحث المحلي من خلال اشتقاق مرشحين قريبين للأنماط الصعبة التخليق مثل الثوابت العشوائية والأقنعة والإزاحات والدورانات الثابتة والتعبيرات الأفينية والتعبيرات متعددة الحدود المحدودة.
أولاً، لنقم بإنشاء أوراكل تبسيط يستخدم قاعدة بيانات تبسيط محسوبة مسبقًا كمدخل ويجمع التعبيرات الموجودة فيها في فئات تكافؤ.
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.pickle
msynth - INFO: Computing oracle for 30 variables and 50 samples.
Using library at 'database/3_variables_constants_7_nodes.txt'
msynth - INFO: Writing oracle to oracle.pickle
msynth - INFO: Done in 632.84 seconds
اعتمادًا على حجم قاعدة بيانات التبسيط المحسوبة مسبقًا، قد يستغرق هذا بضع دقائق أو ساعات، حسب جهاز الكمبيوتر الخاص بك. بدلاً من ذلك، يمكنك استخدام oracle.pickle المحسوب مسبقًا.
اختياريًا، يمكن استخدام علامة --sqlite لإنشاء الأوراكل بتنسيق SQLite، مما يتيح التحميل الكسول وأوقات بدء تشغيل أسرع بكثير:
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite
بعد ذلك، يمكن استخدام الأوراكل المُسلسل لتبسيط التعبيرات المعقدة:
from msynth import Simplifier
# initialize simplifier
simplifier = Simplifier(oracle_path)
# simplify expression
simplified = simplifier.simplify(expression)
بدلاً من ذلك، يمكننا تبسيط التعبيرات المعقدة عبر تخليق البرامج وتعلم التعبيرات بنفس سلوك المدخلات والمخرجات:
from msynth import Synthesizer
# initialize synthesizer
synthesizer = Synthesizer()
# simplify via program synthesis
simplified = synthesizer.simplify(expression)
من الممكن أيضًا دمج تبسيط التعبيرات مع محرك التنفيذ الرمزي الخاص بـ Miasm:
$ python scripts/symbolic_simplification.py samples/mba_challenge 0x1290 oracle.pickle
[snip]
before: {({RDI[0:32] & RSI[0:32] 0 32, 0x0 32 64} * 0x2 + {RDI[0:32] ^ RSI[0:32] 0 32, 0x0 32 64})[0:32] 0 32, 0x0 32 64}
simplified: {RDI[0:32] + RSI[0:32] 0 32, 0x0 32 64}
[snip]
يمكن العثور على أمثلة استخدام إضافية في دليل scripts.