Verification of Robust Properties for Access Control Policies

إليك ملخص تقني مفصل لورقة "التحقق من الخصائص المتينة لسياسات التحكم في الوصول" للباحث ألكسندر ف. غيورغيو.

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

إن سياسات التحكم في الوصول في الأنظمة الحديثة نادراً ما تكون ثابتة؛ فهي تُطوّر بشكل تكراري، وتتكون من مكونات تُدار بشكل مستقل، وتتوسع مع تطور الهياكل التنظيمية. تعتمد أدوات التحقق الحالية (مثل Margrave وZelkova وأدوات التحقق القائمة على البرمجة المنطقية ASP) على نهج دلالي نموذجي (model-theoretic) أو برمجة منطقية يفترض أن السياسة كاملة ومحددة بالكامل قبل بدء عملية التحقق.

هذا الافتراض يخلق فجوة حرجة:

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

تعالج الورقة مشكلة التحقق من الخصائص المتينة (Robust Property Verification): تحديد ما تلتزم به بنية السياسة، بغض النظر عن كيفية حل القرارات المعلقة أو كيفية توسيع السياسة لاحقاً.

٢. المنهجية

يقترح المؤلف إطار عمل قائماً على الدلالات القائمة على نظرية الإثبات (Proof-Theoretic Semantics)، وتحديداً دلالات تمديد القاعدة (Base-Extension Semantics). بدلاً من تعريف الحقيقة عبر نماذج ثابتة، يعرّف الإطار معنى الخاصية من خلال سلوكها الاستنتاجي عبر جميع التمديدات الممكنة للسياسة.

أ. حكم الدعم ($\Vdash_P \phi$)

الكائن الدلالي الأساسي هو الحكم $\Vdash_P \phi$، والذي ينص على أن السياسة $P$ تمتلك الخاصية المتينة $\phi$. يتم تعريف هذا الحكم استقرائياً على بنية $\phi$:

• الذري (Atomic): $\Vdash_P A$ إذا وفقط إذا كان $A$ قابلاً للاشتقاق من $P$ ($\vdash_P A$).
• الاستلزام ($\Rightarrow$): $\Vdash_P \phi \Rightarrow \psi$ إذا وفقط إذا كان لأي تمديد $Q \supseteq P$، إذا تحقق $\Vdash_Q \phi$ فإن $\Vdash_Q \psi$. وهذا يجسد الالتزامات الشرطية.
• الفصل المتين ($\oplus$): $\Vdash_P \phi \oplus \psi$ إذا وفقط إذا كان لأي تمديد $Q \supseteq P$ وأي صيغة ذرية $A$، إذا كان $\phi$ يفرض $A$ في $Q$ و$\psi$ يفرض $A$ في $Q$، فإن $A$ قابلة للاشتقاق في $Q$. وهذا يسمح بالاستدلال حول البدائل المعلقة (على سبيل المثال: "أياً كان من سيتم اختياره كرئيس، فإن قاعدة تضارب المصالح ستظل قائمة") دون الالتزام باختيار محدد.
• الاقتران المتين ($\otimes$): $\Vdash_P \phi \otimes \psi$ إذا وفقط إذا كان لأي تمديد $Q \supseteq P$ وأي صيغة ذرية $A$، إذا كان $\phi$ و$\psi$ يفرضان $A$ مجتمعين في $Q$، فإن $A$ قابلة للاشتقاق في $Q$. وهذا يضمن تحقق الخصائص في آن واحد، ويكشف حالات الفشل حيث تحقق القواعد قيوداً فردية ولكنها تكسر قواعد الجمع بينها.
• النفي ($\neg$): يُعرَّف كـ $\phi \Rightarrow 0$، حيث يمثل $0$ فساد السياسة (policy corruption) (وهي حالة تصبح فيها كل الصيغ الذرية قابلة للاشتقاق). $\Vdash_P \neg \phi$ تعني أن أي تمديد يدعم $\phi$ يؤدي إلى إفساد السياسة.

ب. الخصائص النظرية الرئيسية

• الرتابة (Monotonicity) (الافتراض 6): إذا كان $\Vdash_P \phi$ و $P \subseteq Q$، فإن $\Vdash_Q \phi$. هذا هو أساس التركيبية (Compositionality): بمجرد التحقق من خاصية متينة، فإنها تظل صالحة تحت أي تمديد مستقبلي للسياسة، مما يلغي الحاجة لإعادة التحقق.
• الاستدلالية (Inferentiality): يعتمد الإطار حصرياً على علاقة الاشتقاق ($\vdash$) ولا يتطلب نماذج أو قيم خارجية.

ج. الاختزال الحسابي

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

• الترميز (Encoding): يتم ترميز الخصائص المتينة إلى أهداف برمجة منطقية ($\lceil \cdot \rceil$) باستخدام أسلوب تمرير الاستمرارية (continuation-passing style) والمكممات الذرية من الدرجة الثانية.
  • يُرمز الفصل ($\oplus$) والاقتران ($\otimes$) باستخدام التكميم الكلي من الدرجة الثانية على المحمولات الذرية ($\forall X$).
• الدلالات التشغيلية: يختزل التحقق من المتانة إلى بحث موحد عن الإثبات (باستخدام قواعد مثل Fact وBackchain وAugment وGeneric وInstance) في لغة قائمة على جمل هورن (Horn-clause).
• النظرية 12 (الصحة والاكتمال): $\Vdash_P \phi$ إذا وفقط إذا كان $P \vdash_O \lceil \phi \rceil$. وهذا يثبت أن الحكم الدلالي قابل للتقرير وقابل للتنفيذ.

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

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

٤. النتائج

• نظرياً: نجح الإطار في سد الفجوة بين المتانة الدلالية (التكميم عبر جميع التمديدات) والجدوى الحسابية (البحث عن إثبات منتهٍ).
• عملياً: يعني الاختزال إلى البرمجة المنطقية أنه يمكن استخدام أدوات موجودة (مثل $\lambda$Prolog أو Twelf) لتنفيذ التحقق من المتانة.
• دراسة حالة: تم تطبيق الإطار على مثال نظام إدارة مؤتمرات. وقد نجح في التحقق من:
  • فصل المهام (Separation of Duty): إثبات أنه أياً كان من سيتم تعيينه كرئيس (آليس، أو بوب، أو كارول)، فإنه لا يمكنه مراجعة ورقته الخاصة، حتى قبل اتخاذ قرار التعيين.
    તેમને سلامة التفويض (Delegation Safety): إثبات أن قواعد التفويض تمنع تضارب المصالح هيكلياً بغض النظر عن التعيينات المستقبلية.
  • القيود المركبة (Compound Constraints): اكتشاف حالات الفشل حيث تحقق القواعد قيوداً فردية ولكنها تفشل عند الجمع بينها (عبر الاقتران المتين).

٥. الأهمية

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

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