الخلاصة

  • رتبت Dorothy E. Denning في بحثها المنفرد عام 1976 فئات الأمن ترتيباً جزئياً، واستخدمت الحد الأعلى الأدنى، أو join، لتحديد الفئة الدنيا لنتيجة تتأثر بمدخلات متعددة.
  • يتتبع النموذج النقل الصريح والتبعيات الضمنية الناتجة عن شروط التحكم، لكنه يثبت فقط التدفقات التي تظهر في تمثيل البرنامج وتحت التسميات والترتيب المعلنين.
  • تظل القنوات الخفية وسوء التصنيف وعيوب التنفيذ وخفض السرية بلا مبرر مسائل منفصلة. اجتياز فحص الشبكة دليل على ضابط واحد، وليس حكماً على النظام كله.

عندما تعتمد نتيجة واحدة على مدخلين مختلفين، إلى أي فئة يجوز أن تذهب؟ في بحث “A Lattice Model of Secure Information Flow” تجيب Dorothy E. Denning: نأخذ أدنى فئة يُسمح لكلا المدخلين بالوصول إليها. هذا هو الحد الأعلى الأدنى، أو join.

تعني الصيغة A → B أن معلومات الفئة A مسموح لها بالتدفق إلى B. العلاقة انعكاسية ومتعدية ومضادة للتناظر، ولذلك تشكل ترتيباً جزئياً. يمكن لفئتين معزولتين ألا تكونا قابلتين للمقارنة، مع وجود فئة عليا مشتركة. وإذا كانت c تعتمد على a وb فالمطلوب هو class(a) join class(b) → class(c).

تحول هذه القاعدة السياسة إلى سؤال قابل للفحص. لكنها لا تقول إن c آمنة في الواقع، بل تقول إن التأثير الممثل مسموح به ضمن التصنيفات والترتيب المختارين.

الشرط ينقل معلومة أيضاً

يعرف النموذج التدفق بوصفه تأثيراً، لا مجرد نسخ. الإسناد b := a تدفق صريح. أما if a = 0 then b := c فينشئ تبعية ضمنية: قد تكشف الحالة النهائية لـ b ما إذا كان الشرط المتعلق بـ a قد تحقق، رغم عدم نسخ قيمة a.

لا يزال ذلك مهماً في البرمجيات الحديثة. الفروع والأخطاء والعدادات والتوقيت قد تحمل إشارات إلى جانب الحقول المنقولة. جرد صلاحيات القراءة وحده لا يلتقط هذه العلاقات؛ على التحليل أن يجمع فئات كل ما يؤثر في المخرج.

يمكن نشر فئات المتغيرات والتعبيرات وشروط التحكم قبل التشغيل ورفض الوجهات غير المسموحة. توسع ورقة “Certification of Programs for Secure Information Flow” هذه الآلية.

ويجب حفظ نسبة العمل بدقة. بحث الشبكة لعام 1976 من تأليف Dorothy E. Denning وحدها. أما بحث الاعتماد فهو من تأليف Dorothy E. Denning وPeter J. Denning معاً، ونشر عام 1977 بعد Purdue Technical Report 76-181. الخلط بينهما يمحو المؤلف المشارك ويخفي الانتقال من النموذج إلى منهج الاعتماد.

أين يتوقف البرهان

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

التسميات نفسها افتراضات. إذا وسم سر بأنه عام، فقد يسمح التحليل بدقة بتدفق لم ترده المؤسسة. وفي الاتجاه الآخر، يؤدي السماح بالصعود فقط إلى الإفراط في التصنيف. تناقش الدراسة المشتركة “Data Security” خفض السرية المصرح به والبرامج التي تفقد معلومات. لكن كليهما يحتاج إلى سلطة ودليل مستقلين: من أجاز، وما الذي أزيل، وكيف اختُبر؟

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

عادت Denning عام 1999 إلى هذا المبدأ في “The Limits of Formal Security Models”: تثبت الأساليب الشكلية خصائص داخل نموذج مبسط وافتراضاته، بينما تخرج الهجمات الواقعية كثيراً عن ذلك الصندوق. الدرس ليس التخلي عن البرهان، بل تسمية نطاقه بأمانة.

البرهان داخل سلسلة أدلة

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

ينتمي Bell–LaPadula إلى التاريخ المجاور للأمن متعدد المستويات ويظهر في مراجع Denning، لكنه لا يحل محل حجتها. يسأل التحكم في الوصول إن كان للفاعل حق تنفيذ عملية؛ وتسأل شبكة التدفق عن الفئة التي يجب أن ترثها النتيجة من كل المعلومات المؤثرة فيها.

لذلك يبقى النموذج نافعاً: يثبت خاصية مهمة بدقة، من دون أن يستخدم دقته لإخفاء الأسئلة المتبقية.

المصادر