أعلنت شركة أنثروبيك أن نموذج الذكاء الاصطناعي كلود نجح في كتابة براهين رياضية مدققة آلياً تثبت أن الشيفرات البرمجية المترجمة لنحو 123 مكتبة مفتوحة المصدر لا يمكن أن تنهار ضمن شروط محددة، مكتشفاً مئات الثغرات البرمجية التي استعصت على تريليونات الاختبارات التقليدية لسنوات طويلة.
- إنجاز غير مسبوق في التحقق الصوري على مستوى لغة التجميع
- من اختبارات التشويش العشوائي إلى البراهين الرياضية بلغة روك
- اكتشاف مئات الثغرات التي أخطأتها أدوات الفحص التقليدية
- حدود الضمانات الأمنية وتغير اقتصاديات هندسة البرمجيات
- أسئلة شائعة
إنجاز غير مسبوق في التحقق الصوري على مستوى لغة التجميع
أعلنت شركة «أنثروبيك» المتخصصة في تطوير تقنيات الذكاء الاصطناعي أن نموذجها اللغوي «كلود» تمكن من صياغة وكتابة براهين رياضية مدققة آلياً تثبت بصورة قاطعة أن الشيفرات البرمجية المترجمة والمنتمية إلى 123 مكتبة برمجية مفتوحة المصدر لا يمكن أن تتعرض للانهيار أو التوقف المفاجئ تحت شروط تشغيلية محددة بدقة. وإلى جانب إثبات الموثوقية البرمجية، نجح النموذج أثناء إعداد هذه البراهين في رصد واكتشاف ثغرات وأخطاء برمجية عميقة ظلت مختبئة لسنوات طويلة دون أن ينتبه إليها أحد، وذلك على الرغم من إخضاع تلك المكتبات لتريليونات من عمليات التشغيل والاختبار الآلي المتواصل.
وجاءت هذه النتائج في بحث علمي وتقني نشرته الشركة في 22 أكتوبر، وأعده «فريق الاختراق الحدودي» التابع لشركة «أنثروبيك» بالتعاون الوثيق مع شركة «ثيورم» المتخصصة في الأساليب الرياضية الصورية. ووصفت «أنثروبيك» هذا المشروع بأنه ما تعتقد أنه «أول جهد واسع النطاق لاستخدام الذكاء الاصطناعي في تطبيق التحقق الصوري على برمجيات الإنتاج الفعلية عند مستوى شيفرة التجميع». وأوضحت الشركة في ورقتها البحثية أن أنظمة الذكاء الاصطناعي أصبحت اليوم قادرة على إيجاد الثغرات البرمجية واستغلالها بسهولة فائقة، ولذلك لم يعد الاعتماد على اختبارات البرمجيات التقليدية وحده كافياً للدفاع عن الأنظمة وحمايتها من الهجمات السيبرانية المتقدمة.
من اختبارات التشويش العشوائي إلى البراهين الرياضية بلغة روك
انطلق الفريق البحثي في مهمته من اختبارات الفحص العشوائي المعروفة باسم اختبارات التشويش والمستمدة من برنامج «أو إس إس فاز» التابع لشركة «جوجل»، حيث قام الباحثون بتحويل كل اختبار منها إلى مواصفة رياضية صورية دقيقة. ونصت القاعدة الصارمة المعتمدة في هذه المواصفات على ضمان عدم انهيار الاختبار مطلقاً عند التعامل مع أي مدخلات بيانات يقل حجمها عن 64 ميغابايت، وذلك بعد ترجمة الشيفرة البرمجية إلى لغة الآلة الخاصة بمعمارية المعالجات المفتوحة «ريسك فايف».
وعلى مدار بضعة أسابيع من العمل المتواصل، نجح نموذج «كلود» في إثبات هذه القاعدة الصارمة لنحو 239 نقطة إدخال برمجية موزعة عبر 123 مكتبة مفتوحة المصدر. ووفقاً لبيانات «أنثروبيك»، يصل إجمالي حجم هذه البراهين الرياضية المجتمعة إلى نحو 180 مليون سطر برمجي مكتوب بلغة الإثبات الرياضي «روك»، في حين يبلغ طول البرهان النموذجي الواحد قرابة 600000 سطر من الشيفرات. وأفاد موقع «إنترستينغ إنجينيرينغ» الإخباري بأن مدقق البراهين في لغة «روك» يتولى التحقق آلياً من مطابقة كل برهان لمواصفاته الرياضية، مما يعفي المطورين البشريين من الحاجة إلى مراجعة ملايين الأسطر المولدة سطراً بسطر.
وأكدت «أنثروبيك» أنها تعمل حالياً على نشر مجموعة فرعية من هذه البراهين للجمهور، جنباً إلى جنب مع النماذج الدلالية الخاصة بمعمارية «ريسك فايف» ونظام التشغيل «لينكس» التي استندت إليها تلك الإثباتات. وفي السياق ذاته، أورد موقع «يونايت أي آي» أن شركة «ثيورم» تعرض تشغيل خط المعالجة والتحقق ذاته لصالح مشاريع البرمجيات مفتوحة المصدر المؤهلة مجاناً بالكامل من خلال برنامجها الجديد المسمى «أو إس إس فيريفاي»، كما أطلقت الشركة مهارة مخصصة داخل نموذج «كلود» لمساعدة المشرفين على تطوير المكتبات البرمجية في التسجيل والانضمام إلى البرنامج بسهولة.
اكتشاف مئات الثغرات التي أخطأتها أدوات الفحص التقليدية
أثناء عملية صياغة وكتابة البراهين الرياضية، كشف «كلود» عن مئات الأخطاء والثغرات البرمجية الخفية، حيث بادر النموذج إلى كتابة ترقيعات برمجية لإصلاحها أولاً قبل أن يشرع في إثبات سلامة الشيفرة المعدلة رياضياً. ومن بين الحالات اللافتة التي وثقها البحث، عثر النموذج في إحدى أدوات فك ضغط البيانات على خطأ ناتج عن تجاوز الحد الأدنى للعداد الرقمي، وهو ما كان يؤدي إلى كتابة بيانات خارج حدود الذاكرة المسموح بها، غير أن هذا الخلل لم يكن ليظهر إلا عند إدخال ملفات يبلغ حجمها نحو 20 ميغابايت وتصادف امتلاكها لتخطيط هيكلي نادر للغاية.
وفي حالة ثانية داخل برنامج لفك ترميز الصور، رصد النموذج ثغرة قراءة خارج حدود الذاكرة، لكن تفعيلها كان يتطلب مدخلات بحجم 64 ميغابايت واستهلاك أكثر من 2 غيغابايت من الذاكرة العشوائية، وهو ما يفسر عجز أدوات الفحص التقليدية عن التقاطها. كما أعاد «كلود» اكتشاف ثغرة أمنية معروفة في مكتبة «ليب إكسبات» الشهيرة، وتوصل كذلك إلى خلل منطقي خطير كانت فيه إحدى الميزات المصممة لتقييد الملفات المسموح للتطبيق بتحميلها تتعطل ولا يتم فرضها وتطبيقها في جميع الحالات، بحسب ما أوردته الورقة البحثية.
حدود الضمانات الأمنية وتغير اقتصاديات هندسة البرمجيات
وعلى الرغم من أهمية هذا الاختراق التقني، نبهت شركة «أنثروبيك» بوضوح إلى أن هذه البراهين الرياضية لا تعني أن المكتبات البرمجية التي شملتها الدراسة أصبحت خالية تماماً من جميع الأخطاء المحتملة في كل الظروف. إذ تفترض البراهين المنجزة وجود ملف تنفيذي ثابت أحادي الخيط يعمل ضمن ميزانية ذاكرة محددة مسبقاً على معالج مركزي بمعمارية «ريسك فايف» تحت بيئة نظام التشغيل «لينكس».
وأوضحت الشركة في تقريرها أن أي أخطاء برمجية متبقية إما أن تكون واقعة خارج النطاق المحدد لهذه البراهين، وإما أن تكون كامنة في المكونات الموثوقة التي اعتمدت عليها الدراسة، ويقصد بذلك النماذج الرياضية للعتاد الصلب ونظام التشغيل، وصياغة النظريات نفسها، وأداة التدقيق الخاصة بلغة «روك» ذاتها. وأشار موقع «إنترستينغ إنجينيرينغ» إلى أن الغالبية العظمى من الأنظمة البرمجية المنشورة فعلياً في العالم الحقيقي تعتمد على معماريات معالجات أخرى أو إعدادات تشغيلية متعددة الخيوط تختلف عن البيئة الافتراضية للبحث.
ومع ذلك، ترى «أنثروبيك» أن الجدوى الاقتصادية للتحقق البرمجي الصوري تشهد تحولاً جذرياً بفضل الذكاء الاصطناعي. وكتب الفريق البحثي في ختام تقريره رسالة مباشرة للمبرمجين جاء فيها: «نحن نشجع جميع المطورين على استكشاف التحقق الصوري باستخدام النماذج اللغوية الكبيرة، ولا سيما أولئك الذين جربوا هذا النهج سابقاً مع نماذج أقل كفاءة ووجدوا أنه لم ينجح حينها».
أسئلة شائعة
السؤال: ماذا أثبت نموذج كلود في البحث الجديد لشركة أنثروبيك؟
الإجابة: نجح نموذج كلود في كتابة براهين رياضية مدققة آلياً تثبت أن الشيفرات البرمجية المترجمة لنحو 123 مكتبة مفتوحة المصدر لا يمكن أن تنهار عند معالجة مدخلات يقل حجمها عن 64 ميغابايت ضمن بيئة محددة.
السؤال: ما حجم البراهين الرياضية التي كتبها نموذج كلود؟
الإجابة: بلغ إجمالي حجم البراهين نحو 180 مليون سطر برمجي مكتوب بلغة روك عبر 239 نقطة إدخال، بمتوسط يقارب 600000 سطر للبرهان الواحد.
السؤال: كيف ساعدت عملية التحقق الصوري في كشف ثغرات جديدة؟
الإجابة: أثناء محاولة إثبات سلامة الشيفرات، اكتشف كلود مئات الثغرات المعقدة التي أخطأتها اختبارات التشويش لسنوات، مثل ثغرات تجاوز حدود الذاكرة في برامج فك الضغط وفك ترميز الصور ومكتبة ليب إكسبات، وقام بترقيعها قبل إثبات صحتها.
السؤال: ما هي القيود التقنية للضمانات التي تقدمها هذه البراهين؟
الإجابة: تفترض البراهين تشغيل ملف تنفيذي ثابت أحادي الخيط بميزانية ذاكرة محددة على معالج بمعمارية ريسك فايف ونظام لينكس، ولا تغطي الأخطاء الخارجة عن هذا النطاق أو الكامنة في نماذج العتاد ومدقق لغة روك نفسه.
