ذكاء DeepMind يتحقق من شيفرة تشفير Signal في أربعة أسابيع

ما هو التحقق الرسمي من الشيفرة؟

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

كيف يعمل النظام؟

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

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

لم يشمل المشروع تطبيق Signal للهاتف بأكمله. وتشير Wired إلى أن DeepMind استفادت من عمل سابق في التحقق الرسمي أجرته Signal Foundation. وقال إيهرن كريت، المدير التقني في Signal، إن العمل السابق «ركز على أجزاء أصغر من الشيفرة»، بينما يتيح نهج DeepMind «توسعاً كبيراً».

ولا يريد الباحثون وضعاً يكتب فيه الذكاء الاصطناعي الأهداف والبراهين معاً. وقال سواراط تشودري من DeepMind إنهم لا يريدون عالماً يولّد فيه الذكاء الاصطناعي الأهداف والبراهين ويؤدي امتحانات كتبها بنفسه. لذلك راجع البشر المواصفات والأجزاء المعلّمة.

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