ما الذي يستطيع البرهان أن يعد به

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

أما البرهان فيبدأ من الطرف الآخر. إنه لا يجرّب حالات. بل يبيّن، بالرياضيات، أن عبارةً ما تصح فيها كلها.

كل الحالات، لا التي جرّبناها فقط

خذ وعدًا صغيرًا: هذه الشيفرة لا تقرأ أبدًا ما بعد نهاية مخزنها المؤقت. يستطيع الاختبار أن يعطيها ألف مدخل، أو مليار مدخل، ثم يفيد بأن أيًّا منها لم يُفشلها. أما البرهان فيقول شيئًا من نوع آخر: لا يوجد مدخل يُفشلها. لم يُعثر على واحد، ولا وجود لواحد.

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

متحقق منه آليًا

هذا معنى «متحقق منه آليًا». يُكتب البرهان كاملًا، بلغة يستطيع قراءتها برنامج يسمى مساعد البراهين، ويتحقق البرنامج من كل خطوة وفق قواعد المنطق. لا يتعب عند الصفحة التسعمئة، ولا يأخذ بكلام أحد.

وهكذا يُتحقق من براهين seL4، في مساعد براهين اسمه Isabelle/HOL. وهي منشورة للعموم، ويستطيع أي أحد أن يعيد تشغيلها.

ما تقوله براهين seL4

seL4 هي النواة التي يعمل عليها كل نظام من أنظمة NoWayOS: نحو 10,000 سطر من الشيفرة، وهي الشيفرة الوحيدة التي تتحكم بالجهاز تحكمًا كاملًا. وحجمها هو بيت القصيد. فالحجة حول عشرة آلاف سطر يمكن إتمامها. أما الحجة حول عشرات الملايين فلا يمكن إتمامها بعد.

تعرض seL4 Foundation هذه البراهين في طبقات:

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

وليست كل طبقة مكتملة لكل معالج ولكل إعداد. وهذا مهم، وسنعود إليه.

ما يسلّم به البرهان

البرهان واسع بقدر عبارته تمامًا، وهو يقوم على افتراضاته. وتدوّن seL4 افتراضاتها: أن العتاد يتصرف كما يقول نموذجه، وأن بضع مئات من أسطر الشيفرة في أدنى مستوى صحيحة، وأن الشيفرة التي تعمل قبل بدء النواة قد أدّت عملها. وبرهان السرية لا يغطي التوقيت.

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

وليس هذا ضعفًا في البراهين. بل هو ما يجعلها جديرة بالاقتناء: إنها تقول بدقة ما تغطيه، فتعرف بدقة ما الذي بقي.

أين يقف NoWayOS

هذا هو الموقف بوضوح. يعمل NoWayOS على seL4، لكن لا توجد اليوم صورة من صور NoWayOS داخل براهين seL4 المكتملة. يستخدم NoWayOS إعداد الحرجية المختلطة في seL4، وبراهينه لمعالجاتنا ما زالت جارية. وبراهين seL4 لم تغطِّ قط شيفرة NoWayOS نفسه. لذلك لا نصف NoWayOS بأنه “متحقق منه رسميًا”، ولن نفعل.

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

براهين أصغر من صنعنا

تحصل شيفرة NoWayOS على ضمانها بطريق آخر: Rust، والعزل، والمراجعة، والاختبار، وبراهين من نوع أكثر تواضعًا.

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

ثم نُفسد المفككات عمدًا، لنتأكد من أن البراهين تنتبه. فالبرهان الذي لا يمكن أن يفشل ليس أفضل من اختبار لا يمكن أن يفشل.

حجمه الصادق

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

ولهذا بُني NoWayOS على النواة التي تملك هذه البراهين، ولهذا يخبرك، صورةً صورة، إلى أين تصل.