تقول Anthropic إن Claude أثبت خصائص الأمان في 123 مكتبة

نشرت Anthropic بحثًا في 22 أكتوبر 2026، أفادت فيه بأن Claude أعدّ براهين رسمية مدققة آليًا لخصائص الأمان على مستوى شيفرة التجميع RISC-V، شملت 239 نقطة دخول لاختبارات التشويش عبر 123 مكتبة مفتوحة المصدر، وذلك بالتعاون مع Theorem.

وفقًا لـ Anthropic، أصلح Claude الأخطاء التي عثر عليها، ثم أثبت أن البرامج ستنتهي دائمًا على نحو طبيعي من دون التسبب في أخطاء تتعلق بسلامة الذاكرة أو إخفاق التأكيدات، مع كل مدخل يقل حجمه عن 64 MB، ومع كل استجابة ممكنة لنظام التشغيل Linux وتخطيط للذاكرة ضمن النموذج. تفترض البراهين أن البرنامج يعمل بوصفه ملفًا ثنائيًا ثابتًا أحادي الخيط، بميزانية ذاكرة محددة، على وحدة معالجة مركزية RISC-V تستخدم Linux. وقالت Anthropic إن البراهين تتألف من نحو 180 مليون سطر من Rocq، وإن البرهان المعتاد يمتد إلى نحو 600,000 سطر لتغطية ملفات ثنائية يبلغ طولها الوسيط 18,000 تعليمة RISC-V. وقالت الشركة إن هذه، على حد علمها، أول محاولة واسعة النطاق لاستخدام الذكاء الاصطناعي لتطبيق التحقق الرسمي على برمجيات الإنتاج على مستوى شيفرة التجميع.

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

تحويل اختبارات التشويش إلى براهين رسمية

تحوّل هذه المنهجية اختبار التشويش القابل للترجمة البرمجية الموجود في كل مكتبة إلى مواصفة رسمية تجسّد قاعدة واحدة: لا يتعطل الاختبار مع أي مدخل يقل حجمه عن 64 MB. وتُعرَّف المواصفة على تعليمات RISC-V المترجمة، باستخدام الدلالات الرسمية التي وضعتها Theorem لمجموعة تعليمات RISC-V وعمليات Linux، فيما يتحقق مدقّق البراهين Rocq من مطابقة كل برهان مكتمل للمواصفة. وتقول Anthropic إن هذا لا يترك للمطورين سوى ثلاثة مكونات عليهم الوثوق بها: النماذج الرسمية لـ RISC-V وعمليات Linux، ونصوص المبرهنات الدقيقة، ومدقّق Rocq نفسه.

قالت Anthropic إنها طبّقت هذه العملية على مئات المشاريع ضمن مبادرة OSS-Fuzz التابعة لـ Google، التي توفر اختبارات تشويش مستمرة للمشاريع المؤهلة مفتوحة المصدر، وتضيف تلقائيًا أدوات إلى برامج C وC++ باستخدام AddressSanitizer، وهي أداة تتسبب في تعطل البرنامج كلما جرى الوصول إلى الذاكرة بطريقة غير سليمة. ويعرض ملحق مؤرخ في 22 أكتوبر 2026 المبرهنة الكاملة التي أُثبتت: مع كل المدخلات التي يقل حجمها عن 64 MiB وكل تخطيطات الذاكرة، لا يتعطل الملف الثنائي المزود بأدوات ASan ولا الملف الثنائي العادي، ولا يتوقف أي منهما قسرًا أو يُظهر سلوكًا غير مشمول بالنموذج؛ كما ينتج كلاهما آثار قراءة وكتابة متطابقة، وسلوكًا متطابقًا عند الخروج، وحالة نهائية متطابقة لنظام الملفات.

يذكر الملحق أن Claude كتب نحو مليار سطر من Rocq خلال العمل، اجتاز نحو 180 مليونًا منها مدقّق البراهين؛ إذ حصلت نقطة الدخول إلى المحلّل، المؤلفة من 391 سطرًا، في cJSON على برهان من 630,000 سطر، بينما حصلت fftw3، التي رُبط بها 51,000 سطر، على برهان من 480,000 سطر. ولأن Claude سُمح له بإصلاح الشيفرة قبل إكمال البرهان، قالت Anthropic إنها فرضت عقوبات على الإصلاحات، ومنحت نقاطًا إضافية لإثبات المدخلات التي غيّرها الإصلاح، وسجلت الإصلاحات ودققتها للحد من التلاعب بنظام المكافآت.

أخطاء كُشفت أثناء محاولات الإثبات

أفادت Anthropic بأن محاولات إجراء البراهين كشفت مئات الأخطاء، كان من المستبعد أن تعثر اختبارات التشويش على كثير منها. ففي أثناء إثبات نقطة الدخول إلى إحدى المكتبات، عثر Claude على نقص في قيمة عدّاد داخل أداة لفك الضغط أدى إلى كتابة خارج حدود الذاكرة، لكن ذلك لم يحدث إلا مع مدخلات يبلغ حجمها نحو 20 MB، وبترتيب نادر ومحدد. وشملت الاكتشافات الأخرى قراءة خارج حدود الذاكرة في وحدة فك ترميز الصور، استلزمت مدخلًا بحجم 64 MB وأكثر من 2 GB من الذاكرة؛ وقراءة خارج حدود الذاكرة تتطلب تسلسلًا معينًا من الاستدعاءات عبر مقبضين للملف نفسه؛ وإعادة اكتشاف الثغرة CVE-2026-56132 في libexpat، التي تتطلب مدخلًا متداخلًا بعمق.

كما عثر Claude على أخطاء منطقية لا تؤدي إلى تعطل البرنامج، منها عدم تطبيق قيد يحدد الملفات التي يمكن للتطبيق تحميلها في جميع الحالات. وقالت Anthropic إن محاولات التحقق من عدة تطبيقات أساسية واسعة الاستخدام كشفت خطأً منطقيًا لم يكن معروفًا من قبل وظل كامنًا لأكثر من عقد، وإنها عثرت، خلال محاولة للتحقق من قارئ PDF واسع الاستخدام، على عدد من أخطاء الأمان في أسبوع واحد يعادل عادةً ما يُبلّغ عنه خلال عام.

تجارب إضافية ونتائج تتعلق بالكفاءة

إلى جانب OSS-Fuzz، طلبت Anthropic من Claude كتابة مواصفة رسمية للوثيقة RFC 1950، وهي وثيقة تقنية تحدد تنسيق ضغط zlib، ثم إثبات أن تطبيق zlib في نواة Linux ينفذها على نحو صحيح. وأثبت Claude صحة الملف الثنائي المترجم لـ x86 مباشرةً، باستخدام دلالات رسمية لمجموعة تعليمات x86 أنشأها Claude، وقالت Anthropic إنها كررت العملية مع ست مكتبات أخرى واسعة الاستخدام، فعثرت على أخطاء طفيفة في حالات طرفية لا يمكن استغلالها، ويجري الإبلاغ عنها للمشروعات المعنية. وأفادت الشركة أيضًا بأن إنشاء دلالات x86 كشف مئات الأخطاء في الوثائق المرجعية الرسمية وعددًا أقل من الأخطاء في العتاد نفسه، وأن تنفيذ الدلالات خطوةً خطوةً يمكنه إقلاع بيئة مستخدم Ubuntu على نواة Linux.

في تجربة أخرى، أنشأ Claude مفسّرًا لجزء كبير من لغة Python باستخدام Rust، وأثبت بأداة التحقق Verus أنه يلتزم بدلالات CPython الموضحة في ورقة أكاديمية. وينص الملحق التقني على إثبات المستويات الـ17 جميعها في المفسّر، مع صحة المبرهنة القائلة: «كلما أعاد المفسّر نتيجة، كانت تلك هي النتيجة التي تحددها الدلالات الشكلية». وقالت Anthropic إن الاختبارات التجريبية على 1.7 مليون برنامج Python مولّد عشوائيًا أظهرت تطابق السلوك مع CPython في 99.95% من الاختبارات؛ ومن بين سبعة أخطاء أُدخلت عمدًا، اجتازت خمسةٌ الاختبارات العشوائية، في حين أخلّت الأخطاء السبعة جميعها بالإثبات.

لقياس الكفاءة، أنشأت Anthropic 36 مهمة تحقق صغيرة عن طريق تقليص نقاط الدخول الفعلية في OSS-Fuzz، ما أفضى إلى برامج تضم من 283 إلى 2,491 تعليمة، مع حصر المدخلات في 64 بايتًا واستبدال AddressSanitizer ببيئة تشغيل «mini-ASan» تضم نحو 100 تعليمة. وتفيد Anthropic بأن Opus 5.5 يثبت نصف المهام باستخدام رموز أقل بنحو 40% مقارنةً بـ Opus 5. وتفيد Anthropic أيضًا بأن الوكلاء الذين سُمح لهم بنسخ براهين بعضهم بعضًا في مساحة عمل مشتركة احتاجوا إلى رموز أقل بنسبة 17% من الوكلاء الذين عملوا بمفردهم، وأن بعضهم نجح بعد أن أخفق سابقًا في العمل منفردًا، وأن الوكلاء الذين عملوا بمفردهم لم يتمكنوا من إكمال اثنين من البراهين. وقالت الشركة إن أثر إعادة الاستخدام نفسه ظهر على نطاق واسع خلال جهود OSS-Fuzz، إذ نسخت فرق الوكلاء البراهين المكتملة وعدّلتها، لأن جزءًا كبيرًا من كل برهان يتناول شيفرة وقت التشغيل المشتركة في C وشيفرة تهيئة AddressSanitizer.

القيود المعلنة وبرنامج OSS Verify

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

تتيح Theorem خط المعالجة نفسه مجانًا لمشروعات المصادر المفتوحة المؤهلة عبر برنامجها OSS Verify. ويجري التسجيل عبر طلب دمج يضيف ملفات project.yaml وDockerfile وbuild.sh إلى مستودع البرنامج، وتقول Theorem إنها تراجع المشروعات وفق معايير مشابهة لتلك المتبعة في OSS-Fuzz، مع إعطاء الأولوية للبنية التحتية الحيوية واسعة الاستخدام. ووفقًا لـ Theorem، يتلقى القائمون على صيانة المشروعات برهانًا من Rocq، يتحقق منه Rocq kernel، يثبت أن كل هدف اختبار ضبابي لا يتعطل عند تلقي أي مدخل يصل حجمه إلى 64 MiB؛ وتُبلّغ الشركة القائمين على الصيانة سرًا بالبريد الإلكتروني عن الأخطاء المكتشفة أثناء جهود الإثبات، من دون تحديد موعد للإفصاح عنها، وقد يستغرق إعداد البراهين عدة أيام. وتهدف خارطة طريق Theorem إلى التحقق من منظومة Nix بأكملها، بما يشمل البنية التحتية الحيوية مثل glibc وOpenSSL وcURL.