🌟 Strilight

رفع حلقات SMT عالي الأداء $O(1)$ ونطاق الفواصل المتباعدة (Strided Interval Domain) لتحليل ثنائيات x86_64

📖 1. نظرة عامة والمشكلة الأساسية

محركات التنفيذ الرمزي التقليدية (Symbolic Execution) والتنقيح الديناميكي للبرامج الثنائية (DBI) (مثل angr أو Triton أو KLEE) تعاني من مشكلة انفجار المسارات والحلقات سيئة السمعة. عند مواجهة [...][...]

Strilight تحل هذه المشكلة جذريًا عبر معالجة الحلقات كـتكرارات جبرية مغلقة الصيغة (closed-form) ضمن نطاق الفواصل المتباعدة:

$$\vec{\mathbf{R}}(N) = \vec{\mathbf{R}}_0 + \vec{\boldsymbol{\Delta}} \cdot N$$

بدلًا من محاكاة $N$ تكرار، تقوم Strilight بضغط تتبعات التنفيذ المتكررة في بنى LoopBlock هرمية، وتقيّم خطواتها التجريدية الأفينية ومتعددة الدورات، وترفع [...]

⚡ 2. الابتكارات المعمارية الرئيسية

graph LR
    A[Raw Machine Code / Trace] --> B[sl.disassemble & sl.compress]
    B --> C[sl.evaluate / LoopEvaluator]
    C -->|Strided Interval Domain| D[LoopSummary + Invariant Contract]
    D -->|O1 Closed-Form Lifting| E["Z3 SMT-LIB2 Solver"]
    E --> F[Instant Solution in less than 100 ms]

1. ضغط التتبع بدون فكّ الحلقات (Zero-Unroll): يحدد الحواف الراجعة ويضغط ملايين تتبعات التعليمات الخطية في رسوم بيانية هرمية مضغوطة لـLoopBlock في أقل من $<1\text{ ms}$.
2. نطاق الفواصل المتباعدة وVSA ثنائي القناع: يتتبع تحولات المسجلات والذاكرة باستخدام الخطوات والتطابقات النمطية: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. استخراج الأنماط متعددة الدورات والدورية: يكتشف تحولات الذاكرة والمسجلات الفرعية الدورية المعقدة ($P > 1$).
4. عقد الثبات الحديدي: يصيغ شرط حدود الخروج الأول الدقيق لمنع حلول SMT من "الانتقال الآني" عبر حدود إنهاء الحلقة: $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. بنية معيارية مفصولة: فك تجميع أصلي عبر Capstone مع جسور تتبع مخصصة قابلة للتركيب.

🚀 3. ملفات التوزيع المعيارية

تم تعبئة Strilight كملفات معيارية مستقلة بحيث لا تحمل إلا المكوّنات التي يحتاجها خط أنابيبك:

# Profile 1: Core Engine (Pure Compressor + Embedded Def-Use Slicer + Capstone)
pip install strilight

# Profile 2: Symbolic Engine (Core Compressor + Z3 O(1) SMT Lifter)
pip install strilight[solver]

# Profile 3: Dynamic Slicing Suite (Core Compressor + Full PathTree Backward/Forward Tracker)
pip install strilight[tracker]

# Profile 4: Complete Bundle (All Engines + Full Tracker + Z3 Solver)
pip install strilight[all]

🧪 4. تصنيف مجموعة الاختبارات والتحقق

تتحقق مجموعة الاختبارات من صحة كل وحدة بمعدل نجاح 100% عبر الطبقات المفصولة:

الطبقة 1: اختبارات الضاغط الأساسي والتفسير المجرد (يتطلب strilight)

لا تبعيات حلول ثقيلة. تعمل في $<1\text{ second}$ على أي منصة:

الطبقة 2: اختبارات التقطيع الديناميكي ومتعقب التبعيات (يتطلب strilight[tracker])

يتحقق من تتبع تدفق البيانات الديناميكي الكامل وتبعيات التحكم:

الطبقة 3: اختبارات رافع SMT الرمزي والحلّال (يتطلب strilight[solver])

يتحقق من توليد معادلات BitVector والاستبدالات الظلية وحل قيود Z3:

💡 5. بدء سريع: 3 طرق لاستخدام Strilight

الخيار أ: تحليل حلقة بسطر واحد (sl.analyze)

حلّل أي حلقة كود آلة خام x86-64 واستخرج تحويلها مغلق الصيغة في سطر واحد:

import strilight as sl

# Loop bytecode: add eax, 8; sub ebx, 3; inc ecx; cmp ecx, 100000; jl 0x1000
loop_bytes = bytes.fromhex("83c008 83eb03 ffc1 81f9a0860100 7ced")

# ONE-LINE ANALYSIS:
summary = sl.analyze(loop_bytes, iterations=100000)

print(summary.deltas)
# Output: {'eax': 8, 'ebx': -3, 'ecx': 1}

# View the mathematical invariant contract:
print(summary.invariant_contract.to_dict())

الخيار ب: فك التجميع والضغط والتقييم خطوة بخطوة

import strilight as sl

# 1. Disassemble machine code bytes
instructions = sl.disassemble(loop_bytes, base_address=0x1000)

# 2. Package into a symbolic loop block
block = sl.LoopBlock(body=instructions, iterations=100000)

# 3. Extract closed-form mathematical steps (Deltas & Exit Predicates)
summary = sl.evaluate(block)
print(f"Exit Condition: {summary.exit_condition}")

الخيار ج: حل SMT فوري $O(1)$ باستخدام Z3

احسب عدد التكرارات ($N$) أو مفتاح الإدخال المطلوب لتحقيق شرط هدف في أقل من $<100\text{ ms}$:

import strilight as sl
import z3

# Disassemble and evaluate
summary = sl.analyze(loop_bytes, iterations=100000)

# Initialize Z3 translator
translator = sl.Z3Translator()
translator.solver.add(translator.get_register('eax') == 0)
translator.solver.add(translator.get_register('ebx') == 500000)
translator.solver.add(translator.get_register('ecx') == 0)

# Lift loop summary in O(1) into Z3
translator.translate_loop_summary(summary, max_iterations=100000)

# Goal: When does EAX reach 800,000?
translator.solver.add(translator.get_register('eax') == 800000)

# Solve in milliseconds!
if translator.solver.check() == z3.sat:
    model = translator.solver.model()
    solved_N = model.eval(summary.loop_counter_var).as_long()
    print(f"[+] Solved N = {solved_N:,} iterations in O(1) time!")

📊 6. نتائج قياس الأداء على ثنائيات حقيقية

اختُبرت ضد ملفات تنفيذية معقدة لنظام Windows 64-بت (CrackMe Suite) تحتوي على حلقات متداخلة، وتقطيعًا فرعيًا للمسجلات، وأنماط خطوات مبهمة:

التحقق من الحقيقة المرجعية (Ground-Truth): تُتحقق جميع المفاتيح المستعادة عبر تنفيذ الثنائي المترجم الأصلي (.exe) بواسطة subprocess والتأكد من استجابة ACCESS GRANTED.

📚 7. مرجع واجهة برمجة التطبيقات

دوال الواجهة عالية المستوى:

• sl.analyze(code_bytes, iterations=1000, ...): فك تجميع وتقييم بسطر واحد.
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64): مفكك بايتات خام عبر Capstone.
• sl.compress(trace, min_iterations=3): ضاغط تتبعات هرمي.
• sl.evaluate(block_or_trace, k_passes=100): مقيّم الحالة المجردة والثوابت.

الفئات الأساسية:

• sl.Instruction: تمثيل موحّد لتعليمات التجميع.
• sl.LoopBlock: عقدة حلقة هرمية بحدود تكرار.
• sl.LoopSummary: ملخص تحويل مغلق الصيغة يحتوي على الدلتا والأنماط الدورية ومجموعات الثوابت.
• sl.LoopInvariantContract: واصف رسمي لثبات الخروج البنيوي ومولّد قواعد حدود SMT.
• sl.StridedInterval: تمثيل رياضي للفواصل مع محاذاة الخطوة والتطابق النمطي.
• sl.Z3Translator: رافع SMT رمزي يحوّل ملخصات الحلقات إلى قيود BitVector في Z3.

📄 الترخيص

ترخيص مزدوج: MIT / ملكي. طُوّر بكل ❤️ من أجل الهندسة العكسية عالية الأداء وتحليل الثنائيات.