أظهر باحثون في Google DeepMind أن نظامًا للذكاء الاصطناعي يستطيع إثبات خصائص أمنية مهمة في بروتوكول المراسلة Signal رياضيًا. واستخدم الفريق إطارًا جديدًا يُسمى AlphaProof Code للتحقق رسميًا من عدة ضمانات تشفيرية. استغرق العمل نحو أربعة أسابيع، ونُفّذ في إطار مشروع بحثي لا منتج تجاري. ولم يُعثر على ثغرات جديدة في الأجزاء التي فحصها الفريق، فيما رصد الذكاء الاصطناعي، على نحو صحيح، ثغرات أقدم كانت قد أُصلحت بالفعل عند تشغيله على إصدارات سابقة من البروتوكول.
يعني التحقق الرسمي استخدام الرياضيات للتأكد من أن البرنامج يعمل تمامًا كما هو مقصود، من دون ترك مجال لثغرات خفية. وكان هذا الإجراء يتطلب تاريخيًا من الخبراء كتابة مواصفات مفصلة، وتحويلها إلى صيغ رياضية، ثم بناء البرهان؛ وهي مهمة شاقة قد تستغرق أشهرًا. وبإسناد جانب كبير من العمل إلى ذكاء اصطناعي وكيل، أي ذكاء اصطناعي يستطيع وضع أهداف فرعية ومتابعتها، قلّصت DeepMind المدة إلى أسابيع. ويقول الباحثون إن الذكاء الاصطناعي ظل بحاجة إلى إشراف بشري في مراحل أساسية، لكنه استطاع اقتراح البراهين وتصحيحها ذاتيًا.
وأشار Ehren Kret، كبير مسؤولي التكنولوجيا في Signal، إلى أن أعمال التحقق السابقة اقتصرت على أجزاء صغيرة من الشيفرة. وقال إن نهج DeepMind يتيح «توسيعًا كبيرًا» لنطاق ما يمكن التحقق منه. وينشر الفريق المواصفات والبرهان اللذين أعدهما كي تتمكن مجموعات أخرى من البناء عليهما. ورغم أن النتيجة مبشرة، تحذر DeepMind من أن تطبيق هذا النهج على تطبيقات كاملة أو سلاسل توريد برمجية بأكملها لا يزال تحديًا، كما لم يُكشف عن تكلفة التحقق المدعوم بالذكاء الاصطناعي.
لماذا يهم هذا؟
إذا أمكن للذكاء الاصطناعي إثبات أمن بروتوكولات التشفير بموثوقية، فقد يكتسب مستخدمو Signal وGoogle Messages وWhatsApp والتطبيقات المشابهة ثقة أكبر بأن رسائلهم تظل خاصة. أما الشركات التي تعتمد على الاتصالات المشفرة، مثل المصارف ومقدمي الرعاية الصحية والصحفيين، فقد تتيح لها هذه التقنية مستقبلًا الحصول على ضمانات قابلة للتحقق قانونيًا بأن برامجها خالية من العيوب الحرجة.
لماذا يهم
بالنسبة إلى المستخدم العادي، يعني هذا الخبر أن التشفير الذي يحمي محادثاته خضع لفحص رياضي إضافي، ما يقلل احتمال وجود أخطاء خفية. وبالنسبة إلى الشركات الملزمة بإثبات امتثالها لقواعد الخصوصية، قد يصبح التحقق بمساعدة الذكاء الاصطناعي وسيلة جديدة لإثبات الأمان من دون عمليات تدقيق يدوية طويلة.
