2025-11-10T03:00:57.254697

Decompiling for Constant-Time Analysis

Arranz-Olmos, Barthe, Blatter et al.
Cryptographic libraries are a main target of timing side-channel attacks. A practical means to protect against these attacks is to adhere to the constant-time (CT) policy. However, it is hard to write constant-time code, and even constant-time code can be turned vulnerable by mainstream compilers. So how can we verify that binary code is constant-time? The obvious answer is to use binary-level CT tools. To do so, a common approach is to use decompilers or lifters as a front-end for CT analysis tools operating on source code or IR. Unfortunately, this approach is problematic with current decompilers. To illustrate this fact, we use the recent Clangover vulnerability and other constructed examples to show that five popular decompilers eliminate CT violations, rendering them not applicable with the approach. In this paper, we develop foundations to asses whether a decompiler is fit for the Decompile-then-Analyze approach. We propose CT transparency, which states that a transformation neither eliminates nor introduces CT violations, and a general method for proving that a program transformation is CT transparent. Then, we build CT-RetDec, a CT analysis tool based on a modified version of the LLVM-based decompiler RetDec. We evaluate CT-RetDec on a benchmark of real-world vulnerabilities in binaries, and show that the modifications had significant impact on CT-RetDec's performance. As a contribution of independent interest, we found that popular tools for binary-level CT analysis rely on decompiler-like transformations before analysis. We show that two such tools employ transformations that are not CT transparent, and, consequently, that they incorrectly accept non-CT programs. While our examples are very specific and do not invalidate the general approach of these tools, we advocate that tool developers counter such potential issues by proving the transparency of such transformations.
academic

فك التجميع لتحليل الوقت الثابت

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

  • معرّف الورقة: 2501.04183
  • العنوان: Decompiling for Constant-Time Analysis
  • المؤلفون: Santiago Arranz-Olmos (MPI-SP)، Gilles Barthe (MPI-SP & IMDEA)، Lionel Blatter (MPI-SP)، Youcef Bouzid (ENS Paris-Saclay)، Sören van der Wall (TU Braunschweig)، Zhiyuan Zhang (MPI-SP)
  • التصنيف: cs.PL (لغات البرمجة)
  • تاريخ النشر: يناير 2025 (نسخة arXiv المسبقة)
  • رابط الورقة: https://arxiv.org/abs/2501.04183

الملخص

تشكل مكتبات التشفير هدفاً رئيسياً لهجمات القنوات الجانبية المتعلقة بالتوقيت. تتمثل الطريقة العملية للدفاع ضد هذه الهجمات في اتباع استراتيجية الوقت الثابت (CT). ومع ذلك، فإن كتابة كود الوقت الثابت أمر صعب، وحتى الكود المصدري ذو الوقت الثابت قد يتم تحويله بواسطة مترجمات البرامج السائدة إلى كود ثنائي معرّض للثغرات. تبحث هذه الورقة عن كيفية التحقق من امتثال الكود الثنائي لمتطلبات الوقت الثابت. تتمثل إحدى الطرق الشائعة في استخدام أداة فك التجميع كواجهة أمامية لتحويل الكود الثنائي إلى كود مصدري أو تمثيل وسيط، ثم تطبيق أدوات تحليل CT الموجودة. للأسف، تعاني طريقة "فك التجميع-التحليل" من مشاكل. تثبت هذه الورقة من خلال أمثلة مثل ثغرة Clangover أن خمس أدوات فك تجميع شهيرة تقضي على انتهاكات CT، مما يجعل نتائج التحليل غير موثوقة.

السياق البحثي والدافع

خلفية المشكلة

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

المشكلة الأساسية

تعاني طريقة "فك التجميع-التحليل" الحالية من عيب جوهري: قد تقضي أدوات فك التجميع على انتهاكات CT أثناء عملية التحويل، مما يؤدي إلى أن تعتقد أدوات التحليل بشكل خاطئ أن الكود الثنائي المعرّض للثغرات آمن.

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

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

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

  1. اكتشاف وإثبات المشكلة: إثبات من خلال أمثلة مثل Clangover أن خمس أدوات فك تجميع سائدة تقضي على انتهاكات CT، مما يجعل نتائج التحليل غير موثوقة
  2. اقتراح نظرية الشفافية CT: تعريف رسمي لمفهوم شفافية CT، أي أن تحويل البرنامج لا يقضي على انتهاكات CT ولا يدخلها
  3. تطوير تقنيات الإثبات: اقتراح طريقة عامة قائمة على المحاكاة لإثبات شفافية CT لتحويلات البرامج
  4. بناء أداة عملية: تطوير أداة CT-RetDec بناءً على نسخة معدلة من أداة فك التجميع RetDec لإجراء تحليل CT ثنائي موثوق
  5. اكتشاف عيوب الأدوات: إثبات أن التحويلات المستخدمة داخلياً بواسطة أدوات تحليل CT الموجودة (CT-Verif و BinSec) غير شفافة أيضاً وتحتوي على ثغرات أمان

شرح الطريقة

تعريف المهمة

المدخل: برنامج ثنائي المخرج: نتيجة تحليل CT (آمن/غير آمن) القيود: يجب أن تعكس نتائج التحليل بدقة خصائص CT الفعلية للبرنامج الثنائي

الإطار النظري

تعريف شفافية CT

بالنسبة لتحويل البرنامج ⟦⋅⟧:Ls→Lt\llbracket \cdot \rrbracket : L_s \to L_t، يتم تعريف ثلاث خصائص:

  1. الانعكاسية (Reflection): إذا كان ⟦P⟧\llbracket P \rrbracket هو φ-CT، فإن P هو φ-CT
  2. الحفاظ (Preservation): إذا كان P هو φ-CT، فإن ⟦P⟧\llbracket P \rrbracket هو φ-CT
  3. الشفافية (Transparency): تحقيق الانعكاسية والحفاظ معاً

تقنيات المحاكاة

استخدام طريقتي المحاكاة المتزامنة والمحاكاة المرنة:

المحاكاة المتزامنة: كل خطوة في برنامج الإخراج تقابل خطوة واحدة في برنامج الإدخال

  • علاقة المحاكاة: s∼ts \sim t
  • محول الملاحظة: T:Os→OtT : O_s \to O_t
  • الشرط الأساسي: يجب أن يكون T حقنياً

المحاكاة المرنة: السماح ببرامج الإدخال والإخراج بتنفيذ عدد خطوات مختلف

  • دالة عدد الخطوات: ns:PC→N>0ns : PC \to \mathbb{N}_{>0}
  • دالة اللاحقة: sf:PC→Os∗sf : PC \to O_s^*
  • حقنية PC: محول الملاحظة حقني في كل نقطة برنامج

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

  1. مفهوم حقنية PC: توسيع تقنيات الحفاظ على CT الموجودة من خلال مطالبة محول الملاحظة بأن يكون حقنياً في كل نقطة برنامج لضمان الانعكاسية
  2. إطار موحد: توحيد تحويلات البرامج المتعددة تحت نفس الإطار النظري للتحليل
  3. التوجه العملي: توفير ليس فقط التحليل النظري بل أيضاً تطوير أدوات عملية قابلة للاستخدام

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

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

  1. اختبار أدوات فك التجميع: استخدام ثغرة Clangover والأمثلة الدنيا المبنية لاختبار 5 أدوات فك تجميع
  2. مجموعة الاختبارات المرجعية: 160 برنامجاً ثنائياً يحتوي على 10 أنواع من ثغرات القنوات الجانبية المعروفة
    • المترجمات: Clang 10/14/18/21
    • مستويات التحسين: -O0, -Os
    • المعمارية: x86-32, x86-64

مؤشرات التقييم

  • الدقة: ما إذا تم تحديد انتهاكات CT بشكل صحيح
  • الاكتمال: ما إذا تم تفويت أي ثغرات حقيقية
  • معدل الإنذارات الكاذبة: ما إذا تم وضع علامة على الكود الآمن كغير آمن

طرق المقارنة

  • RetDec الأصلي + CT-LLVM
  • CT-RetDec (النسخة المعدلة)
  • التحليل اليدوي كمعيار ذهبي

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

  • تعطيل 10 تمريرات تحسين غير شفافة في RetDec
  • الاحتفاظ بـ 52 تمريرة، 7 منها مثبتة نظرياً أنها شفافة
  • استخدام CT-LLVM لإجراء تحليل CT النهائي

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

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

اختبار شفافية أدوات فك التجميع

جميع أدوات فك التجميع الخمس المختبرة تقضي على بعض انتهاكات CT:

أداة فك التجميعClangoverBranch CoalescingEmpty BranchDead LoadDead Store
Angr✗✗-✗-
BinaryNinja-✗✗✗✗
Ghidra--✗✗-
Hex-Rays-✗✗✗-
RetDec✗✗✗✗✗

تقييم أداء CT-RetDec

على 160 برنامجاً مرجعياً:

  • معدل الدقة: 100% (بدون إنذارات كاذبة أو تفويتات)
  • RetDec الأصلي: يفوت معظم انتهاكات CT
  • تأثير التحسين: تحسين كبير في موثوقية تحليل CT

تحليل تحويلات البرامج

تحليل شفافية 10 تحويلات برامج شائعة:

التحويلات الشفافة (7 أنواع):

  • استبدال التعبيرات (طي الثوابت والتوسيع وغيرها)
  • حذف الفروع الميتة
  • حذف الإسناد الميت
  • تحسين مكافحة الفيضان
  • التحليل المنظم
  • دوران الحلقة

التحويلات غير الشفافة (3 أنواع):

  • دمج الفروع
  • تحويل If
  • حذف الوصول إلى الذاكرة

اكتشاف عيوب الأدوات

اكتشاف ثغرات أمان في أدوات CT-Verif و BinSec:

  • CT-Verif: محول SMACK يقضي على التحميل الميت، مما يؤدي إلى قبول برامج غير CT
  • BinSec: عملية رفع DBA تدمج الفروع الفارغة، مما يقضي على انتهاكات CT

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

تحليل القنوات الجانبية

تركز أدوات تحليل CT الموجودة بشكل أساسي على:

  • بناء البرنامج المنتج (CT-Verif)
  • أنظمة الأنواع (Jasmin)
  • محللات SMT (Vale)
  • التفسير المجرد (Blazy وآخرون)
  • التنفيذ الرمزي (BinSec)

الترجمة الآمنة

تركز الأبحاث ذات الصلة على كيفية حفاظ المترجمات على خصائص الأمان:

  • تقنيات محاكاة CT (Barthe وآخرون)
  • طريقة محول التسرب
  • إثباتات الحفاظ على CT لمترجمات Jasmin و CompCert

صحة فك التجميع

تركز الأعمال الموجودة بشكل أساسي على الصحة الوظيفية، مع إيلاء اهتمام أقل للحفاظ على خصائص الأمان.

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

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

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

القيود

  1. نطاق التغطية: يقتصر التحليل على استراتيجيات CT الأساسية، دون تناول فك التشفير والنماذج المتسربة المحسنة
  2. أنواع التحويلات: يغطي التحليل النظري فقط 10 تحويلات شائعة، بينما يحتوي RetDec على 62 تمريرة
  3. عيوب التنفيذ: حتى التحويلات الشفافة نظرياً قد تحتوي على أخطاء في التنفيذ

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

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

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

المميزات

  1. أهمية المشكلة: حل مشكلة حاسمة في التحليل الأمني العملي
  2. المساهمة النظرية: اقتراح إطار نظري شامل لشفافية CT
  3. الإثبات الكافي: التحقق من النظرية من خلال أمثلة متعددة واختبارات معيارية
  4. القيمة العملية: تطوير أدوات قابلة للاستخدام واكتشاف ثغرات في الأدوات الموجودة
  5. الصرامة الرسمية: توفير إثباتات ميكانيكية في Coq

أوجه القصور

  1. تغطية النظرية: تحليل فقط لأنواع جزئية من تحويلات البرامج
  2. حجم التجارب: بينما تحتوي الاختبارات المرجعية على ثغرات حقيقية، إلا أن الحجم نسبياً محدود
  3. اكتمال الأداة: لا تزال CT-RetDec تعتمد على طرق تجريبية لتعطيل بعض التمريرات

التأثير

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

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

  1. تحليل البرامج التشفيرية: مناسبة للسيناريوهات التي تتطلب تحليل CT على التطبيقات التشفيرية الثنائية
  2. تطوير المترجمات: توفير أساس نظري للتحقق من أمان تحسينات المترجم
  3. تطوير أدوات الأمان: توفير إرشادات لتطوير أدوات تحليل ثنائية موثوقة

المراجع

تستشهد الورقة بـ 61 مرجعاً ذا صلة، تغطي تحليل القنوات الجانبية وتقنيات الترجمة الآمنة وتقنيات فك التجميع وغيرها من المجالات المهمة، مما توفر أساساً نظرياً متيناً للبحث.