أكمل فريق البحث في Google DeepMind التحقق الرسمي من أمان رسائل Signal، مشيرًا إلى أن هذه هي المرة الأولى التي يتم فيها مساعدة الذكاء الاصطناعي في بناء إثبات، مما يربط بين ضمانات الأمان على مستوى البروتوكول وتنفيذ تشفير مستخدم على نطاق واسع.
تم إنجاز هذا العمل بفضل AlphaProof Code، وهو إطار عمل متعدد الوكلاء مخصص للتعريفات الرسمية والتحقق من البرمجيات. في العملية، يقوم وكيل موجه بشريًا بكتابة تعريفات Lean، وتقييم دلالات الشيفرة الآلية، ثم يقوم الوكيل بتوليد الإثبات، الذي يتم التحقق منه نقطة بنقطة بواسطة نواة Lean.
كان الهدف من التحقق هو عملية المصافحة PQXDH بعد الكمومية وTriple Ratchet في Signal، مما أكد تصميم libsignal من حيث السرية الأمامية، والمصادقة، وقدرة الاسترداد بعد تسرب المفاتيح، وسرية المصافحة. هذه الخطوة تقربنا أكثر من الفكرة التي طرحتها مؤسسة الذكاء الاصطناعي المفيد في أبريل من هذا العام: حيث تأمل المؤسسة في استخدام التحقق الرسمي Lean لبروتوكول Signal وتطبيقاته.
تمت العملية بالتعاون مع عدة نماذج، حيث تم تحويل أهداف الأمان الخاصة بـ Signal إلى تعريفات رياضية تمت مراجعتها يدويًا، ثم قام وكيل Gemini Carbon بتوليد شيفرة Lean بناءً على ذلك، لإثبات صحة تنفيذ libsignal. وقد قام الوكيل بتوليد 6.5 مليون سطر من الشيفرة، ثم أجرت الفريق جولة تدقيق، وحددت الأجزاء التي تحتاج إلى مراجعة بشرية.
Google DeepMind تحقق بنجاح من أمان رسائل Signal
قال Swarat Chaudhuri، عالم أبحاث في Google DeepMind وأستاذ في جامعة تكساس في أوستن: "هذا نظام تم بناؤه أساسًا للتعاون بين البشر والذكاء الاصطناعي". وأشار إلى أن الطريقة التقليدية هي أن يقوم الرياضيون بتقديم مشاكل محددة بوضوح للذكاء الاصطناعي لإثباتها، بينما في هذه الحالة كان من الضروري أولاً تحديد ما يجب إثباته.