أعلنت «جوجل ديب مايند» استخدام الذكاء الاصطناعي للتحقق رياضيًا من خصائص أمنية أساسية في الشيفرة التي تنفذ بروتوكول «سيجنال» للتراسل المشفر. لكن النتيجة لا تعني أن تطبيق سيجنال كله خالٍ من الثغرات، ولا أنها شهادة بأن أحدًا لا يستطيع قراءة أي محادثة على واتساب مهما كانت حالة الهاتف أو الحساب.
الخبر، الذي أعلنته الشركة في 10 نوفمبر، يتعلق بأداة بحثية اسمها AlphaProof Code. وتكمن أهميته في الانتقال من فحص تصميم التشفير إلى إثبات أن شيفرة محددة، بعد تحويلها إلى تعليمات تنفذها الآلة، تحقق ضمانات أمنية محددة. وهذا فرق مهم عن الاكتفاء بأن تبدو الشيفرة سليمة عند مراجعتها.
ما الذي أثبتته ديب مايند؟
بحسب الإعلان الرسمي، عمل باحثون مع نماذج ذكاء اصطناعي لصياغة الأهداف الأمنية في صورة مواصفات رياضية، راجعها خبراء بشر. ثم تولت مجموعة من وكلاء الذكاء الاصطناعي كتابة البراهين، قبل أن تتحقق منها أداة Lean المخصصة لفحص صحة البراهين.
وتوضح الورقة التقنية المنشورة للمشروع أن العمل شمل نحو 6.5 مليون سطر من البراهين التي فحصتها الآلة. الرقم يصف حجم البرهان، وليس عدد ثغرات اكتُشفت، ولا نسبة تحسن في أمان الرسائل.
يغطي البحث خصائص في المصافحة التشفيرية PQXDH وآلية Triple Ratchet داخل مكتبة libsignal، منها التحقق من الهوية وسرية المصافحة وحماية الرسائل السابقة، وإمكان استعادة حماية الاتصال بعد اختراق وفق شروط النموذج الأمني. ولا تعني الخاصية الأخيرة أن استمرار سيطرة مهاجم على الهاتف يصبح آمنًا تلقائيًا.
لماذا يهم فحص الشيفرة المنفذة؟
يمكن أن يكون تصميم بروتوكول التشفير صحيحًا، بينما يقع خطأ عند تحويله إلى برنامج. يحاول هذا البحث تقليل الفجوة بين الأمرين: هل التنفيذ الذي تفحصه الدراسة يفي فعلًا بالخصائص التي اتفق الباحثون على إثباتها؟
وتقول ديب مايند إن عملية التحقق استغرقت أربعة أسابيع. وهذه مدة المشروع كما أعلنتها الشركة، وليست وعدًا بإمكان فحص أي تطبيق كامل بالمدة نفسها. كما أن البشر ظلوا مسؤولين عن مراجعة المواصفات والافتراضات التي يبنى عليها البرهان.
وللتأكد من أن المنهج لا يمنح نتائج مطمئنة للشيفرة الخاطئة، أعاد الباحثون إدخال خطأين حقيقيين سبق إصلاحهما إلى نسخة معزولة من الشيفرة. وفي الحالتين أنتج النظام برهانًا بأن النسخة المعدلة غير آمنة. هذه تجربة على خطأين معروفين، وليست إعلانًا عن ثغرتين جديدتين في الإصدار الذي يستخدمه الجمهور الآن.
أين تتوقف حدود النتيجة؟
تحدد الورقة نطاقًا تقنيًا واضحًا: إصدار معين من libsignal داخل برنامج صغير لسطر الأوامر، جرى تجميعه لبيئة AArch64 على لينكس. وتغطي البراهين بدء جلسة وإرسال رسالة واستقبالها، بينما لا تشمل عملية إنشاء المفاتيح نفسها ضمن البرنامج التجريبي.
كما يعتمد الاستنتاج على مواصفات ونموذج لتنفيذ التعليمات، وعلى افتراضات بشأن الأدوات التشفيرية الأساسية وبعض الدوال التي يستدعيها البرنامج. لذلك فالعبارة الدقيقة هي إثبات خصائص محددة ضمن نطاق وافتراضات معلنة، لا إثبات أمان كل جهاز أو كل سطر في التطبيق.
وفي تغطية مستقلة لمجلة WIRED، أكد الباحثون أن الدراسة لم تتحقق رسميًا من تطبيق سيجنال المحمول بالكامل. ولم يعلنوا اكتشاف ثغرات جديدة في الأجزاء التي فحصوها، كما لم تكشف جوجل تكلفة المشروع أو خطة لطرحه كمنتج تجاري.
وماذا تعني لمستخدم واتساب؟
تستخدم خدمات واسعة الانتشار، منها واتساب ورسائل جوجل، تقنيات مبنية على بروتوكول سيجنال أو نسخًا منه، وفق الورقة البحثية. لكن فحص تنفيذ libsignal في البيئة المحددة لا يساوي فحص كل تنفيذ تستخدمه هذه التطبيقات، ولا يراجع تلقائيًا واجهاتها وحساباتها والنسخ الاحتياطية والأجهزة المرتبطة بها.
ويظل من المهم التمييز بين حماية الرسالة أثناء انتقالها وبين ما يحدث عند طرفي المحادثة. فالبحث ليس اختبارًا لهاتف بعينه، ولا ضمانًا ضد قراءة شخص يمتلك وصولًا إلى الجهاز أو إلى الرسائل بعد فك تشفيرها عند المستلم.
بالنسبة للقارئ، النتيجة تدعم الثقة في خصائص تشفير محددة وتعرض طريقة قد توسع نطاق مراجعة البرمجيات مستقبلًا. لكنها لا تبرر تجاهل تحديثات الأمان أو مشاركة رموز تسجيل الدخول، ولا تتطلب تنزيل أداة جديدة للاستفادة من «حماية» منفصلة. AlphaProof Code هنا مشروع بحثي للتحقق، وليس تطبيق حماية أطلقته جوجل للمستخدمين.
