ديب مايند تثبت رسميًا الضمانات الأساسية لبروتوكول Signal خلال 4 أسابيع بمساعدة الذكاء الاصطناعي

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

ماذا فعلوا بالضبط

استخدم فريق DeepMind إطار عمل جديدًا هو AlphaProof Code. استغرق العمل أربعة أسابيع وكان مصممًا كإثبات للمفهوم. يحمي بروتوكول Signal المراسلات ليس في تطبيق Signal نفسه فحسب، بل أيضًا في Google Messages وWhatsApp، ولذلك فهو من أكثر البروتوكولات التشفيرية استخدامًا في العالم.

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

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

أين المحاذير

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

السؤال الرئيس للصناعة هو الحجم والتكلفة. أجرت DeepMind التحليل مجانًا كمشروع بحثي، ورفضت Google الكشف عن كلفته. وعندما سُئلت الشركة عما إذا كانت تخطط لمنتج أو خدمة تجارية للتحقق الرسمي، لم تقدم جوابًا أيضًا. ويعترف الباحث سواراط تشودهوري نفسه بأن أمام توسيع النطاق ليشمل برمجيات العالم كلها «طريقًا طويلًا».

الإنسان يبقى في الحلقة

أكثر ما يثير الاهتمام هو العملية التي يسميها الفريق «human-AI collaboration». يساهم الوكلاء في كل مرحلة تقريبًا ويصححون أخطاءهم بأنفسهم، لكنهم يطلبون مراجعة بشرية عند المفترقات الأساسية. ويقول تشودهوري صراحة إنه لا يريد «عالم vibe coding» يصوغ فيه الذكاء الاصطناعي الأهداف بنفسه ويكتب البراهين بنفسه ويجتاز اختباراته بنفسه في الواقع. المطلوب حل وسط.

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

ماذا نفعل بهذا

على المطورين والمؤسسين الذين يقوم منتجهم على منطق حرج (المدفوعات والتشفير وبروتوكولات المزامنة) أن ينظروا إلى التحقق الرسمي كخيار حقيقي لا كغرابة أكاديمية. وما دامت تكلفته مجهولة، فمن المبكر إدراجها في الميزانية. لكن هناك فائدة ملموسة: تنشر DeepMind المواصفات والبرهان الخاصين بـ Signal، ويمكن دراستهما واستخدامهما في أعمال تحقق أخرى.

وبحسب بوشميت كوهلي من Google Cloud وDeepMind، ستتمكن البنوك والشركات الأخرى التي تعتمد على ضمانات الصحة من القول «يمكنني إثبات هذه الخصائص». حتى الآن هذا وعد أكثر منه منتجًا جاهزًا. لكن التحقق بالذكاء الاصطناعي اجتاز أول اختبار جدي له على بروتوكول حقيقي واسع الاستخدام.