Formal Verification of Probing Security via Conditional Independence

تخيل أنك تحاول الحفاظ على وصفة سرية آمنة في مطبخ صاخب ومليء بالضجيج. في عالم التشفير، هذه "الوصفة السرية" هي المفتاح الخاص، و"الضجيج" هو هجوم القنوات الجانبية (Side-channel attack). المهاجمون لا يحاولون كسر الرياضيات؛ بل يحاولون التلصص على "التسريبات" (مثل استهلاك الطاقة أو التوقيت) أثناء قيام الكمبيوتر بمعالجة الأرقام لتخمين سرك.

ولإيقاف ذلك، يستخدم علماء التشفير تقنية تسمى التقنيع (Masking). فكر في التقنيع كأنه تمزيق وصفتك السرية إلى $t+1$ من قطع الورق (حصص). أنت تعطي قطعة واحدة لكل طباخ من الطباخين الـ $t+1$. وطالما أن المتلصص لا يمكنه رؤية سوى $t$ من القطع (أو أقل)، فلن يرى سوى هراء عشوائي. لا يمكنهم إعادة بناء الوصفة لأنهم يفتقدون قطعة واحدة حاسمة على الأقل.

ومع ذلك، فإن إثبات أن وصفة معقدة (خوارزمية) آمنة حقاً هو أمر صعب للغاية. إذا حاولت التحقق منها يدوياً، فقد تفوتك تسريب صغير، مما يؤدي إلى فشل نظام الأمان بأكمله. وهنا يأتي دور الورقة البحثية.

المشكلة: التحقق من "التسريب"

يريد المؤلفون بناء إثبات رسمي (ضمان رياضي) بأن الخوارزمية المقنعة آمنة. يتم القيام بذلك تقليدياً باستخدام مفهوم "المحاكي" (Simulator).

• فكرة المحاكي: تخيل صندوقاً سحرياً (المحاكي) يحاول إعادة إنشاء بالضبط ما يراه المتلصص. إذا استطاع الصندوق السحري إنشاء نفس "التسريب" تماماً باستخدام المعلومات العامة فقط (مثل قائمة المكونات) ودون رؤية قطع الوصفة السرية أبداً، فإن الخوارزمية الحقيقية تكون آمنة. المتلصص لا يتعلم شيئاً جديداً.

لكن بناء هذه المحاكيات يدوياً عرضة للخطأ. أراد المؤلفون طريقة أفضل لإثبات ذلك.

الحل: أداة منطقية جديدة (Lilac)

قدم المؤلفون اتصالاً بين "المحاكيات" ومفهومة الاستقلال الشرطي (Conditional Independence).

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

تثبت الورقة أنه إذا وجد محاكٍ، فإن السر يكون مستقلاً شرطياً عن التسريب، بشرط معرفة المعلومات العامة.

للتحقق من ذلك رياضياً، يستخدمون أداة تسمى Lilac.

• ما هي Lilac؟ فكر في Lilac ككتيب قواعد صارم وفائق القوة للاحتمالات. إنه يشبه لعبة منطقية حيث يتعين عليك إثبات أن مجموعتين من البطاقات (المتغيرات العشوائية) ممزوجتان بشكل مستقل عن بعضهما البعض.
• "الاقتران الفاصل" (Separating Conjunction): في كتيب القواعد هذا، يوجد رمز خاص (مثل عصا سحرية) يقول: "هاتان المجموعتان من البطاقات منفصلتان تماماً ولا تؤثر إحداهما على الأخرى".
• الابتكار: أضاف المؤلفون قواعد جديدة إلى كتيب القواعد هذا للتعامل مع "الاشتراط" (جزء "بشرط أن..."). وهذا يسمح لهم بإثبات أنه حتى لو رأى المتلصص بعض البيانات، فإنها لا تكشف عن السر لأنهم يمتلكون بالفعل البيانات العامة.

ما فعلوه بالفعل

لم يتحدث المؤلفون عن النظرية فحسب؛ بل بنوا نظاماً للتحقق من خوارزميات تشفير حقيقية باستخدام هذا المنطق الجديد. طبقوا طريقتهم على ثلاث "أدوات" (لبنات بناء) محددة تُستخدم في التشفير الحديث:

1. MINIADDREPNOISE: أداة تُستخدم لإضافة ضوضاء عشوائية إلى البيانات (مثل إضافة الملح إلى الحساء لإخفاء نكهته الأصلية). لقد أثبتوا أنه حتى لو تلصص المهاجم على بعض الحساء المملح، فلا يمكنه معرفة النكهة الأصلية.
2. REFRESH: أداة تأخذ القطع الممزقة من السر وتعيد خلطها بحيث تبدو جديدة تماماً، مما يمنع المهاجمين من تتبعها بمرور الوقت. لقد أثبتوا أن عملية إعادة الخلط هذه آمنة.
3. SECMULT (الضرب الآمن): أداة تضرب رقمين سريين معاً دون الكشف عن النتيجة حتى النهاية تماماً. هذا أحد أصعب العمليات التي يمكن تأمينها. لقد أثبتوا أن عملية الضرب هذه آمنة ضد هجمات "t-probing".

الخلا الخلاصة

تزعم الورقة أنه من خلال ترجمة الفكرة المعقدة لـ "المحاكيات" إلى لغة "الاستقلال الشرطي"، يمكنهم استخدام نظام المنطق Lilac للتحقق تلقائياً وبدقة من أن أدوات التشفير هذه آمنة.

لقد نجحوا في إثبات ذلك من خلال كتابة إثباتات رسمية لـ MINIADDREPNOISE و REFRESH و SECMULT، مما يظهر أن هذه الخوارزميات المحددة تستوفي متطلبات الأمان الصارمة اللازمة لحماية الأسرار ضد هجمات القنوات الجانبية. لم يدّعوا أنهم سيصلحون جميع مشاكل الأمان المستقبلية أو تطبيق ذلك على الأجهزة الطبية؛ عملهم يتعلق حصرياً بإثبات سلامة عمليات الرياضيات التشفيرية هذه باستخدام إطار منطقي جديد.