وكلاء ذكاء اصطناعي من DeepMind يتحققون رياضياً من شيفرة تشفير Signal في أربعة أسابيع

كشفت Google DeepMind عن AlphaProof Code، وهو إطار ذكاء اصطناعي متعدد الوكلاء لـالتحقق الصوري، أي البرهنة رياضياً على أن البرنامج يفعل ما تنص عليه مواصفاته. وكان أول اختبار كبير له مكتبة libsignal، التنفيذ المرجعي لبروتوكول Signal الذي يحمي الرسائل في Signal وGoogle Messages وتطبيقات أخرى.

ما الذي تم إثباته

• كتب خبراء بشريون، بالتعاون مع نماذج ذكاء اصطناعي، مواصفات صورية لأهداف أمان Signal وراجعوا كل واحدة منها.
• ثم ولّد وكلاء البرهنة (تقول DeepMind إنهم يعملون بنموذج Gemini Carbon) نحو 6.5 مليون سطر من براهين Lean، تستند إلى نحو 26 ألف سطر من المواصفات الموثوقة ونموذج صوري لشيفرة الآلة AArch64.
• تغطي البراهين مصافحة PQXDH المقاومة للحوسبة الكمية وTriple Ratchet، وتثبت السرية الأمامية والمصادقة والأمان بعد الاختراق وسرية المصافحة — وذلك لـشيفرة الآلة المترجمة من libsignal v0.105.4 دون تعديل، لا لتصميم البروتوكول فقط.
• استغرق المشروع أربعة أسابيع. وللتحقق، أعاد الفريق إدخال ثغرتين حقيقيتين أُصلحتا منذ زمن في نسخة معزولة، فأثبت النظام أن هاتين النسختين غير آمنتين.

الحدود

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