التحقق الشكلي مع Claude: براهين لـ 123 مكتبة مفتوحة المصدر

في 22 أكتوبر نشر فريق Frontier Red Team في Anthropic بالتعاون مع شركة Theorem دراسةً كتب فيها Claude براهين أمان شكلية لـ 123 مكتبة مفتوحة المصدر من مشروع OSS-Fuzz. وتتعلق البراهين بشيفرة RISC-V المُصرَّفة، لا بالشيفرة المصدرية. وبحسب المؤلفين، هذا أول تحقق شكلي بهذا الحجم من برمجيات إنتاجية على مستوى لغة التجميع باستخدام الذكاء الاصطناعي.

كيف يعمل التحقق الشكلي مع Claude؟

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

خط المعالجة في الدراسة كالتالي:

1. نقطة الانطلاق هي اختبارات الـ fuzzing الموجودة في OSS-Fuzz (مشروع من Google يغمر المكتبات باستمرار ببيانات عشوائية).
2. تُصرَّف المكتبة مع الاختبار إلى ملف تنفيذي لـ RISC-V.
3. من دلالات (semantics) معالج RISC-V وعملية Linux التي أعدّتها Theorem تُولَّد مواصفات تلقائيًا: يجب أن ينتهي البرنامج دائمًا بشكل طبيعي، دون أخطاء ذاكرة ودون فشل في التأكيدات (assertions).
4. يكتب Claude البرهان، ويؤكد مدقق البراهين Rocq أن البرهان يستوفي المواصفات.
5. عندما يصادف Claude خطأً، يصلح الشيفرة، وتُولَّد المواصفات من جديد ويُبنى البرهان من البداية.

يشمل الضمان كل مُدخل أصغر من 64 ميغابايت، وكل استجابة نظام وترتيب ذاكرة ضمن النموذج (على افتراض برنامج ثابت الربط أحادي الخيط على RISC-V وLinux).

ما الأرقام التي قدّمتها Anthropic؟

1. 239 نقطة دخول في 123 مكتبة.
2. نحو 180 مليون سطر من البراهين بلغة Rocq إجمالًا؛ البرهان النموذجي يقارب 600 ألف سطر ويتعلق ببرنامج يبلغ وسيط عدد تعليماته 18 ألف تعليمة RISC-V.
3. استغرق العمل كله بضعة أسابيع.
4. في 36 مهمة صغيرة، برهن Opus 5.5 على نصفها مستهلكًا أقل بنحو 40% من التوكنات مقارنةً بـ Opus 5، واستهلك الوكلاء العاملون في مساحة مشتركة أقل بنسبة 17% مما لو عمل كل منهم منفردًا.

والطريف أن برهان cpp-httplib تطلّب إثبات أن الشجرة الحمراء-السوداء في libc++ ذات عمق محدود لوغاريتميًا، لأن تلك كانت الطريقة الوحيدة لاستبعاد طفح المكدس (stack overflow) في مُهدِّم std::set.

ما الأخطاء التي عثر عليها Claude؟

بحسب المؤلفين، كشفت العملية مئات الأخطاء التي صمدت أمام سنوات من الـ fuzzing. أمثلة من المنشور:

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

إضافةً إلى ذلك، ثلاث تجارب أخرى. كتب Claude مواصفات شكلية لـ RFC 1950 وبرهن على ملفات x86 الثنائية أن zlib في نواة Linux ينفّذها تنفيذًا صحيحًا. وبنى أيضًا بلغة Rust مفسّرًا لمجموعة فرعية من Python تصرّف مثل CPython في 99.95% من 1.7 مليون برنامج عشوائي. أما محاولة التحقق من قارئ PDF شائع فقد عثرت في أسبوع على عدد من الثغرات الأمنية يعادل ما يُبلَّغ عنه عادةً في عام.

إنه الاتجاه نفسه الذي رأيناه في PHP2Shell وClaude Mythos في Bank of America: نماذج الذكاء الاصطناعي تجد أخطاءً غفل عنها البشر والأدوات التقليدية لسنوات. لكن الأمر هذه المرة لا ينتهي برقعة إصلاح فحسب، بل ببرهان.

ما الذي ينبغي الانتباه إليه؟

أولًا، إلى معنى «مُتحقَّق منه». يكتب المؤلفون صراحةً أن التحقق الشكلي لا يعني شيفرة خالية من الأخطاء (بالنص الأصلي «»Formally verified« does not mean »bug-free.«»). فالبرهان لا يكون أفضل من المواصفات، ومن نموذجي RISC-V وLinux، ومن مدقق Rocq نفسه.

ثانيًا، إلى النطاق. تتعلق البراهين بملفات RISC-V ثنائية ثابتة الربط وأحادية الخيط مع musl، بينما يشغّل معظمنا الشيفرة على x86 أو ARM مع glibc. كما أنها لا تشمل الشيفرة الميتة، ولا الحالات التي يكون فيها البرنامج المستدعي للمكتبة هو من يُفسد الذاكرة.

ثالثًا، إلى التكلفة. قد تستهلك براهين منفردة مئات الملايين من التوكنات، وهو ما يعدّه المؤلفون أنفسهم القيد الرئيسي.

جزء من البراهين متاح بالفعل على GitHub (oss-verify-proofs)، مع دلالات RISC-V وLinux. أما الباقي فينتظر، لأنه قد يكشف أخطاءً لم تُصلَح بعد.

الأسئلة الشائعة

ما هو التحقق الشكلي؟

برهان رياضي يتحقق منه برنامج، على أن الشيفرة تتمتع بخاصية معيّنة مع جميع المدخلات، مثل أنها لا تكتب أبدًا خارج حدود المخزن المؤقت. أما الاختبارات والـ fuzzing فتفحص حالات مختارة فقط.

هل المكتبات المُتحقَّق منها خالية من الأخطاء؟

لا. يضمن البرهان غياب الأعطال فقط ضمن النموذج الموصوف (RISC-V، Linux، مُدخل أصغر من 64 ميغابايت، خيط واحد). وقد تكمن الأخطاء في المواصفات، أو في نموذج الآلة، أو خارج هذا النطاق.

هل يمكنني التحقق من مشروعي؟

تدير Theorem برنامج OSS Verify، وهو برنامج مجاني لمشاريع مفتوحة المصدر مختارة. يتقدم به مشرف المشروع عبر pull request يتضمن الملفات project.yaml وDockerfile وbuild.sh، على نحو مشابه لـ OSS-Fuzz. ويجب الاستعداد لنقل عملية البناء إلى ملفات riscv64 ثنائية ثابتة الربط.