Access Hoare Logic

إليك ملخص تقني مفصل لورقة "منطق هوار للوصول" (Access Hoare Logic) من تأليف أرنولد بيكمان وأنتون ستيتزر.

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

يعد منطق هوار القياسي (Standard Hoare Logic) الإطار التأسيسي للتحقق من صحة البرامج الحاسوبية. وهو يعمل على مبدأ الكفاية (Sufficiency): إذا تحقق الشرط المسبق $P$ قبل التنفيذ، وانتهى البرنامج، فإن الشرط اللاحق $Q$ سيتحقق حتماً. صياغتها الرسمية: $\{P\} C \{Q\}$.

ومع ذلك، تتطلب أمن الوصول (Access Security) (مثل التحكم في الوصول، والمصادقة، والعقود الذكية في البلوكشين) ضماناً منطقياً مختلفاً جوهرياً. لكي يكون النظام آمناً من حيث الوصول، يجب أن يضمن منح الوصول فقط إذا استوفيت شروط محددة قبل التنفيذ. هذا سؤال عن الضرورة (Necessity)، وليس مجرد الكفاية.

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

2. المنهجية

يقترح المؤلفان منطق هوار للوصول (aHl)، وهو نظام صوري يعكس اتجاه الاستدلال الموجود في منطق هوار القياسي.

المفهوم الجوهري: ثلاثية هوار للوصول

بدلاً من $\{P\} C \{Q\}$، يستخدم aHl الثلاثية $\langle P \rangle C \langle Q \rangle$.

• الدلالات (Semantics): تكون $\langle P \rangle C \langle Q \rangle$ صالحة إذا وفقط إذا كان لكل الحالات $s, s'$، إذا أدى تنفيذ $C$ في الحالة $s$ إلى الحالة $s'$ حيث يتحقق $Q$، فإن $P$ يجب أن تكون قد تحققت في الحالة $s$.
• التعريف الرسمي: $\forall s, s'. [s \xrightarrow{C} s' \land Q(s') \implies P(s)]$.
• الاتجاه المنطقي: إنه يستدل للخلف من الشرط اللاحق إلى الشرط المسبق. $P$ هي شرط ضروري لـ $Q$.

الحساب (The Calculus)

يحدد المؤلفان حساباً مباشراً لـ aHl مع قواعد محددة تختلف عن منطق هوار القياسي لاستيعاب متطلب "الضرورة":

1. الإسناد (Assignment): $\langle P[E/V] \rangle V := E \langle P \rangle$ (مشابه لهوار، ولكن يُفسر كضرورة).
2. قاعدة الاستتباع (Consequence Rule): هذا هو الانحراف الأكثر أهمية.
   • منطق هوار القياسي: يمكننا تقوية الشرط المسبق وإضعاف الشرط اللاحق.
   • هوار للوصول: يمكننا إضعاف الشرط المسبق وتقوية الشرط اللاحق.
   • الاستدلال: إذا كان $P_2 \implies P_1$ و $Q_2 \implies Q_1$، ونحن نعلم أن $Q_2$ تستلزم $P_2$، فإن $Q_1$ (شرط أقوى) تستلزم $P_1$ (شرط أضعف).
3. قواعد الشرط (Conditional) والحلقة (While): تم تكييف القواعد لاستخدام الاستلزام ($B \to P$) بدلاً من العطف ($B \land P$) في المقدمات، مما يعكس التدفق العكسي للمنطق.

العلاقة بالمنطق القياسي

• ثنائية النفي (Negation Duality): تثبت الورقة أن $\langle P \rangle C \langle Q \rangle$ مكافئة منطقياً لـ $\{\neg P\} C \{\neg Q\}$ في المنطق الكلاسيكي.
• المنطق الحدسي (Intuitionistic Logic): يجادل المؤلفون ضد مجرد اختزال aHl إلى منطق هوار القياسي عبر النفي. القيام بذلك يؤدي إلى إدخال علاقات مضادة (مثل $\neg B \to \neg A$) والتي يصعب التعامل معها في مبرهنات المنطق الحدسي (مثل Coq) ويمكن أن تكسر قابلية التحقق. لقد أثبتوا أنه يمكن بناء aHl مباشرة باستخدام المنطق الحدسي.

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

1. تعريف منطق هوار للوصول: نظام صوري مصمم خصيصاً للاستدلال حول أمن الوصول، مما يميزه عن صحة البرامج العامة.
2. براهين السلامة والتمام (Soundness and Completeness): يثبت المؤلفان أن حسابهم سليم (الثلاثيات المثبتة صالحة) وتام (كل الثلاثيات الصالحة قابلة للإثبات) فيما يتعلق بالتعريف الدلالي.
3. الارتباط بالشرط المسبق الأقوى/الأضعف:
   • حددوا الشرط المسبق الأقوى لـ aHl ($P_s$) كمجموعة الحالات التي يمكن أن تصل إلى شرط لاحق $Q$.
   • أثبتوا أنه بالنسبة للبرامج التي تنتهي، يتطابق الشرط المسبق الأقوى في aHl مع الشرط المسبق الأضعف في منطق هوار القياسي.
   • يوفر هذا جسراً نظرياً: $P_s^{aHl} = P_w^{Hoare} \cap \text{TerminationSet}$.
4. التمييز عن منطق عدم الصحة (Incorrectness Logic): توضح الورقة أنه بينما يعد "منطق عدم الصحة" (الذي يستخدم التقريب من أسفل) رؤية عكسية للمحول الأمامي للمنطق القياسي، فإن aHl هو الرؤية العكسية الصحيحة للمحول الخلفي (أمن الوصول).

4. النتائج والأمثلة

تتحقق الورقة من الإطار من خلال ثلاثة أمثلة متميزة:

• المفاتيح الإلكترونية (نظام الفنادق):
  • السيناريو: يقوم قفل الباب بتحديث مفتاحه بعد استخدام الضيف لبطاقة.
  • النتيجة: يظهر المؤلفون أن برنامجاً ذا تحليل لغوي غامض (حيث يتم تنفيذ acc := true دون شرط) يفشل في اختبار aHl لأن الشرط المسبق (امتلاك مفتاح صالح) ليس ضرورياً للشرط اللاحق (الباب مفتوح). التحليل اللغوي الصحيح يجتاز الفحص.
• عقود البيتكوين الذكية (Bitcoin Smart Contracts):
  • السيناريو: التحقق من نص القفل scriptPubKeyP2PKH.
  • النتيجة: يثبت المنطق أنه لكي تنجح المعاملة (الشرط اللاحق: قمة المكدس هي true)، يجب أن يكون نص فك القفل قد قدم توقيعاً ومفتاحاً عاماً (public key hash) صالحين (الشرط المسبق). هذا يضفي صبغة رسمية على ضمانة الأمن لمعاملات البيتكوين.
• حلقة التحكم في الوصول (CheckList):
  • السيناريو: منح الوصول إذا وجد مفتاح في قائمة.
  • النتيجة: اشتقاق رسمي باستخدام ثوابت الحلقة (loop invariants) يوضح أن الوصول يُمنح فقط إذا تم العثور على المفتاح في القائمة، مما يثبت ضرورة نتيجة البحث.

5. الأهمية

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

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