رمز إثبات الحمل

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

تم وصف رمز حمل البرهان في الأصل عام 1996 بواسطة جورج نيكولا وبيتر لي .

استخدمت الدراسة الأصلية المنشورة عام 1996 ^{[ 1 ]} حول الشيفرة الحاملة للإثبات مرشحات الحزم كمثال: حيث يُمرر تطبيق يعمل في وضع المستخدم دالةً مكتوبةً بلغة الآلة إلى النواة لتحديد ما إذا كان التطبيق مهتمًا بمعالجة حزمة شبكة معينة أم لا. ولأن مرشح الحزم يعمل في وضع النواة ، فقد يُعرّض سلامة النظام للخطر إذا احتوى على شيفرة خبيثة تكتب في هياكل بيانات النواة. تشمل الأساليب التقليدية لحل هذه المشكلة تفسير لغة خاصة بمجال ترشيح الحزم، وإضافة فحوصات على كل عملية وصول إلى الذاكرة ( عزل أخطاء البرمجيات )، وكتابة المرشح بلغة عالية المستوى تُجمّعها النواة قبل تشغيلها. تعاني هذه الأساليب من عيوب في الأداء بالنسبة للشيفرة التي تُشغّل بشكل متكرر مثل مرشح الحزم، باستثناء أسلوب التجميع داخل النواة، الذي يُجمّع الشيفرة عند تحميلها فقط، وليس في كل مرة تُنفّذ فيها.

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

• لغة التجميع المكتوبة
• اشتقاق البرنامج
• التحقق الرسمي
• مرشح حزم بيركلي

• جورج سي. نيكولا وبيتر لي. رمز حمل البرهان . تقرير فني CMU-CS-96-165، نوفمبر 1996. (62 صفحة)
• جورج سي. نيكولا وبيتر لي. وكلاء آمنون وغير موثوق بهم باستخدام رمز يحمل إثباتًا . الوكلاء المتنقلون والأمن، جيوفاني فيجنا (محرر)، سلسلة محاضرات في علوم الحاسوب، المجلد 1419، سبرينغر-فيرلاغ، برلين، ISBN 3-540-64792-9، 1998.
• جورج سي. نيكولا. التجميع باستخدام البراهين . أطروحة دكتوراه، كلية علوم الحاسوب، جامعة كارنيجي ميلون، سبتمبر 1998.