تعاني معظم البرمجيات من أخطاء كثيرة، ويستطيع الذكاء الاصطناعي اليوم اكتشافها واستغلالها بسهولة. لم تعد الدفاعات التقليدية ضد الهجمات الإلكترونية كافية، لذا يحتاج المطورون إلى طرق تثبت خلو الشيفرة من الأخطاء. يمكن للتحقق الرسمي من البرمجيات أن يوفر هذا الضمان، لكنه تاريخيًا تطلّب سنوات من الجهد المتخصص، مما جعله غير عملي لمعظم المشاريع الواقعية.
في تعاون مع Theorem، يبيّن الباحثون أن هذا الوضع يتغير. فنماذج اللغة الكبيرة قادرة الآن على إنتاج براهين رسمية على نطاق واسع، مما يتيح مسارات تطوير جديدة تتضمن ضمانات أمنية مُثبتة. وباستخدام Claude، أثبت الفريق خصائص أمنية على مستوى لغة التجميع (RISC-V) عبر أكثر من 100 مكتبة برمجية مفتوحة المصدر في الاستخدام الفعلي. وبحسب علمهم، فهذه أول جهد واسع النطاق يستخدم الذكاء الاصطناعي لتطبيق التحقق الرسمي على برمجيات الإنتاج عند هذا المستوى. وأثناء كتابة البراهين، كشف Claude أيضًا أخطاء ظلت بعيدة عن الاكتشاف لسنوات رغم تريليونات مرات التشغيل الاختباري.
يبني النهج على طريقة قديمة: يحوّل المطورون الشيفرة إلى نموذج رياضي ويحاولون إثبات أنها تتبع دائمًا قواعد الأمان المحددة. وتشير البراهين الفاشلة إلى أخطاء محتملة. وتقليديًا، قد تكون البراهين أكبر بكثير من الشيفرة الأصلية، وتتطلب مهارات نادرة ومتخصصة. فقد استغرق بناء نواة seL4 عامين من العمل البشري، أما التحقق منها فاستغرق 20 عامًا.
ولاختبار النهج، أثبت Claude أن 123 برنامجًا مفتوح المصدر ستنتهي دائمًا بشكل طبيعي دون أخطاء في أمان الذاكرة أو فشل في التأكيدات، لكل مدخل أقل من 64 ميغابايت، وذلك تحت افتراضات معلنة حول بيئة التشغيل. ويقر الباحثون بأن هذا بعيد عن إصلاح كل الأخطاء الممكنة، لكنهم يقولون إنه يقدم خارطة طريق. وقد نُشر جزء من البراهين ليتمكن الآخرون من التحقق منها وإعادة استخدامها.
المصدر: Hacker News · لخّصه HeadlinesBriefing