التحقق الرسمي من البرمجيات مع Claude يشمل 123 مكتبة مفتوحة

شيفرة بلغة التجميع على شاشة بجانب براهين رياضية يدققها برنامج تحقق آلي

تحقق رسمي احتاج في seL4 إلى 20 سنة عمل بشري صار يُنجز آلياً: 180 مليون سطر برهان لـ123 مكتبة خلال أسابيع.

ضمن ملف: Anthropic، نماذج الذكاء الاصطناعي

بقلم: نور | محررة الأبحاث والدراسات · صوت تحريري بإشراف بشري

المصدر الأساسي: Anthropic Research

لماذا يهم

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

صارت 239 نقطة دخول في 123 مكتبة مفتوحة المصدر تحمل برهاناً رياضياً على أنها لن تنهار مع أي مدخل يقل حجمه عن 64 ميغابايت (وفقاً لـ Anthropic). كتب Claude هذه البراهين خلال أسابيع قليلة، وهي لا تعمل على الشيفرة المصدرية بل على التعليمات المترجمة إلى لغة تجميع RISC-V، أي على الملف التنفيذي الذي يعمل فعلاً. نشرت Anthropic النتائج في ورقة بحثية بالتعاون مع شركة Theorem، ووقّعها فريق يضم Keane Lucas وAengus Lynch وLuna Tong وNicholas Carlini وNickolai Zeldovich وJason Gross وآخرين. وتصف الشركة العمل بأنه، “على حد علمها”، أول محاولة واسعة النطاق لاستخدام الذكاء الاصطناعي في التحقق الرسمي من برمجيات إنتاجية على مستوى لغة التجميع. القصة تستند إلى مصدر وحيد هو الورقة البحثية نفسها، وكل الأرقام الواردة فيها أرقام معلنة من الشركة نفسها لم يتسنَّ التحقق منها بشكل مستقل حتى الآن.

تبدأ الورقة من تشخيص أمني قاتم، فمعظم البرمجيات مليئة بالأخطاء، والنماذج اللغوية باتت تجدها وتستغلها بسهولة. مثالها الأوضح نواة Linux، وهي من أكثر البرمجيات اختباراً وتعمل على مليارات الأجهزة، وقد كُشف فيها مؤخراً عن أكثر من 1,000 ثغرة (وفقاً لـ LWN.net). وتربط Anthropic ذلك بأبحاثها السابقة عن قدرة النماذج على تطوير الاستغلالات، وبتجربة Mozilla في تقوية Firefox باستخدام نموذج Claude Mythos Preview. حجتها أن النماذج الرائدة تتحسن في ربط أخطاء تبدو بريئة لتصنع منها استغلالات حرجة، ولذلك لم تعد الدفاعات المعتادة كافية، والمطلوب أدوات تجد الأخطاء وتصلحها ثم تقدم دليلاً على أنه لم يعد هناك المزيد.

التحقق الرسمي هو الطريقة التي تقدم هذا الدليل. يترجم المطور شيفرته إلى نموذج رياضي، ثم يحاول إثبات أنها تلتزم دائماً بمجموعة محددة من القواعد الأمنية. فشل الإثبات يعني احتمال وجود خطأ، وطبيعة الفشل تشير إلى مكانه. ومع تكرار الدورة بعد إزالة سبب الفشل في كل مرة، يصل المطور إلى برهان على خلو الشيفرة من أي خطأ يخالف تلك القواعد. العائق كان الكلفة دائماً، فالبراهين قد تكون أكبر من الشيفرة الأصلية بأضعاف، وكتابتها تحتاج مهارة نادرة. بناء نواة نظام التشغيل seL4 استغرق سنتي عمل بشري، بينما احتاج التحقق الرسمي منها إلى 20 سنة عمل بشري (وفقاً لـ Anthropic). لهذا ظلت التقنية حكراً على التطبيقات بالغة الحساسية مثل برمجيات الطيران في Airbus.

وقبل أي برهان يجب تعريف معنى “الصحيح”، أي كتابة المواصفة. بعض البرامج مواصفتها واضحة، مثل مفكك صور PNG الذي يحوّل البايتات إلى صورة وفق المعيار RFC 2083. لكن ما معنى أن يكون محرر نصوص أو متصفح ويب صحيحاً؟ هنا جاء الحل الأذكى في الورقة، وهو تحويل اختبارات الـ fuzzing التي كتبها المطورون أصلاً إلى مواصفة رسمية تقول إن “هذا الاختبار ينجح دائماً”. في الـ fuzzing يكتب المطور نقطة دخول تستقبل المدخلات، ويضخ محرك الاختبار فيها أعداداً هائلة من المدخلات شبه العشوائية والمعدّلة بحثاً عن انهيار. إنه أسلوب قائم على القوة الغاشمة، والمدخلات الممكنة لا نهائية، فلا يضمن المرور بكل مسار مهما طال التشغيل. أما إذا أثبت Claude المواصفة، فيصبح تشغيل الـ fuzzing على تلك النقطة بلا جدوى لأنه لن يجد شيئاً.

بحسب الورقة البحثية، تتلخص نتائج التجربة في خمس نتائج رئيسية:

على صعيد الحجم، بلغت البراهين نحو 180 مليون سطر بلغة Rocq، والبرهان النموذجي نحو 600,000 سطر لملفات تنفيذية متوسط طولها 18,000 تعليمة RISC-V (وفقاً لـ Anthropic). البرهان إذن أكبر من الشيفرة التي يغطيها بنحو 33 مرة، وهو بالضبط نوع العمل الطويل المحدد الهدف الذي تتفوق فيه النماذج ويستنزف البشر.
طُبّق المسار على مئات المشاريع من مبادرة OSS-Fuzz من Google، التي توفر اختباراً مستمراً للمشاريع المفتوحة المؤهلة وتضم آلاف نقاط الدخول التي كتبها المطورون. تُجهَّز برامج C وC++ فيها تلقائياً بأداة AddressSanitizer التي تُسقط البرنامج عند أي وصول غير سليم إلى الذاكرة، وهو من أبرز أسباب الثغرات. تُترجم المكتبة واختبارها إلى ملف RISC-V، ثم تُستخرج المواصفة آلياً من النماذج الرسمية التي طورتها Theorem لتعليمات RISC-V ولعمليات Linux، فيكتب Claude البرهان وتتحقق منه نواة Rocq.
لا يحتاج هذا الكم من البراهين إلى مراجعة بشرية تقريباً، لأن مدقق Rocq هو من يضمن مطابقة البرهان للمواصفة. ما يبقى على المطور أن يثق به ثلاثة مكونات فقط: النماذج الرسمية لـ RISC-V ولعمليات Linux، والصيغة الدقيقة للمبرهنات المثبتة، ومدقق Rocq نفسه. والأهم أن هذه المكونات لا تكبر مهما زاد عدد المشاريع المثبتة.
كشفت محاولات الإثبات مئات الأخطاء (وفقاً لـ Anthropic)، بعضها أفلت من الاكتشاف لسنوات رغم تريليونات عمليات الاختبار بحسب الورقة. ولكي لا يتوقف Claude بانتظار إنسان، سُمح له بإصلاح الشيفرة، فتُولَّد المواصفة من جديد بعد كل إصلاح ويتابع إثباتها. كثير من هذه الأخطاء يصعب أن يبلغه أي fuzzer، لأن أدوات الـ fuzzing تعدّل مدخلات صغيرة لا تتجاوز عادة 1 ميغابايت (وفقاً لـ Anthropic) وتعتمد على تغطية الشيفرة لتوجيه البحث، بينما يستبعد البرهان كل انهيار على أي مسار يمكن بلوغه من نقطة الدخول.
الضمان محدود بشروط صريحة، فالبراهين تفترض برنامجاً أحادي الخيط، مبنياً كملف ثابت، بميزانية ذاكرة ثابتة، على معالج RISC-V ونظام Linux. وتصر الورقة على أن هذا لا يعني خلو المكتبات من الأخطاء، فأي خطأ متبقٍّ إما داخل المكونات الموثوقة أو خارج نطاق البرهان. وترى Anthropic أن توسيع النطاق “في المتناول” عبر توحيد النماذج الرسمية لمعماريات وعمليات أنظمة تشغيل أخرى، وهو تقدير لم يُختبر بعد.

على المستوى العملي، تنشر Anthropic جزءاً من البراهين ليتمكن أي شخص من التحقق منها وإعادة استخدامها: البراهين الكاملة للاختبارات التي لم تحتج إلى إصلاح، والنماذج الرسمية لـ RISC-V ونظام التشغيل غير المنشورة سابقاً، ومواصفات الاختبارات التي لم يتمكن الفريق من إثباتها، مع دعوة صريحة للتحقق المستقل. وتعرض Theorem تشغيل المسار نفسه لمشاريع مفتوحة المصدر أخرى، وتنشر “مهارة” (skill) لـ Claude تساعد المطورين على البدء بالتحقق من شيفرتهم. لم تُعلن أي تفاصيل عن تسعير هذه الخدمة أو شروط الأهلية لها. وتذكر الورقة أيضاً تجارب أولية بأساليب تحقق رسمي أخرى، منها تقييم أمان خوارزمية الضغط zlib، وإثبات التكافؤ السلوكي لمفسّر Python مكتوب بلغة Rust، واقتلاع أخطاء قديمة من برمجيات حرجة.

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

تقديرنا أن الخبر الحقيقي ليس رقم 180 مليوناً، بل انقلاب اقتصاديات التحقق الرسمي: تقنية كانت تكلّف عشرة أضعاف كتابة البرنامج صارت تُنفَّذ آلياً على مئات نقاط الدخول، مع قاعدة ثقة ثابتة الحجم. لكن الحماس يجب أن يبقى مضبوطاً، فضمان “عدم الانهيار” لا يغطي الأخطاء المنطقية، ولا البرامج متعددة الخيوط، ولا معماريات مثل x86 وARM التي تشغّل معظم الخوادم والهواتف، ولم تصدر بعد مراجعة مستقلة منشورة للنتائج. إذا كنت تدير مكتبة ضمن OSS-Fuzz، فالسؤال لم يعد هل يمكنك تحمّل كلفة التحقق الرسمي، بل هل تستطيع تبرير تركه للمهاجمين الذين يستخدمون النماذج نفسها للبحث عن ثغراتك.

المصادر