2025-11-25T11:37:18.016926

Augmenting Smart Contract Decompiler Output through Fine-grained Dependency Analysis and LLM-facilitated Semantic Recovery

Liao, Nan, Gao et al.
Decompiler is a specialized type of reverse engineering tool extensively employed in program analysis tasks, particularly in program comprehension and vulnerability detection. However, current Solidity smart contract decompilers face significant limitations in reconstructing the original source code. In particular, the bottleneck of SOTA decompilers lies in inaccurate method identification, incorrect variable type recovery, and missing contract attributes. These deficiencies hinder downstream tasks and understanding of the program logic. To address these challenges, we propose SmartHalo, a new framework that enhances decompiler output by combining static analysis (SA) and large language models (LLM). SmartHalo leverages the complementary strengths of SA's accuracy in control and data flow analysis and LLM's capability in semantic prediction. More specifically, \system{} constructs a new data structure - Dependency Graph (DG), to extract semantic dependencies via static analysis. Then, it takes DG to create prompts for LLM optimization. Finally, the correctness of LLM outputs is validated through symbolic execution and formal verification. Evaluation on a dataset consisting of 465 randomly selected smart contract methods shows that SmartHalo significantly improves the quality of the decompiled code, compared to SOTA decompilers (e.g., Gigahorse). Notably, integrating GPT-4o with SmartHalo further enhances its performance, achieving precision rates of 87.39% for method boundaries, 90.39% for variable types, and 80.65% for contract attributes.
academic

تحسين مخرجات معكوس الهندسة للعقود الذكية من خلال تحليل الاعتماديات الدقيقة واستعادة الدلالات بمساعدة نماذج اللغة الكبيرة

المعلومات الأساسية

  • معرّف الورقة: 2501.08670
  • العنوان: تحسين مخرجات معكوس الهندسة للعقود الذكية من خلال تحليل الاعتماديات الدقيقة واستعادة الدلالات بمساعدة نماذج اللغة الكبيرة
  • المؤلفون: Zeqin Liao, Yuhong Nan, Zixu Gao, Henglong Liang, Sicheng Hao, Peifan Ren, Zibin Zheng
  • التصنيف: cs.SE (هندسة البرمجيات)
  • تاريخ النشر: يناير 2025 (نسخة أولية على arXiv)
  • رابط الورقة: https://arxiv.org/abs/2501.08670

الملخص

معكوسات الهندسة للعقود الذكية هي أدوات هندسة عكسية مستخدمة على نطاق واسع في تحليل البرامج، خاصة في فهم البرامج والكشف عن الثغرات. ومع ذلك، فإن معكوسات الهندسة الحالية لعقود Solidity الذكية تواجه قيودًا كبيرة في إعادة بناء الكود المصدري الأصلي، والتي تتجلى بشكل أساسي في ثلاثة جوانب: عدم دقة تحديد الدوال، وأخطاء استعادة أنواع المتغيرات، وغياب خصائص العقد. لمعالجة هذه التحديات، تقترح هذه الورقة إطار عمل SmartHalo، الذي يجمع بين التحليل الثابت (SA) ونماذج اللغة الكبيرة (LLM) لتحسين مخرجات معكوس الهندسة. يستفيد SmartHalo من دقة التحليل الثابت في تحليل تدفق التحكم والبيانات وقدرة نماذج اللغة الكبيرة على التنبؤ الدلالي. بشكل محدد، يقوم الإطار ببناء بنية بيانات رسم بياني الاعتماديات (DG) لاستخراج علاقات الاعتماديات الدلالية، ثم ينشئ تعليمات محسّنة لنموذج اللغة الكبيرة بناءً على DG، وأخيرًا يتحقق من صحة مخرجات نموذج اللغة الكبيرة من خلال التنفيذ الرمزي والتحقق الرسمي.

خلفية البحث والدافع

تعريف المشكلة

تواجه معكوسات الهندسة للعقود الذكية ثلاث مشاكل أساسية:

  1. عدم دقة تحديد حدود الدوال: لا تستطيع معكوسات الهندسة الحالية تحديد حدود الدوال بدقة، وغالبًا ما تستعيد عدة دوال بشكل خاطئ كدالة واحدة، أو تحذف دوال مهمة
  2. أخطاء استعادة أنواع المتغيرات: الأنواع المُنتجة من قبل معكوس الهندسة غير متسقة مع القواعد الثابتة للمجال، مثل استعادة قيمة الإرجاع bytes32 لدالة keccak256 بشكل خاطئ كنوع uint256
  3. غياب خصائص العقد: متغيرات الحالة في العقود الذكية تسجل خصائص العقد الحرجة (مثل الأصول والهويات والموجهات)، لكنها غائبة تمامًا في الكود المعكوس

تحليل الأهمية

تعيق هذه العيوب بشكل خطير المهام اللاحقة:

  • التأثير على دقة الكشف عن الثغرات، مما يؤدي إلى إيجابيات وسلبيات خاطئة
  • تقليل كفاءة فهم البرامج
  • تحديد مهام التحليل المتقدمة مثل تحليل تدفق الاستدعاءات بين العقود

قيود الطرق الموجودة

  • SmartDagger: يمكنه فقط استعادة خصائص العقد جزئيًا للمتغيرات الحالية، بناءً على نماذج التعلم العميق، مع انخفاض الأداء على العقود الناشئة
  • Neural-FEBI: لا يدعم استعادة حدود الدوال ذات المعدّلات أو الدوال الموروثة
  • SigRec/VarLifter/DeepInfer: يمكنه فقط استعادة أنواع المعاملات جزئيًا للدوال المعروفة، ويعتمد على قواعد اكتشافية محددة مسبقًا، مع تغطية منخفضة

الدافع البحثي

بناءً على رؤيتين أساسيتين:

  1. الأنماط الطبيعية للبرمجيات: يميل المبرمجون إلى استخدام هياكل كود متشابهة وخصائص عقود ومتغيرات وحدود دوال متشابهة في سياقات متشابهة
  2. التعزيز التعاوني بين التحليل الثابت ونماذج اللغة الكبيرة: التحليل الثابت يتمتع بدقة عالية في التعامل مع القيود الثابتة المعقدة، بينما نماذج اللغة الكبيرة تتمتع بمرونة في التنبؤ بالأهداف التي تفتقر إلى القيود الثابتة

المساهمات الأساسية

  1. تحديد وتحليل منهجي للقيود الرئيسية في مخرجات معكوسات الهندسة الحالية للعقود الذكية
  2. اقتراح إطار عمل SmartHalo، الذي يجمع بشكل مبتكر بين التحليل الثابت ونماذج اللغة الكبيرة لتحسين مخرجات معكوس الهندسة
  3. تصميم بنية بيانات رسم بياني الاعتماديات (DG)، لاستخراج ثلاثة أنواع من علاقات الاعتماديات الدلالية (الاعتماديات الحالية، اعتماديات تدفق التحكم، اعتماديات النوع)
  4. إنشاء آلية تحقق صارمة من الصحة، من خلال التنفيذ الرمزي والتحقق الرسمي للتعامل مع مشكلة الهلوسة في نماذج اللغة الكبيرة
  5. تقييم شامل والتحقق من فعالية SmartHalo في استعادة حدود الدوال وأنواع المتغيرات وخصائص العقد

شرح الطريقة

تعريف المهمة

الإدخال: الكود الزائف الذي ينتجه معكوس الهندسة الإخراج: كود معكوس محسّن يتضمن حدود دوال دقيقة وأنواع متغيرات وخصائص عقد القيود: الحفاظ على تكافؤ سلوك البرنامج، الامتثال لقواعس النوع الثابتة في Solidity

معمارية النموذج

يعتمد SmartHalo على معمارية ثلاثية المراحل:

1. استخراج الدلالات القائم على الاعتماديات

  • تحليل تدفق التحكم: استخدام Tree-sitter لبناء شجرة بناء الجملة، التحويل إلى تمثيل وسيط بثلاثة عناوين، وإنشاء رسوم بيانية لتدفق التحكم والبيانات
  • تحديد الاعتماديات:
    • اعتماديات النوع: العلاقات بين نوع المتغير والمتغيرات أو التعبيرات الأخرى
    • الاعتماديات الحالية: علاقات القراءة والكتابة بين متغيرات الحالة
    • اعتماديات تدفق التحكم: علاقات مسارات التنفيذ للبرنامج
  • بناء رسم بياني الاعتماديات: DG = (Nc, Ec, Xe)، حيث Nc مجموعة العقد (المتغيرات والتعبيرات)، Ec مجموعة الحواف (ثلاثة أنواع من الاعتماديات)، Xe دالة التسمية

2. التحسين الدلالي المدفوع بنموذج اللغة الكبيرة

  • توليد سياق الكود:
    • المتغيرات: إجراء تقطيع الكود بناءً على DG، استخراج مقاطع الكود المتعلقة بالمتغير المستهدف
    • الدوال: البحث عن سلسلة الاستدعاء التي تحتوي على الدالة المستهدفة
  • توليد مرشحي الاستدلال:
    • مرشحو أنواع المتغيرات: جمع الأنواع المدمجة من وثائق Solidity
    • مرشحو خصائص العقد: Limit, Fee, Flag, Address, Asset, Router, Others
  • تعليمات سلسلة الفكر (COT): تحويل علاقات الاعتماديات في DG إلى وصفات خطوات الاستدلال

3. التحقق من الصحة

  • فحص تكافؤ سلوك البرنامج:
    • إجراء التنفيذ الرمزي للدوال الأصلية والمحسّنة
    • استخدام محلل Z3 للتحقق الرسمي
    • تأكيد التكافؤ: Φ = ¬(s ⇔ s′)
  • فحص انتهاك القواعد الثابتة: الكشف عن أخطاء استدلال النوع بناءً على قواعد نوع Solidity

نقاط الابتكار التقني

  1. تحليل الاعتماديات الدقيقة: أول استخراج منهجي واستخدام لثلاثة أنواع من علاقات الاعتماديات الدلالية
  2. إطار عمل التعاون بين التحليل الثابت ونموذج اللغة الكبيرة: يجمع بشكل مبتكر بين دقة التحليل الثابت وقدرة فهم اللغة لنموذج اللغة الكبيرة
  3. آلية ضمان الصحة الصارمة: ضمان صحة نتائج التحسين من خلال التنفيذ الرمزي والتحقق الرسمي
  4. تصميم عام: يدعم تكامل نماذج لغة كبيرة وأدوات معكوسة هندسة مختلفة

إعداد التجارب

مجموعات البيانات

  • مجموعة البيانات للتقييم: تم اختيار 500 دالة عشوائيًا من أكبر مجموعة بيانات مفتوحة المصدر للعقود الذكية، مع الحصول في النهاية على 456 زوجًا من الكود المصدري والمخرجات المعكوسة
  • مجموعة بيانات العقود المعقدة: تم اختيار 50 عقدًا ذكيًا عشوائيًا من 682 تطبيق DApp حقيقي (حوالي 900 دالة)
  • مجموعة بيانات الكشف عن الثغرات: تتضمن 81 ثغرة إعادة دخول مصنفة، 18 زوجًا من العقود الهجومية، 50 عقدًا بثغرات تجاوز عدد صحيح

مقاييس التقييم

  • مطابقة حدود الدوال: تطابق كامل لنقاط البداية والنهاية مع دوال المستوى المصدري
  • مطابقة النوع: تطابق كامل بين النوع المتنبأ به والنوع الفعلي (بما في ذلك تخطيط البيانات ومعلومات الحقول)
  • مطابقة خصائص العقد: تطابق كامل بين الخصائص المتنبأ بها والخصائص الفعلية
  • معدل فشل إعادة التجميع: معدل أخطاء التجميع في الكود المحسّن

طرق المقارنة

  • SmartDagger: للمقارنة مع استعادة خصائص العقد
  • VarLifter: للمقارنة مع استدلال نوع المتغير
  • معكوس الهندسة الأصلي: Gigahorse/Dedaub كخط أساس

تفاصيل التنفيذ

  • بيئة التطوير: Python 3.8.10، 1799 سطر كود
  • اختيار نموذج اللغة الكبيرة: استخدام GPT-3.5 بشكل أساسي، مع دعم GPT-4o mini و Llama-3 و Deepseek-v3 و Qwen-2.5-coder
  • تكوين الأجهزة: معالج Intel i9-10980XE، GPU RTX 3090، ذاكرة RAM 250GB

نتائج التجارب

النتائج الرئيسية

مقارنة التأثير الإجمالي (مع معكوس الهندسة الأصلي)

المقياستحسن الدقةتحسن الاستدعاء
تحديد حدود الدوال+20.30%+30.03%
استدلال نوع المتغير+30.02%+42.04%
استعادة خصائص العقد68.06%90.93%

المقارنة مع طرق الحالة الفنية الأفضل

  • مقابل SmartDagger (خصائص العقد): تحسن الدقة 44.69%، تحسن الاستدعاء 80.86%
  • مقابل VarLifter (نوع المتغير): تحسن الدقة 13.51%، تحسن الاستدعاء 77.08%

مقارنة الأداء عبر نماذج اللغة الكبيرة المختلفة

نموذج اللغة الكبيرةحدود الدوال (D/R)نوع المتغير (D/R)خصائص العقد (D/R)
GPT-3.588.26%/80.51%92.27%/84.26%68.06%/90.93%
GPT-4o mini91.32%/87.38%90.40%/88.82%80.66%/91.78%
Llama-366.09%/55.11%62.41%/48.53%61.68%/60.34%

تجارب الاستئصال

مقارنة استخدام التحليل الثابت ونموذج اللغة الكبيرة بشكل منفصل وإطار عمل SmartHalo الكامل:

  • مساهمة التحليل الثابت: توفير استخراج اعتماديات دقيق والتحقق من القيود
  • مساهمة نموذج اللغة الكبيرة: توفير فهم دلالي وقدرة التعرف على الأنماط النادرة
  • التأثير التعاوني: SmartHalo يتفوق على استخدام نموذج اللغة الكبيرة بمفرده بنسبة 19.23%/29.23% في حدود الدوال

التحقق من القدرة على التعميم

  • عبر معكوسات الهندسة: تحسن كبير على Heimdall و Panoramix
  • العقود المعقدة: الحفاظ على أداء جيدة على تطبيقات DApp الحقيقية المعقدة
  • تحليل الكفاءة: متوسط وقت المعالجة 23.99 ثانية، التكلفة $0.00136/دالة

تأثير المهام اللاحقة

  • الكشف عن ثغرات إعادة الدخول: تحسن الدقة من 72.16% إلى 80.41%
  • تحديد الهجمات: تحسن الاستدعاء من 83.33% إلى 100.00%
  • الكشف عن تجاوز الأعداد الصحيحة: تحسن الدقة 21.96%، تحسن الاستدعاء 38.00%

الأعمال ذات الصلة

معكوسات الهندسة للعقود الذكية

  • Gigahorse/Elipmoc: تحويل بايتكود EVM إلى تمثيل كود بثلاثة عناوين
  • Erays/EtherSolve: استعادة رسم بياني تدفق التحكم من بايتكود EVM
  • SigRec/DeepInfer: استعادة توقيعات الدوال العامة

تحسين معكوسات الهندسة

  • استعادة المعلومات الدلالية: DEBIN و OSPREY و BDA وغيرها تستعيد اعتماديات البرنامج من خلال التحليل الثابت
  • تحسين أسماء المتغيرات والأنواع: DIRE و DIRTY و DeGPT وغيرها تستخدم التعلم العميق لتحسين مخرجات معكوس الهندسة

مزايا هذه الورقة

مقارنة بالأعمال الموجودة، يتمتع SmartHalo بـ:

  1. أهداف تحسين أكثر شمولاً: معالجة حدود الدوال وأنواع المتغيرات وخصائص العقد في نفس الوقت
  2. قدرة تعميم أقوى: لا يعتمد على بيانات تدريب محددة، ويتكيف مع العقود الناشئة
  3. ضمان صحة صارم: ضمان صحة نتائج التحسين من خلال التحقق الرسمي

الخلاصة والمناقشة

الاستنتاجات الرئيسية

  1. SmartHalo يحسن بشكل كبير جودة معكوسات الهندسة للعقود الذكية، مع تحقيق تحسينات جوهرية في ثلاثة مقاييس رئيسية
  2. إطار عمل التعاون بين التحليل الثابت ونموذج اللغة الكبيرة ثبت فعاليته، مع الاستفادة الكاملة من المزايا التكاملية للطرفين
  3. آلية التحقق الصارمة من الصحة نجحت في السيطرة على مشكلة الهلوسة في نموذج اللغة الكبيرة
  4. الإطار يتمتع بقدرة تعميم جيدة، مع دعم نماذج لغة كبيرة وأدوات معكوسة هندسة متعددة

القيود

  1. استعادة هياكل الوراثة: لا يمكن استعادة علاقات الوراثة داخل العقد، لأن مستوى البايتكود يفتقد معلومات الفئة
  2. حجم مجموعة البيانات: مجموعة البيانات للتقييم نسبيًا صغيرة (456 دالة)، لكنها مقارنة بحجم الأبحاث الحالية الأفضل
  3. تطور واجهات برمجة تطبيقات نموذج اللغة الكبيرة: قد يؤثر على إمكانية تكرار النتائج
  4. معالجة الحالات المعقدة: الأداء محدودة في حالات الاستدعاءات منخفضة المستوى والتجميع المضمن والاعتماديات خارج السلسلة

الاتجاهات المستقبلية

  1. استعادة هياكل الوراثة: استكشاف استدلال علاقات الوراثة بناءً على مطابقة الأنماط
  2. تقييم على نطاق أوسع: التحقق من قوة الطريقة على مجموعات بيانات أكبر
  3. تدريب نماذج متخصصة: تدريب نماذج متخصصة لفهم العقود الذكية
  4. التحسين في الوقت الفعلي: دعم تحسين معكوس الهندسة عبر الإنترنت

التقييم المتعمق

المزايا

  1. تعريف المشكلة واضح: تحديد منهجي وتحليل للمشاكل الأساسية في معكوسات الهندسة للعقود الذكية
  2. قوة الابتكار في الطريقة: أول اقتراح لإطار عمل التعاون بين التحليل الثابت ونموذج اللغة الكبيرة، مع تصميم ذكي لبنية بيانات رسم بياني الاعتماديات
  3. حل تقني كامل: من استخراج الدلالات والتحسين المحسّن إلى التحقق من الصحة يشكل حلقة مغلقة كاملة
  4. تقييم تجريبي شامل: تجارب مقارنة متعددة الأبعاد، بما في ذلك دراسات الاستئصال والتحقق من المهام اللاحقة
  5. قيمة عملية عالية: 60.22% من الكود المحسّن يمكن إعادة تجميعه مباشرة، مما يحسن الفائدة العملية بشكل كبير

أوجه القصور

  1. تحليل نظري غير كافٍ: نقص التحليل المتعمق للضمانات النظرية للطريقة
  2. تحليل الأخطاء محدود: يمكن أن يكون تحليل السبب الجذري لحالات فشل التحسين أعمق
  3. التكلفة الحسابية: قد يؤدي التنفيذ الرمزي والتحقق الرسمي إلى تكاليف حسابية عالية
  4. الاعتماد على الأدوات الخارجية: يعتمد على جودة معكوسات الهندسة الموجودة وواجهات برمجة تطبيقات نموذج اللغة الكبيرة

التأثير

  1. المساهمة الأكاديمية: توفير نموذج بحثي جديد لمجال تحليل العقود الذكية
  2. القيمة العملية: يمكن تطبيقها مباشرة على تدقيق أمان العقود الذكية وفهم البرامج
  3. قابلية التوسع: يدعم تصميم الإطار تكامل أدوات تحليل ونماذج مختلفة
  4. المساهمة مفتوحة المصدر: التزام المؤلفين بفتح الكود ومجموعات البيانات، مما يسهل تكرار البحث

السيناريوهات المعمول بها

  1. تدقيق أمان العقود الذكية: تحسين قابلية قراءة ودقة الكود المعكوس
  2. أدوات الكشف عن الثغرات: كخطوة معالجة مسبقة لتحسين دقة الكشف
  3. أدوات فهم البرامج: مساعدة المطورين على فهم منطق العقود الخارجية
  4. البحث الأكاديمي: توفير بيانات عالية الجودة لأبحاث تحليل العقود الذكية

المراجع

تستشهد الورقة بـ 96 مرجعًا ذا صلة، تتضمن بشكل أساسي:

  • تحليل العقود الذكية: أعمال كلاسيكية مثل Gigahorse و SmartDagger و VarLifter
  • نظرية تحليل البرامج: أدبيات التنفيذ الرمزي والتحقق الرسمي
  • تطبيقات التعلم الآلي: تطبيق التعلم العميق في تحليل البرامج
  • تقنيات معكوسات الهندسة: طرق وأدوات تحسين معكوسات الهندسة التقليدية

التقييم الإجمالي: هذه ورقة بحثية عالية الجودة في هندسة البرمجيات، تقترح حلاً مبتكرًا لمشكلة مهمة في معكوسات الهندسة للعقود الذكية. التصميم المنهجي معقول، والتقييم التجريبي شامل، والقيمة العملية بارزة. على الرغم من وجود بعض القيود، فإن المساهمة الإجمالية كبيرة وذات تأثير مهم على مجال تحليل أمان العقود الذكية.