💻 computer science

A Deductive System for Contract Satisfaction Proofs

تقدم هذه الورقة نظام إثبات استنتاجي سليم وكامل يعتمد على التماثل النسبي والاستدلال التعاوني لتمكين التحقق التفاعلي والنمطي من استيفاء عقود الأجهزة والبرمجيات، كما تم توضيحه من خلال صياغته الرسمية في مساعد الإثبات Rocq وتطبيقه على براهين أمنية معقدة.

المؤلفون الأصليون: Arthur Correnson, Haoyi Zeng, Jana Hofmann

نُشر 2026-04-13

📖 5 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلفون الأصليون: Arthur Correnson, Haoyi Zeng, Jana Hofmann

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

الصورة الكبيرة: مشكلة "الصندوق الأسود"

تخيل أنك مطور برمجيات تكتب وصفة سرية (برنامج) لطاهٍ مشهور جداً (عتاد الحاسوب/Hardware). تريد التأكد من أنه مهما كان الشخص الذي يتناول الطعام، لا يمكنه معرفة مكوناتك السرية بمجرد مراقبة حركات الطاهي.

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

ولإيقاف ذلك، ابتكر المهندسون ما يسمى "عقود العتاد والبرمجيات" (Hardware-Software Contracts). فكر في هذه العقود كأنها "كتيب قواعد مبسط" للطاهي.

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

المشكلة: كيف نثبت أن الطاهي الحقيقي الفوضوي يتبع بالفعل كتيب القواعد المبسط؟ إذا قال العقد "لا توجد فتات"، ولكن الطاهي الحقيقي أسقط فتاتاً، فإن النظام الأمني بأكمله يفشل.

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

كان إثبات ذلك سابقاً يشبه محاولة إثبات أن خدعة سحرية تعمل عبر مشاهدتها مليون مرة (الاختبار/Testing) أو محاولة محاكاة كل حركة في جدول بيانات (التحقق من النموذج/Model checking).

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

الطريقة الجديدة: "المحقق التفاعلي" (هذه الورقة البحثية)

بنى مؤلفو هذه الورقة أداة جديدة تسمى "النظام الاستنتاجي" (Deductive System). تخيل هذا كأنه لعبة محقق ذكي وتفاعلي تُلعب داخل برنامج كمبيوتر (يسمى مساعد الإثبات/Proof Assistant).

بدلاً من تخمين الإجابة، تعمل أنت والكمبيوتر معاً لبناء حجة منطقية، خطوة بخطوة، تضمن أن الإثبات صحيح تماماً.

الفكرة الجوهرية: "تساوي الأثر النسبي" (Relative Trace Equality)

لفهم طريقتهم، تخيل عداءين على مضمار سباق:

العداء (أ) (العقد): يركض على مضمار ناعم ومثالي.
العداء (ب) (العتاد): يركض على مضمار حقيقي وعر.

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

تقدم الورقة تقنية تسمى "التماثل النسبي" (Relative Bisimulation).

التشبيه: تخيل أنك حكم يراقب أربعة عداءين في وقت واحد:
- عدّاءان على مضمار العقد (العداء A1 والعداء A2).
- عدّاءان على مضمار العتاد (العداء B1 والعداء B2).
- السيناريو: تبدأ العداءين A1 وA2 بمكونات سرية مختلفة قليلاً. وتبدأ العداءين B1 وB2 بنفس المكونات السرية.
- القاعدة: إذا انتهى العداءان A1 وA2 بالظهور بشكل متطابق (نفس الخطوات)، فيجب أن ينتهي العداءان B1 وB2 أيضاً بالظهور بشكل متطابق.

"التماثل النسبي" هو وسيلة للتحقق من هؤلاء العداء الأربعة في وقت واحد لضمان بقائهم في حالة تزامن، حتى لو كانوا يركضون بسرعات مختلفة.

الخدعة السحرية: تقنيات "الاستقراء المشترك" (Coinduction) و"الارتقاء إلى" (Up-To)

الجزء الأصعب في هذا الإثبات هو أن العداءين قد يخرجان عن التزامن.

المشكلة: قد يأخذ عداء العقد "اختصاراً" (خطوة تحدث فورياً)، بينما يتعين على عداء العتاد المرور عبر حقل طيني (أخذ خطوات كثيرة للقيام بنفس الشيء).
الطريقة القديمة: كان عليك إجبارهم على التحرك في نفس الوقت تماماً (خطوة بخطوة)، وهو أمر مستحيل إذا كان أحدهم سريعاً والآخر بطيئاً.
الطريقة الجديدة (الاستقراء المشترك/Coinduction): يستخدم المؤلفون تقنية الاستقراء المشترك. فكر في هذا كأنه "فرضية السفر عبر الزمن".
- بدلاً من التحقق من كل خطوة من البداية إلى النهاية، تقول: "أفترض أنه إذا وصلنا إلى حالة مستقبلية حيث لا يزال العداءان في حالة تزامن، فنحن في أمان."
- تقوم ببناء "شبكة أمان" (Invariant) تلتقط العداءين إذا ابتعدا عن بعضهما.
- تقنيات "الارتقاء إلى" (Up-To Techniques): هذه مثل امتلاك "كود غش" يسمح لك بتجاوز الأجزاء المملة من الإثبات. إذا كنت تعلم أن اثنين من العداءين متماثلان جوهرياً (التماটি/Symmetry) أو أن أحد المسارات يؤدي إلى مسار آخر (التعدي/Transitivity)، يمكنك القفز للأمام دون إعادة إثبات الأساسيات.

دراستا الحالة: إثبات خدعة "التنبؤ الخاطئ الدائم"

اختبرت الورقة نظامها على مشكلتين أمنيتين من الواقع:

عقد "التنبؤ الخاطئ الدائم" (Always-Mispredict):
- السيناريو: تحاول وحدات المعالجة المركزية الحديثة تخمين أي اتجاه سيفتح الباب (تنبؤ الفرع/Branch Prediction) لتوفير الوقت. إذا أخطأت في التخمين، يجب عليها "التراجع" عن العمل، لكنها أحياناً تترك "فتاتاً" (تسريباً) خلفها.
- العقد: يقول كتيب القواعد: "دعونا نتظاهر بأن المعالج دائماً يخمن بشكل خاطئ ويجرب كلا البابين". هذا يخلق نمطاً يمكن التنبؤ به من الفتات.
- الإثبات: استخدم المؤلفون نظامهم لإثبات أنه حتى لو خمن المعالج الحقيقي بشكل صحيح أحياناً، فإنه لن يسرب معلومات أكثر مما يسربه عقد "التنبؤ الخاطئ دائماً". إنه يشبه إثبات أن السائق الحذر (العقد) دائماً أكثر أماناً من السائق المتهور (العتاد)، حتى لو حالف السائق المتهور الحظ أحياناً.
عقد "التسلسل" (Sequential):
- السيناريو: تقوم وحدات المعالجة المركزية الحقيقية بأداء الأشياء خارج الترتيب لتكون سريعة (مثل طاهٍ يقطع الخضروات بينما يغلي الماء).
- العقد: يقول كتيب القواعد: "دعونا نتظاهر بأن المعالج يقوم بكل شيء بترتيب صارم، واحداً تلو الآخر".
- الإثبات: أثبتوا أنه على الرغم من أن المعالج الحقيقي فوضوي وسريع، إلا أنه لا يسرب أسراراً لا يسربها الإصدار البطيء والمنضبط.

لماذا هذا مهم؟

الثقة: في السابق، كان علينا الوثوق بأن الرياضيات صحيحة. الآن، لدينا إثبات موثق حاسوبياً بأن الرياضيات صحيحة.
الوحدات (Modularity): يمكنك بناء الإثبات مثل قطع "الليغو". إذا أثبتَّ أن جزءاً واحداً يعمل، يمكنك إعادة استخدام هذه القطعة لإثباتات أخرى.
الأمان: يساعد هذا في منع هجمات من نوع "Meltdown" و"Spectre" في المستقبل من خلال منح مصممي العتاد طريقة دقيقة للتحقق من عملهم قبل بناء الرقائق.

ملخص التشبيه

تخيل أنك تحاول إثبات أن سيارة لعبة (العقد) تتصرف تماماً مثل سيارة سباق حقيقية (العتاد) فيما يتعلق بكمية الوقود التي تسربها.

الطريقة القديمة كانت تتمثل في قيادة كلتا السيارتين لمسافة 1000 ميل والأمل في عدم تسربهما.
هذه الورقة تبني غرفة محاكاة سحرية حيث يمكنك إيقاف الوقت، والنظر في المحركات لكلتا السيارتين في آن واحد، وإثبات رياضياً أنه إذا كانت سيارة اللعبة لا تسرب شيئاً، فإن السيارة الحقيقية لا يمكنها تسريب أي شيء أيضاً، حتى لو كانت السيارة الحقيقية تقود بسرعة أكبر أو تأخذ منعطفات مختلفة.

هذا النظام يجعل إثباتات الأمن أقل شبهاً بلعبة التخمين وأكثر شبهاً بسلسلة منطقية صارمة وغير قابلة للكسر.

إليك ملخص تقني مفصل لورقة البحث "نظام استنتاجي لإثباتات استيفاء العقود" (A Deductive System for Contract Satisfaction Proofs) من تأليف كورينسون، وزنغ، وهوفمان.

1. بيان المشكلة

تتناول الورقة تحدي التحقق من عقود الأجهزة والبرمجيات (Hardware-Software Contracts). هذه العقود هي مواصفات مجردة لسلوك تسريب البيانات في المعالج (side-channel information) على مستوى بنية مجموعة التعليمات (ISA). وهي تتيح لمطوري البرمجيات التحقق من أمن البرامج (مثل الهجمات ضد Spectre/Meltdown) دون الحاجة إلى معرفة عميقة بالتفاصيل الدقيقة للبنية المجهرية (microarchitectural details).

ولكي يكون هذا التجريد صالحاً، يجب أن يستوفي العتاد (Hardware) العقد. رسمياً، يستوفي العتاد $H$ عقداً $C$ إذا كان:
$\forall P, \sigma, \sigma', \mu. \llbracket P \rrbracket_C(\sigma) = \llbracket P \rrbracket_C(\sigma') \implies \llbracket P \rrbracket_H(\sigma, \mu) = \llbracket P \rrbracket_H(\sigma', \mu)$
وهذا يعني أنه إذا تنبأ العقد بمسارات تسريب متطابقة لمدخلين مختلفين، فيجب على العتاد الفعلي أيضاً إنتاج مسارات تسريب متطابقة.

تحديات إثبات الاستيفاء:

التعقيد العلاقاتي: الخاصية هي خاصية فائقة رباعية (4-ary hyperproperty)، تربط بين مسارين للعقد ومسارين للعتاد في آن واحد.
عدم التزامن (Asynchronicity): غالباً ما تسير عمليات تنفيذ العقد والعتاد بسرعات مختلفة (على سبيل المثال، قد يحاكي العقد خطوة التنبؤ الخاطئ خطوة بخطوة بينما ينفذ العتاد بشكل استباقي، أو قد ينفذ العتاد خارج الترتيب بينما يكون العقد تسلسلياً).
قصور الطرق الحالية:
- التحقق من النماذج (Model Checking): يعتمد غالباً على البحث الآلي عن الثوابت (invariants)، وهو ما قد يفشل في الإنهاء أو يفشل في تقديم تفسيرات لحالات الفشل.
- البراهين الورقية: معقدة للغاية (مثلاً أكثر من 25 صفحة كثيفة) ويصعب التحقق منها بدقة.
- البراهين التفاعلية الحالية: تتطلب عادةً تعريف علاقات محاكاة معقدة (مثل المحاكاة ثلاثية الأبعاد) مسبقاً، وهو أمر صعب عندما لا يوجد مترجم (compiler) بين العقد والعتاد (حيث يعمل كلاهما تحت دلالات مختلفة لنفس الـ ISA).

2. المنهجية

يقترح المؤلفون نظام برهان استنتاجي (deductive proof system) تم تنفيذه في مساعد البراهن Rocq (المعروف سابقاً بـ Coq). تعتمد المنهجية على ثلاث ركائز أساسية:

أ. تساوي المسار النسبي والمحاكاة المتماثلة النسبية

يجرد المؤلفون المشكلة إلى تساوي المسار النسبي (Relative Trace Equality): إثبات أن "تساوي المسار في النظام (أ) يستلزم تساوي المسار في النظام (ب)".

قدموا المحاكاة المتماثلة النسبية (Relative Bisimulation)، وهي علاقة رباعية ( $s_1, s_2, h_1, h_2$ ) توضح هذا الاستلزام.
الابتكار الرئيسي: على عكس المحاكاة المتماثلة القياسية (التي تتطلب خطوات متزامنة)، تتعامل المحاكاة المتماثلة النسبية مع عدم التزامن عبر فصل خطوات العقد عن خطوات العتاد.
- خطوات العقد: تُعامل استقرائياً (inductively). يسمح النظام "بتخطي" خطوات العقد (توسيع فرضية تساوي مسارات العقد) دون اشتراط تحرك العتاد.
- خطوات العتاد: تُعامل تلازمياً (coinductively). يتطلب النظام إثبات أن تسريب العتاد متساوٍ قبل المضي قدماً في حالة العتاد.
التعريف الرسمي: تُعرف المحاكاة المتماثلة النسبية بأنها النقطة الثابتة العظمى (greatest fixpoint $\nu$ ) لدالة تحتوي على نقطة ثابتة صغرى داخلية (inner least fixpoint $\mu$ ). هذا التناوب بين النقاط الثابتة أمر بالغ الأهمية لضمان السلامة (soundness): فهو يمنع البرهان من قبول جميع الحالات بشكل بديهي (مشكلة في التعريفات "المخففة" الساذجة) مع السماح في الوقت نفسه بالاستدلال غير المتزامن.

ب. الاستقراء المَعلّم (Parameterized Coinduction - Paco)

لجعل البراهن نموذجياً وتزايدياً، يستخدم النظام الاستقراء المَعلّم.

بدلاً من تخمين علاقة ثابتة كاملة مسبقاً، يقوم نظام البرهان ببناء الثابت بشكل تزايدي.
يستخدم النظام خماسيات البرهان (Proof Quintuples) ( $R \vdash [s_1, h_1, s_2, h_2]$ ) لتمثيل حالة البرهان، حيث $R$ هو "فرضية محمية" (مجموعة من رباعيات الحالة المتراكمة حتى الآن).
القواعد الأساسية:
- C-Step / C-Leak: تقدم حالات العقد (استقرائياً) أو استنتاج إذا اختلف تسريب العقد.
- H-Step: تقدم حالات العتاد (تلازمياً) فقط إذا كان التسريب متطابقاً.
- Invariant / Cycle: تسمح بتراكم أزواج حالات جديدة في الفرضية $R$ وإغلاق الدورات عند دخول الحالات مجدداً في $R$ .

ج. تقنيات "حتى" (Up-To Techniques)

لتبسيط البراهن المعقدة، يدمج النظام تقنيات "حتى" (Up-To Techniques) (استغلال التماثل والترانزيتية).

التماثل (Symmetry): تبديل الحالات أو استبدال الحالات بحالات مكافئة في التسريب.
الترانزيتية (Transitivity): تركيب البراهن عن طريق تقليل تسريب العقد أو زيادة تسريب العتاد.
يثبت المؤلفون أن هذه التقنيات سليمة (sound) عند تطبيقها في منتصف البرهان (حتى مع وجود فرضيات غير فارغة) عن طريق ترميزها كـ "دوال متوافقة" ضمن إطار عمل Paco.

3. المساهمات الرئيسية

المحاكاة المتماثلة النسبية: تقنية برهان رباعية جديدة، سليمة وكاملة، تتعامل مع عدم التزامن بين دلالات العقد والعتاد دون الحاجة إلى علاقات محاكاة محددة مسبقاً.
نظام برهان استنتاجي: نظام من قواعد الاستدلال (بناءً على الاستقراء المَعلّم) يتيح براهن نموذجية، تزايدية، وتفاعلية.
الترميز (Formalization): تم ترميز النظام بأكمله في Rocq، مع برهان تم التحقق منه آلياً لصحة واكتمال النظام بالنسبة لتساوي المسار.
تكامل تقنيات "حتى": طريقة منهجية لدمج قواعد التماثل والترانزيتية في النظام الاستنتاجي، مما يقلل بشكل كبير من تعقيد البرهان.
دراسات الحالة: التطبيق الناجح للنظام في سيناريوهين تحديين:
- عقد "التنبؤ الخاطئ الدائم" (Always-Mispredict Contract): إثبات أن عقداً يحاكي التنبؤ بالفرع (التنفيذ الاستباقي) يستوفي نموذج عتاد يحتوي على متنبئ فرع.
- العقد التسلسلي (Sequential Contract): إثبات أن عقداً ينفذ التعليمات تسلسلياً يستوفي نموذج عتاد يعمل خارج الترتيب (out-of-order execution).

4. النتائج

التحقق من مفاهيم CT-SPEC: نجح النظام في التحقق من صحة التجريدات الجوهرية لعقد CT-SPEC (معيار رائد للتحقق من الجوانب الجانبية)، وتحديداً تقنيات "التنبؤ الخاطئ الدائم" و"التنفيذ التسلسلي".
تقليل تعقيد البرهان: سمح استخدام بناء الثابت التزايدي وتقنيات "حتى" للمؤلفين بإدارة براهن كانت ستكون مستعصية أو تتطلب تخمين ثوابت يدوية ضخمة.
الترميز الآلي: البراهن مُرمزة بالكامل في Rocq، مما يلغي خطر الخطأ البشري الموجود في البراهń الورقية ويوفر مستوى عالٍ من الثقة مقارنة بالتحقق من النماذج.

5. الأهمية

تحول تأسيسي: ينقل التحقق من استيفاء العقود من نموذج (التحقق من النماذج) أو (البرهان اليدوي الورقي) إلى نموذج استنتاجي تفاعلي. هذا يسد الفجوة بين الاستدلال الأمني عالي المستوى والتفاصيل الدقيقة للبنية المجهرية.
القابلية للتوسع والنمذجة: الطبيعة التزايدية لنظام البرهان تسمح للمطورين ببناء البراهن قطعة بقطعة، وإعادة استخدام اللمات والفرضيات، وهو أمر ضروري لتوسيع النطاق ليشمل معالجات حديثة معقدة.
القابلية للتعميم: رغم التركيز على عقود الأجهزة والبرمجيات، فإن مفهوم المحاكاة المتماثلة النسبية والنظام الاستنتاجي قابلان للتطبيق في مشاييع استدلال رباعية أخرى في الأمن، مثل الترجمة الآمنة (Secure Compilation) (الحفاظ على عدم التدخل عبر الترجمة) و عدم التدخل الاستباقي (Speculative Non-Interference - SNI).
الاتجاهات المستقبلية: توضح الورقة مسارات نحو التعامل مع عدم الحتمية (non-determinism)، والتنبؤ المتداخل (nested speculation)، وتطوير منطق برنامج أعلى لتجريد تفاصيل الحالة الملموسة.

باختصار، توفر هذه الورقة إطاراً صارماً، تم التحقق منه آلياً، لإثبات أن تنفيذات العتاد تلتزم بعقود الأمان، مما يقدم بديلاً قوياً للتحقق من النماذج والتحقق اليدوي من جوانب التسريب الجانبي.