Claude يثبت أمان 123 مكتبة على مستوى شيفرة RISC-V

نشرت Anthropic وشركة Theorem نتائج مشروع كتب فيه Claude، في وضع مستقل، براهين صورية على صحة شيفرة حقيقية مفتوحة المصدر. وأثبت النموذج خلوّ 239 نقطة دخول في 123 مكتبة من مشروع Google OSS-Fuzz من حالات التعطل. ولا تعمل هذه البراهين على الشيفرة المصدرية، بل على تعليمات RISC-V المترجمة، ويبلغ مجموعها نحو 180 مليون سطر بلغة Rocq. وكان هذا النوع من العمل يتطلب في السابق سنوات من جهد متخصصين قلائل، ولذلك لم يُستخدم إلا حيث يكون ثمن الخطأ باهظًا للغاية، كما في أنظمة الطيران لدى Airbus.

اختبار fuzzing بوصفه مواصفة جاهزة

تكمن المشكلة الرئيسية في التحقق الصوري في أن عليك أولًا أن تشرح ما معنى «صحيح». فلمفكك ترميز PNG توجد وثيقة RFC 2083، أما محرر النصوص أو المتصفح فليست لهما مواصفة واضحة. وقد تحايل الباحثون على ذلك بأخذ اختبارات fuzzing الموجودة لدى المطورين وتحويل شرط «الاختبار لا يتعطل أبدًا» إلى مواصفة صورية. ووُصفت هذه المواصفة فوق نموذج يحاكي كيفية تنفيذ أي ملف ثنائي لمعمارية RISC-V داخل Linux.

يجرّب الـfuzzer عددًا هائلًا من المدخلات شبه العشوائية، لكنه لا يضمن تغطية كاملة. أما البرهان فيقدّم ضمانًا فعليًا: فإذا أثبت Claude أن الاختبار لن يتعطل مع أي مدخل أصغر من 64 ميغابايت، فلن يعثر fuzzing لنقطة الدخول هذه على RISC-V على أي شيء آخر. ويبني OSS-Fuzz برامج C وC++ مع AddressSanitizer، ولذلك يُعدّ أي وصول خاطئ إلى الذاكرة تعطلًا. وبهذا تدخل memory safety، وهي المصدر الرئيسي للثغرات، تلقائيًا ضمن الخاصية المثبتة.

ما الذي تحقق بالضبط

استغرق المشروع عدة أسابيع. ومعيار النجاح هو أن يكتب Claude البرهان وتتحقق منه نواة Rocq، فلا يحتاج الإنسان إلى قراءة مئات الآلاف من الأسطر. ويبقى الاعتماد على ثلاثة أشياء: النماذج الصورية لـRISC-V وعمليات Linux، والصياغات الدقيقة للنظريات، وRocq نفسه.

• 123 مكتبة من OSS-Fuzz، و239 نقطة دخول
• نحو 180 مليون سطر بلغة Rocq، والبرهان النموذجي نحو 600 ألف سطر
• الملف الثنائي الوسيط: 18 000 تعليمة RISC-V
• الضمان: خروج صحيح دون أخطاء في الذاكرة ودون إخفاق في assertions مع أي مدخل حتى 64 ميغابايت
• الافتراضات: ملف ثنائي ثابت (static) أحادي الخيوط، وميزانية ذاكرة ثابتة، وRISC-V وLinux

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

أخطاء ما كان fuzzing ليجدها

حين لم يكن البرهان يكتمل، كان Claude يصلح الشيفرة، ثم تُعاد صياغة المواصفة، ويحاول النموذج إثباتها من جديد. وهكذا ظهرت مئات الأخطاء. ومن شبه المؤكد أن fuzzing لم يكن ليلتقط كثيرًا منها، لأنه يُجري طفرات (mutation) على مدخلات صغيرة، لا تتجاوز عادةً 1 ميغابايت. ومن الأمثلة:

• underflow في عدّاد داخل نسخة من أداة فك الضغط، يؤدي إلى الكتابة خارج حدود المخزن المؤقت، ولا يظهر إلا مع مدخلات بحجم نحو 20 ميغابايت ذات بنية نادرة
• قراءة خارج الحدود في مفكك ترميز صور، تتطلب مدخلًا بحجم 64 ميغابايت وأكثر من 2 غيغابايت من الذاكرة
• قراءة خارج الحدود في مكتبة أخرى بعد تسلسل معيّن من الاستدعاءات عبر واصفين (descriptors) لملف واحد
• إعادة اكتشاف CVE-2026-56132 في libexpat، وهي ثغرة تتطلب تداخلًا عميقًا
• خطأ منطقي دون أي تعطل: دالة تقييد الملفات المحمّلة لم تكن تعمل دائمًا

وللأمر أثر جانبي مهم أيضًا: فحتى محاولة البرهان الفاشلة تكشف عيوبًا حقيقية. وإضافة إلى ذلك، كثيرًا ما تتحقق اختبارات fuzzing من خصائص عالية المستوى، مثل الترميز وفك الترميز دون فقدان. ففي خوارزمية الضغط LZO يؤكد الاختبار أن فك ضغط البيانات المضغوطة يعيد النسخة الأصلية. وإذا انتُهكت الخاصية يتعطل البرنامج، ولذلك فإن إثبات عدم التعطل يعادل إثبات الخاصية نفسها. أما في cpp-httplib فاضطر Claude إلى استبعاد تجاوز المكدس (stack overflow) الناتج عن تعاود عميق في المُدمِّر (destructor) الخاص بـstd::set بشكل منفصل.

الخلاصة العملية للفرق

سياق هذا العمل صارم: فقد كُشف أخيرًا في نواة Linux عن أكثر من 1000 ثغرة، كما تزداد قدرة النماذج على تركيب سلاسل استغلال (exploit chains) من أخطاء صغيرة. وللمقارنة، استغرق تنفيذ نواة seL4 سنتين من العمل البشري، فيما استغرق التحقق منها عشرين سنة. وإذا انخفضت كلفة البراهين مع نمو قدرات النماذج، وأمكن إعادة استخدام البراهين الجاهزة بين قواعد الشيفرة المختلفة، فإن المعادلة الاقتصادية تتغير.

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