كلود يبرهن رياضياً سلامة 123 مكتبة مفتوحة ويكتشف مئات الثغرات

خبر:

أنتج كلود براهين رسمية مُتحقَّقاً منها آلياً تثبت أن 239 نقطة دخول في 123 مكتبة مفتوحة المصدر لا تنهار ولا تقع في أخطاء سلامة الذاكرة لأي مدخل يقل عن 64 ميغابايت، بحسب ما نشره فريق Frontier Red Team في أنثروبيك في 22 أكتوبر 2026 بالتعاون مع شركة Theorem. وخلال العمل اكتشف النموذج مئات الثغرات التي أفلتت من تريليونات عمليات الاختبار، ورقّعها قبل إتمام البراهين.

تفصيل:

• حجم العمل: بلغ مجموع البراهين نحو 180 مليون سطر بلغة Rocq، ويمتد البرهان النموذجي إلى نحو 600,000 سطر لثنائيات يبلغ طولها الوسيط 18,000 تعليمة RISC-V. وأنجز الفريق العمل في أسابيع قليلة، مقارنة بنظام seL4 الذي استغرق تنفيذه سنتي عمل بشري وتحققه الرسمي 20 سنة عمل.
• الافتراضات: تنطبق البراهين على ثنائيات ساكنة أحادية الخيط تعمل على معالج RISC-V ونظام لينكس بميزانية ذاكرة ثابتة. واعتمد الفريق اختبارات التشويش في مشاريع OSS-Fuzz مواصفات رسمية، أي أن الاختبار لا ينهار أبداً لأي مدخل تحت 64 ميغابايت، ويتحقق مدقق Rocq من كل برهان.
• الثغرات المكتشفة: عثر كلود على مئات الأخطاء، منها تجاوز عدّاد في أداة فك ضغط يُستثار بمدخلات نحو 20 ميغابايت، وقراءة خارج الحدود في مفكك صور تحتاج مدخلاً بحجم 64 ميغابايت وأكثر من 2 غيغابايت من الذاكرة، وإعادة اكتشاف الثغرة CVE-2026-56132 في مكتبة libexpat.
• أخطاء منطقية: رصد النموذج أخطاء لا تسبب انهياراً، بينها ميزة تقييد تحميل الملفات لا تُطبَّق دائماً، وخطأ منطقي ظل كامناً أكثر من عقد في تطبيقات حرجة واسعة الاستخدام. وفي قارئ PDF شائع وجد كلود خلال أسبوع واحد عدداً من الثغرات الأمنية يوازي ما يُبلَّغ عنه عادة في سنة.
• تجارب إضافية: أثبت كلود أن تطبيق zlib في نواة لينكس يطابق مواصفة RFC 1950 على مستوى ثنائيات x86، وكرر ذلك لنحو ست مكتبات أخرى. كما بنى مفسّراً لمجموعة فرعية كبيرة من بايثون بلغة Rust وتحقق منه بأداة Verus، فطابق سلوك CPython في 99.95% من 1.7 مليون برنامج عشوائي.
• الكفاءة: في 36 مهمة تحقق صغيرة مشتقة من OSS-Fuzz أثبت Opus 5.5 نصفها مستهلكاً نحو 40% رموزاً أقل من Opus 5، مع ثلاث محاولات لكل مهمة بميزانية 5 ملايين رمز. واحتاج الوكلاء الذين يتشاركون مساحة عمل واحدة إلى رموز أقل بنسبة 17% مقارنة بالوكلاء المنفردين.
• الحدود: شددت أنثروبيك على أن التحقق الرسمي لا يعني خلو البرمجيات من الأخطاء؛ فالآلات الحقيقية تعمل بمعماريتي x86 وARM مع ربط ديناميكي بمكتبة glibc بخلاف النموذج المدروس، وأداة AddressSanitizer لا تكشف كل أخطاء سلامة الذاكرة، وقد يتطلب البرهان الواحد مئات ملايين الرموز.
• الإتاحة: نُشرت مجموعة فرعية من البراهين ودلالات RISC-V ولينكس على GitHub، وتعرض Theorem تشغيل خط العمل نفسه لمشاريع مفتوحة المصدر أخرى عبر برنامج OSS Verify مع مهارة لكلود تساعد المطورين على التحقق من شيفرتهم، فيما تُحجب البراهين التي قد تكشف ثغرات لم تُرقَّع بعد.
• ضد التحايل: لمنع النموذج من ترقيع الشيفرة هرباً من صعوبة البرهان، عاقبت أنثروبيك الترقيعات في نظام الحوافز، وسجّلتها وراجعتها، ومنحت رصيداً إضافياً لإثبات المدخلات التي يغيّرها كل ترقيع، ونشرت مع النتائج مواصفات الاختبارات التي تعذر إثباتها.

ماذا بعد؟

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