AlphaProof Code من DeepMind يتحقق رسميًا من بروتوكول Signal التشفيري في 4 أسابيع

يعرف كل مطور هذا الشعور: الاختبارات خضراء، ومراجعة الشيفرة اكتملت، والتدقيق لم يجد شيئًا، ومع ذلك لا يهدأ البال. فالاختبارات تفحص سيناريوهات محددة، وقد يكمن الخطأ في السيناريو الذي لم يخطر لأحد. هذا مقبول في تطبيق ويب عادي، لكنه غير مقبول في التشفير الذي تقوم عليه خصوصية ملايين المحادثات.

تقترح Google DeepMind طريقًا مختلفًا بإطلاق AlphaProof Code. وهو نظام متعدد الوكلاء يؤتمت التحقق الرسمي من الشيفرة.

ما التحقق الرسمي بلا رياضيات

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

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

ما الذي فُعل مع Signal

طبق الفريق AlphaProof Code على شيفرة البروتوكول التشفيري لـ Signal، وهو الذي يشفّر المحادثات في Signal وGoogle Messages. كتب الوكلاء المبنيون على Gemini 4 Carbon أكثر من ستة ملايين سطر بلغة Lean، وهي لغة وبيئة قابلة للتحقق للبراهين الرسمية. والنتيجة: ثبت رياضيًا أن الشيفرة توفر ضمانات الأمان المعلنة.

رقمان هنا أهم من غيرهما:

• 4 أسابيع. بحسب المؤلفين، تستغرق مهمة بهذا الحجم عادةً سنوات لدى فرق الخبراء.
• ~1%. هي نسبة المواضع التي حددها الوكلاء بأنفسهم، بعد تدقيق إثباتهم الخاص، على أنها تحتاج إلى نظرة بشرية. أما الباقي فمرّ دون تدخل يدوي.

تصف Google ذلك بأنه أول استخدام للذكاء الاصطناعي في التحقق الرسمي من برنامج حقيقي. وهذا تصريح من الشركة نفسها، ولا يوجد حتى الآن تحقق مستقل.

أين الفخ

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

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

وللنهج جانب قوي أيضًا. يُفحص الإثبات آليًا، ولا حاجة إلى تصديق الوكلاء ولا المؤلفين. فإذا قبل Lean الإثبات فهو صحيح. وهلوسات النموذج لا تقلق هنا: فالخطوة الخاطئة لن تجتاز الفحص ببساطة.

ماذا نفعل بهذا

لمطوري الشيفرة الحرجة (التشفير، المدفوعات، أنوية أنظمة التشغيل، بروتوكولات الإجماع): تابعوا انخفاض كلفة التحقق الرسمي. فإذا تأكد أن شهرًا بدلًا من سنوات ينطبق على مشاريع أخرى، فسينخفض حاجز الدخول بشدة.

لمديري المنتجات والمؤسسين في مجال الأمن: بدلًا من «اجتزنا التدقيق» سيمكن تقديم إثبات رياضي قابل للتحقق. وهذه حجة قوية للقطاعات الخاضعة للتنظيم والعملاء من الشركات.

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

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