عرضت شركة أنثروبيك نتائج تجارب استخدمت نماذج الذكاء الاصطناعي للتحقق رسميًا من موثوقية وأمان المشاريع القائمة. خلال التجربة، استُخدمت نماذج الذكاء الاصطناعي لإنشاء براهين رياضية تثبت خلو 123 مكتبة مفتوحة المصدر من أخطاء الذاكرة، والتي تم اختبارها في بنية OSS Fuzz التحتية.
أُجري التحقق على مستوى كود التجميع المُترجم لبنية RISC-V. بلغ إجمالي حجم البراهين المُولَّدة حوالي 180 مليون سطر من التعليمات البرمجية لنظام التحقق Rocq Prover (حوالي 600 سطر لكل ملف ثنائي يحتوي على 18 تعليمة RISC-V). تم توليد البراهين عن طريق التحويل التلقائي لاختبارات التشويه الموجودة إلى مواصفات رسمية، وبعد ذلك أثبت نموذج Claude AI أن البرنامج خالٍ من الأخطاء لأي بيانات إدخال تصل إلى 64 ميجابايت.
خلال عملية بناء البرهان، تمكن نموذج الذكاء الاصطناعي من تحديد مئات الأخطاء البرمجية التي لم يتم اكتشافها سابقًا بواسطة اختبارات الفحص العشوائي، وإعداد حلول لها. وشملت هذه الأخطاء، من بين أمور أخرى، ثغرات تجاوز سعة المخزن المؤقت عند معالجة بيانات إدخال معينة (مثل CVE-2026-56132 في مكتبة libexpat)، بالإضافة إلى أخطاء منطقية. علاوة على ذلك، استُخدم نموذج الذكاء الاصطناعي لإثبات توافق تطبيق نواة النظام لخوارزمية zlib. Linux مواصفات RFC 1950.
تم أيضًا إنشاء مترجم لمجموعة فرعية من لغة بايثون باستخدام لغة رست، حيث تم إعداد برهان رسمي لمطابقته مع دلالات CPython باستخدام مجموعة أدوات Verus. وللمقارنة بين سلوكه وسلوك CPython، تم تنفيذ أكثر من 1.7 مليون برنامج بايثون تم إنشاؤها عشوائيًا. في 99.95% من الحالات، تطابقت نتائج تنفيذ هذه البرامج في التطبيق الجديد وفي CPython، وكانت أي اختلافات تم العثور عليها حالات نادرة معروفة.
يضمن التحقق الرسمي الامتثال للمواصفات، ولكنه لا يقضي تمامًا على المشكلات الأمنية، إذ تبقى المخاطر الناجمة عن مشكلات تعدد الخيوط، والربط الديناميكي، والسلوك الشاذ على الأجهزة الحقيقية غير موثقة رسميًا. ومن أهم مزايا النهج المقترح أنه يعمل مباشرةً مع الملفات الثنائية، مما يُغني عن إعادة كتابة التعليمات البرمجية الموجودة بلغات قابلة للتحقق الرسمي.
المصدر: opennet.ru
