استخدم باحثون في Google DeepMind ذكاءً اصطناعيًا وكيلًا لإثبات عدة ضمانات تشفيرية رئيسية لبروتوكول Signal رياضياً. تم إجراء هذا العمل، الذي استغرق أربعة أسابيع كمشروع إثبات مفهوم، باستخدام إطار عمل جديد للذكاء الاصطناعي يُدعى AlphaProof Code.
يضمن بروتوكول Signal تشفير اتصالات تطبيق Signal، وكذلك، وفقًا للمصدر، تطبيقي Google Messages وWhatsApp. بالنسبة للمقال، يمثل هذا الإثبات تحققًا مستقلًا جديدًا من هذه التشفيرية، التي تحمي كمية هائلة من الرسائل حول العالم. كما يوضح قدرات Google DeepMind في مجال التحقق الرسمي.
التحقق الرسمي هو استخدام الرياضيات للتحقق من أن البرنامج يعمل كما هو متوقع، أي أنه لا يحتوي على ثغرات حرجة. يعتبره مؤيدوه منذ فترة طوحلة الكأس المقدسة لأمن البرمجيات. لكن استخدامه على نطاق واسع لا يزال غير مؤكد، وكذلك فعاليته في مواجهة كميات كبيرة من التعليمات البرمجية.
تحليل مستهدف
قبل عصر الذكاء الاصطناعي، كان يتطلب الأمر وقتًا كبيرًا لوصف خصائص البرنامج، وتحويل هذه الأوصاف إلى صيغ، ثم صياغة البرهان. وفقًا للمصدر، يمكن للذكاء الاصطناعي الوكلي تقليل مدة هذه الخطوة الأخيرة بشكل كبير. ومع ذلك، يبقى نطاق التحليل محدودًا: فهو لم يتحقق رسميًا، على سبيل المثال، من تطبيق Signal للهواتف المحمولة بأكمله.
في الأجزاء التي تم فحصها من البروتوكول، لم يجد الباحثون أي ثغرات جديدة. على العكس من ذلك، عندما طبقوا AlphaProof Code على إصدارات قديمة من Signal تحتوي على ثغرات معروفة وتم إصلاحها منذ فترة طويلة، حددت الأداة هذه الثغرات بشكل صحيح وأظهرت أن البروتوكول لا يمكن التحقق منه رسميًا في تلك الإصدارات. ينشر الباحثون المواصفات والبرهان اللذين تم تطويرهما لتحليل بروتوكول Signal، لتسهيل أعمال التحقق الرسمي الأخرى.
تعود سرعة المشروع جزئيًا إلى أعمال سابقة لـ Signal Foundation في هذا المجال، كما يؤكد باحثو DeepMind. «بينما ركز التحقق الرسمي السابق على أجزاء أصغر من التعليمات البرمجية، تتيح طريقة Google DeepMind توسيعًا كبيرًا»، كما يقول إيرين كريت، المدير التقني لـ Signal، في بيان. «مع تزايد التهديدات الأمنية المرتبطة بالذكاء الاصطناعي، فإن التحقق الدقيق من تنفيذ بروتوكول Signal يمنحنا ثقة أكبر في ضمانات الخصوصية التي يوفرها برنامجنا.»
مسألة تكلفة ونطاق
بالنسبة للخدمات الحرجة المستخدمة في سياقات عالية المخاطر، فإن القدرة على التحقق رسميًا من كل قاعدة تعليمات برمجية وسلسلة التوريد البرمجية بأكملها ستكون، وفقًا لـ Pushmeet Kohli، كبير العلماء في Google Cloud ونائب رئيس الأبحاث في DeepMind، تقدماً كبيرًا. «إذا أمكننا الآن التحقق من صحة هذه التنفيذات، فيمكننا أن نطمئن. تخيل البنوك، وجميع الشركات الأخرى التي تعتمد على ضمانات وتقلق بشأن الأخطاء البرمجية، يمكنها الآن القول: ‘أستطيع إثبات هذه الخصائص’»، كما يقول.
تبقى مسألة، مفتوحة أمام القطاع التكنولوجي بأكمله، حول قدرة التحقق الرسمي الآلي بالذكاء الاصطناعي على الانتقال فعليًا إلى نطاق واسع، وبكلفة معقولة. نفذت DeepMind تحليل Signal مجانًا، كجزء من مشروع بحثي، ولم ترغب Google في الإفادة عن تكلفته. كما لم توضح الشركة ما إذا كانت تخطط لتسويق منتج أو خدمة للتحقق الرسمي.
يقدّر الباحثون أن بعض تقدمهم الحاسم يكمن في «عملية تعاون بين الإنسان والذكاء الاصطناعي»، وفقًا لتعبير Swarat Chaudhuri، عالم أبحاث في DeepMind. تتيح هذه العملية للوكلاء المساهمة وتصحيح أنفسهم تقريبًا في كل خطوة، مع طلب رأي البشر وتحققهم في لحظات حاسمة. «لا نريد هذا العالم الغامض، حيث يحدد الذكاء الاصطناعي الأهداف، وينتج الذكاء الاصطناعي البراهين، ونجتاز الاختبارات التي كتبها بنفسه. هناك طريق وسط.»
