ثغرة “فيض ذاكرة” تضرب قلب Lean 4 وتكشف هشاشة البرمجيات “المثبتة صحتها”
سقوط الضمانات الرياضية أمام اختبارات الذاكرة العملية
105 ملايين عملية فحص عشوائي (Fuzzing) كانت كافية لإسقاط هيبة البرمجيات التي توصف بأنها “موثقة رسمياً”. البداية كانت من محاولة فحص تنفيذ لغة Lean لتطبيق zlib، والنتيجة غير المتوقعة: ثغرة “فيض ذاكرة” (Heap buffer overflow) في محرك التشغيل الخاص بلغة Lean 4 نفسها، وهو خلل يطال كافة إصدارات اللغة حتى اللحظة.
المشروع الذي نُفذ عبر 10 وكلاء ذكاء اصطناعي قاموا ببناء وإثبات صحة تطبيق lean-zip بالكامل، واجه اختباراً حقيقياً أمام أدوات فحص تقليدية مثل AFL++ وAddressSanitizer. ليوناردو دي مورا، المهندس الرئيسي في Lean FRO، كان قد روج لهذا العمل كإنجاز يضمن خلو البرنامج من أخطاء التنفيذ، لكن الواقع كشف فجوة تقنية عميقة بين “صحة الكود المنطقية” و”سلامة المحرك” الذي يدير الذاكرة.
“أي مصفوفة بايتات أقل من 1 جيجابايت، ستتم معالجتها بشكل صحيح تماماً”؛ هذا ما تنص عليه النظرية الرياضية المدمجة داخل الكود. الناحية النظرية تؤكد أن دالة فك الضغط هي المعكوس الدقيق لعملية الضغط، والضمانات هنا تبدو نهائية من وجهة نظر رياضية بحتة، إلا أن الفحص العملي وجد ثغرة في وظيفة lean_alloc_sarray تسببت في انهيار نظام تخصيص الذاكرة.
نتائج الفحص المكثف الذي استمر طوال عطلة نهاية الأسبوع جاءت متباينة؛ لم تُسجل أي ثغرات ذاكرة في كود Lean الذي تم التحقق منه برمجياً، لكن الهجوم نجح في اختراق “الرن تايم” (Runtime) الخاص باللغة، بالإضافة إلى رصد هجمة “حرمان من الخدمة” (DoS) استهدفت محلل الأرشيف في lean-zip، وهو جزء من الكود لم يخضع أصلاً لعملية التحقق الرسمي.
قدرات الذكاء الاصطناعي في اكتشاف الثغرات باتت تثير قلق الشركات الكبرى بشكل فعلي، حيث ترددت شركة “أنثروبيك” (Anthropic) في إطلاق نموذجها “Mythos” واصفة إياه بالخطير جداً لقدرته على كشف عيوب الأنظمة البرمجية الضخمة. ومع تزايد الرهان على التحقق الرسمي (Formal Verification) كحل لصد موجات الهجمات القادمة، تأتي هذه الواقعة لتؤكد أن حتى الأدوات الميكانيكية لإثبات صحة الكود لا تحمي من أخطاء البيئة التحتية التي يعمل فوقها البرنامج، ما يترك الباب مفتوحاً أمام تساؤلات حول جدوى الضمانات الرياضية المطلقة في بيئات تشغيل غير مستقرة.
