CoBRA

إعادة بناء حسابية قائمة على المعاملات — مُبسِّط تعبيرات الحساب المنطقي المختلط (Mixed Boolean-Arithmetic).

يقوم CoBRA بإزالة التعتيم (deobfuscation) عن التعبيرات التي تخلط بين العمليات الحسابية (+, -, *) والعمليات المنطقية على البتات (&, |, ^, ~) وعمليات الإزاحة (<<, >>) — وهي تقنية شائعة الاستخدام في تعتيم البرمجيات.

$ cobra-cli --mba "(x&y)+(x|y)"
x + y

$ cobra-cli --mba "((a^b)|(a^c)) + 65469 * ~((a&(b&c))) + 65470 * (a&(b&c))" --bitwidth 16
67 + (a | b | c)

$ cobra-cli --mba "((a^b)&c) | ((a&b)^c)"
c ^ a & b

$ cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16
x

$ cobra-cli --mba "(x ^ 0x10) + 2 * (x & 0x10)"
16 + x

$ cobra-cli --mba "x << 3"
8 * x

$ cobra-cli --mba "~x"
~x

$ cobra-cli --mba "(x^y)*(x&y) + 3*(x|y)"
(x ^ y) * (x & y) + 3 * (x | y)

$ cobra-cli --mba '-357*(x&~y)*(x&y)+102*(x&~y)*(x&~y)+374*(x&~y)*~(x^y)
  -306*(x&~y)*~(x|y)-17*(x&~y)*~(x|~y)-105*~(x|~y)*(x&y)+30*~(x|~y)*(x&~y)
  +110*~(x|~y)*~(x^y)-90*~(x|~y)*~(x|y)-5*~(x|~y)*~(x|~y)+34*(x&~y)*~x
  -85*(x&~y)*~y+10*~(x|~y)*~x-25*~(x|~y)*~y'
22 * (x & y) + -17 * x + -5 * y

كيف يعمل

يستخدم CoBRA منسّقًا قائمًا على قائمة عمل (worklist) لتبسيط التعبيرات. يدخل كل تعبير إلى قائمة العمل كعنصر عمل مُعلَّم بنوع حالة. يختار المجدول (scheduler) المرحلة التالية بناءً على حالة العنصر، والاعتماديات المسبقة، وذاكرة تخزين مؤقتة للمحاولات تمنع العمل المتكرر.

تُنظَّم 36 مرحلةً منفصلة في عائلات: معالجة شجرة التحليل (AST)، والتقنيات القائمة على التوقيع، والتقنيات شبه الخطية، والتفكيك، والرفع. بعض المراحل تُطلق بدائل محلية أو حلولًا فرعية تُحسم عبر مجموعات تنافسية (competition groups)؛ وخارج هذه المجموعات، تعيد قائمة العمل أول مرشح علوي مُتحققٍ منه بالكامل. تُتحقق جميع النتائج عبر فحص عشوائي للمدخلات (الافتراضي) أو عبر إثبات تكافؤ باستخدام Z3 (--verify).

Input Expression
       |
  [Worklist Scheduler]
       |
  Work items flow through state kinds:
       |
  kFoldedAst ──> AST processing passes
       |         (classify, lower, rewrite)
       |
       +──> kSignatureState ──> Signature techniques
       |    (pattern match, CoB, ANF, polynomial recovery)
       |
       +──> kSemilinearNormalizedIr ──> Semilinear techniques
       |    (normalize, recover structure, refine, reconstruct)
       |
       +──> kCoreCandidate / kRemainderState ──> Decomposition
       |    (extract core, classify residual, solve)
       |
       +──> kLiftedSkeleton ──> Lifting
       |    (virtual variable substitution, outer solve)
       |
       +──> kCandidateExpr ──> Verification
            (spot-check or Z3 proof)
       |
  Simplified Expression

التقنيات القائمة على التوقيع تقيّم التعبير على جميع المدخلات المنطقية للحصول على متجه توقيع. يحوّل فراشي CoB (butterfly) لاستعادة معاملات أساس جداء AND. وتتعامل مطابقة الأنماط، وANF، واستعادة الحدوديات مع مستويات تعقيد مختلفة.

التقنيات شبه الخطية تتعامل مع التعبيرات ذات الأقنعة الثابتة (مثل x & 0xFF). يُفكَّك التعبير إلى ذرّات bitwise موزونة، ثم يعمل استرداد البنية وتحسين الحدود على تبسيط التمثيل الوسيط، وتُعيد تجميع OR المقسمة حسب البتات بناء النتيجة النهائية.

التفكيك يستهدف التعبيرات المختلطة التي تحتوي على جداءات من تعبيرات فرعية bitwise. يُستخرج نواة حدودية، ثم تُصنَّف البقايا وتُحل (حدودية، أو منطقية-صفرية/شبحية، أو قالب احتياطي).

الرفع (Lifting) يستبدل التعبيرات الفرعية المعقدة بمتغيرات افتراضية، ويحل الهيكل الخارجي المبسّط، ثم يعيد التعويض.

الميزات

• تبسيط MBA الخطي — مجاميع موزونة من ذرّات bitwise عبر متجه التوقيع وتحويل CoB
• مطابقة الأنماط المقيّسة — k * f(vars) + c مع تفكيك شانون للتعبيرات المنطقية ذات 4-5 متغيرات
• دعم شبه خطي — ذرّات ذات أقنعة ثابتة مع خفض الثوابت عبر XOR/OR/NOT-AND، واسترداد البنية، وتحسين الحدود، وإعادة البناء المقسمة حسب البتات
• استرداد الحدوديات — حدود متعددة الخطية وقوى مفردة عبر تقسيم المعاملات والفرق المحدود
• معالجة الجداءات المختلطة — محرك تفكيك مع استخراج النواة وحل البقايا وتصنيف البقايا الشبحية
• رفع التعبيرات الفرعية — استبدال الأشجار الفرعية المعقدة بمتغيرات افتراضية لتقليل أبعاد المسألة
• منسّق قائمة العمل — جدولة مراحل تدرك الرسوم البيانية الحلقية الموجهة (DAG) مع إزالة التكرار وبحث محدود
• مجموعات تنافسية — الفروع البديلة المحلية والحلول الفرعية تستخدم اختيار الفائز بناءً على التكلفة مع استمراريات
• إزاحات ثابتة — << يُحوَّل إلى ضرب، و>> يُبسَّط عبر التقنيات شبه الخطية
• تنظيف ANF — الامتصاص، واستخراج العوامل المكعبة المشتركة، والتعرف على OR
• عرض بت قابل للتكوين — حساب معياري من 1 إلى 64 بت
• حذف المتغيرات المساعدة — يقلل عدد المتغيرات عندما تختصر الحدود
• تحقق Z3 — فحص تكافؤ اختياري للمخرجات المبسّطة
• اختبار ذاتي بالفحص العشوائي — تحقق خفيف بمدخلات عشوائية عندما يكون Z3 غير متاح
• إضافة LLVM pass — تكامل مباشر مع خطوط أنابيب المترجم (يتطلب LLVM 19-22)

البناء

راجع BUILD.md للحصول على التفاصيل الكاملة بما في ذلك الاعتماديات الاختيارية (LLVM، Z3).

# Build dependencies (Abseil, Highway; optionally GoogleTest, LLVM, Z3)
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release
cmake --build build-deps

# Build CoBRA
cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCMAKE_BUILD_TYPE=Release
cmake --build build

# (Optional) Build and run tests
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release -DCOBRA_BUILD_TESTS=ON
cmake --build build-deps
cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCMAKE_BUILD_TYPE=Release \
  -DCOBRA_BUILD_TESTS=ON
cmake --build build
ctest --test-dir build --output-on-failure

مع إضافة LLVM Pass

cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCOBRA_BUILD_LLVM_PASS=ON \
  -DCMAKE_BUILD_TYPE=Release
cmake --build build

الاستخدام

# Basic simplification
cobra-cli --mba "(x&y)+(x|y)"

# Specify bitwidth
cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16

# Enable Z3 equivalence verification
cobra-cli --mba "(a^b)+(a&b)+(a&b)" --verify

# Verbose output (show intermediate pipeline steps)
cobra-cli --mba "(x&y)+(x|y)" --verbose

الخيارات

بنية المشروع