DeepMind تثبت رياضيًا أمان شيفرة Signal في 4 أسابيع بدلًا من سنوات

يعرف كل من كتب شيفرات تشفير حقيقة مزعجة: يمكن إثبات البروتوكول ببراعة على الورق، ومع ذلك تظهر الثغرة في الشيفرة. فبين المخطط والتنفيذ هوة واسعة، وفيها تحديدًا تعيش الأخطاء الحقيقية. وتقول Google DeepMind إنها علّمت وكلاء الذكاء الاصطناعي سدّ هذه الهوة في أحد أهم البروتوكولات في العالم، وهو البروتوكول الذي يحمي المراسلات في Signal وGoogle Messages.

ما الذي فُعل بالضبط

يُسمى النظام AlphaProof Code. وهو إطار عمل متعدد الوكلاء يعتمد على عدة نماذج LLM، ويقسّم العمل كما كان سيقسّمه فريق بحثي. في البداية يحوّل خبراء بشريون، بمساعدة النماذج، أهداف الأمان في Signal إلى مواصفات رياضية رسمية. ويراجع إنسان كل مواصفة يدويًا. بعد ذلك يكتب الوكلاء المبنيون على Gemini Carbon البراهين نفسها بلغة Lean، فكانت النتيجة أكثر من ستة ملايين سطر.

ثم تأتي النقطة الأكثر عملية. تتحقق Lean بنفسها من صحة كل برهان، لذا لا حاجة إلى الثقة العمياء بالنموذج: أي استنتاج خاطئ لن يجتاز التحقق ببساطة. كما دقّق الوكلاء النتيجة إضافيًا وحددوا المواضع التي تحتاج إلى نظرة بشرية. وهي نحو 1% من قاعدة الشيفرة. وركّز الخبراء عليها بدلًا من إعادة قراءة ملايين الأسطر.

لماذا ليس هذا مجرد تدقيق آخر

يتوقف التحقق الرسمي المعتاد من البروتوكولات عند مستوى التصميم: يُثبت أن المخطط آمن. أما هنا فقد ذهب الوكلاء أبعد، وأثبتوا خصائص للشيفرة المُصرَّفة التي تعمل على الأجهزة. على سبيل المثال، أن الرسائل تبقى محمية قبل الاختراق المؤقت للجهاز وبعده.

ولاختبار نزاهة النظام أجرى المؤلفون اختبارًا بسيطًا. ففي نسخة معزولة من شيفرة Signal أُعيد إدخال خطأين حقيقيين سبق إصلاحهما. وفي الحالتين أصدر النظام برهانًا قابلًا للتحقق آليًا على أن هذه النسخة غير آمنة. أي أن الأداة تميّز الشيفرة الصحيحة من الخاطئة، ولا «توافق» ببساطة على كل شيء.

وبحسب DeepMind، استغرق كل شيء أربعة أسابيع، في حين كان هذا العمل يستغرق تقليديًا سنوات من فرق الخبراء. ووصف المدير التقني لـ Signal، إيرين كريت، التحويل الآلي للشيفرة الإنتاجية إلى مبرهنات Lean بأنه اختراق كبير.

القيود والخلاصة العملية

ينبغي النظر إلى الحجم بواقعية. فهذا بروتوكول واحد، دُرس طويلًا وبعناية، ويعتمد الجزء الأكبر من الأرقام المعلنة على تقرير DeepMind الذاتي. ولم يُستبعد البشر من العملية: فتحديد ما يُعدّ «آمنًا» لا يزال بيد الخبراء، وأي خطأ في المواصفة يؤدي إلى إثبات شيء آخر غير المطلوب. ويقول المؤلفون أنفسهم إن التوسع يحتاج إلى مزيد من الأبحاث. أما الاتجاهات المعلنة، وهي البرمجيات الثابتة للأجهزة الطبية وبرمجيات شبكات الطاقة، فلا تزال مجرد خطط.

ماذا يعني هذا للمطورين والمؤسسين؟

• ثنائية «النموذج اللغوي يكتب، والمدقق الرسمي يقبل أو يرفض» نمط عملي للمهام التي تكلفة الخطأ فيها مرتفعة. يُسمح للنموذج بأن يخطئ، أما المدقق فلا.
• إذا كنت تعمل على التشفير أو منطق المدفوعات أو الشيفرة المدمجة الحرجة، فلم يعد التحقق الرسمي حكرًا على الفرق الأكاديمية ذات ميزانيات السنوات.
• مهارة صياغة المواصفات تصبح أثمن من مهارة كتابة البراهين. وتنتقل نقطة الاختناق إلى سؤال: «ما الذي نريد ضمانه أصلًا».

ومن الإيجابيات أيضًا أن DeepMind تتيح مخرجات التحقق للعموم. يمكن دراستها واستخدامها نموذجًا لتجارب خاصة مع Lean والوكلاء. ومع أدوات مثل CodeMender التي تبحث عن الثغرات وتصلحها، تتحول البراهين الرسمية إلى جزء من منظومة الحماية المعتادة، لا إلى غرابة أكاديمية نادرة.