ما الذي أُثبت فعلاً
نشر فريق أنثروبيك الأحمر للحدود، بالتعاون مع شركة ثيورم، في الثاني والعشرين من أكتوبر نتائج محاولة لاستخدام كلود في التحقق الشكلي على نطاق واسع. أخذ الفريق اختبارات تشويش قائمة من مشروع «أو إس إس فَز» التابع لغوغل، وعدّ كل اختبار خاصية يجب أن يحققها الكود، وترجمه إلى لغة تجميع «ريسك-في»، ثم كلّف كلود بكتابة براهين يتحقق منها الحاسوب على أن الملف الثنائي الناتج لا ينهار أبداً.
والخاصية ضيّقة ودقيقة: لأي مُدخل دون أربعة وستين ميغابايت لن ينهار البرنامج بخطأ في أمان الذاكرة ولا بتأكيد فاشل. وتفترض البراهين ملفاً ثنائياً ساكناً أحادي الخيط بميزانية ذاكرة ثابتة يعمل على معالج «ريسك-في» تحت لينكس، وتثق بمدقق البراهين «روك»، وبدلالات «ريسك-في» وعمليات لينكس التي طوّرتها ثيورم، وبالعتاد ومترجم «أوكامل» تحتها.
الأرقام
في 123 مكتبة مفتوحة المصدر، أثبت كلود خلوّ 239 نقطة دخول من الانهيار وفق تلك المواصفة. وتبلغ البراهين مجتمعةً نحو 180 مليون سطر بلغة روك. والبرهان النموذجي نحو ستمئة ألف سطر، مقابل طول وسيط للملف الثنائي يبلغ نحو ثمانية عشر ألف تعليمة «ريسك-في». واستغرق العمل بضعة أسابيع.
ولا تذكر أنثروبيك كم نقطة دخول جُرّبت إجمالاً، ولذلك لا تسمح الأرقام باستخلاص نسبة نجاح. وتقول الشركة إنها تنشر براهين الاختبارات التي لم تحتج إلى ترقيع، ومواصفات تلك التي عجزت عن إثباتها.
وظهرت مئات العلل في الطريق، فرقّعها كلود، وهو ما كان يعيد توليد المواصفات. ومن الأمثلة المذكورة: تدفّق سفلي لعدّاد في برنامج فكّ ضغط يسبب كتابة خارج الحدود فقط في ترتيب نادر لنحو عشرين ميغابايت من المُدخلات؛ وقراءة خارج الحدود في فاكّ ترميز صور يحتاج مُدخلاً بأربعة وستين ميغابايت وأكثر من اثنين غيغابايت من الذاكرة؛ وإعادة اكتشاف الثغرة «سي في إي-2026-56132» في مكتبة «ليب إكسبات». وكان أحدها خاصية تقييد ملفات لا تُطبَّق دائماً: علّة منطقية لا تسبب انهياراً قط، وظلّت كامنة أكثر من عقد.
الحيلة الواضحة وما فُعل حيالها
في هذا الترتيب ثغرة يسمّيها الفريق بنفسه. فقد كان بوسع كلود أن يجعل المبرهنة قابلة للإثبات بإعادة كتابة البرنامج كي لا ينهار أبداً. وتقول أنثروبيك إنها عاقبت الترقيعات التي تغيّر السلوك، ومنحت رصيداً إضافياً لإثبات أي المُدخلات يغيّرها ترقيع ما، وسجّلت كل ترقيع ودقّقته.
المشكلة المفتوحة هي الكلفة
على مجموعة قياس من ستٍ وثلاثين مهمة تحقق صغيرة مبنية من كود حقيقي في «أو إس إس فَز»، بثلاث محاولات مستقلة وميزانية خمسة ملايين رمز لكل منها، أثبت «أوبس 5.5» نصفها مستخدماً نحو أربعين في المئة من الرموز أقل من «أوبس 5». أما الوكلاء الذين سُمح لهم بنسخ براهين بعضهم من مساحة عمل مشتركة فاستهلكوا سبعة عشر في المئة رموزاً أقل وأنجزوا أربعاً وثلاثين من الستّ والثلاثين، مقابل اثنتين وثلاثين للوكلاء العاملين منفردين.
وأنثروبيك صريحة بشأن الحدود. فعبارة «مُتحقَّق شكلياً» لا تعني خلوّه من العلل: إذ لا يستطيع مدقق البراهين تأكيد مطابقة المواصفة للواقع، وقد تبقى علل في المواصفة أو نموذج الآلة أو القاعدة الموثوقة. وتغطي البراهين ملفات «ريسك-في» المربوطة بمكتبة «مَسل»، بينما تعمل معظم عمليات النشر على «إكس 86» أو «آرم» مع «غليبسي» مربوطة ديناميكياً. كما قد يكلّف برهان واحد مئات ملايين الرموز، وهو ما تسمّيه الشركة مشكلة مفتوحة أساسية.
وبصورة منفصلة، كتب كلود مواصفة انطلاقاً من المعيار «آر إف سي 1950» وأثبت أن تطبيق «زد ليب» في نواة لينكس يحققها على مستوى الملف الثنائي لمعمارية «إكس 86». وتقول أنثروبيك إنها كررت ذلك مع نحو ست مكتبات أخرى واسعة الاستخدام. والسؤال الجدير بالمتابعة هو ما إذا كان هذا العمل سيتعمّم أبعد من ذلك.
