ديب مايند تتحقق رسميًا من الضمانات الرئيسية لبروتوكول Signal خلال أربعة أسابيع

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

ما الذي أُنجز بالضبط

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

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

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

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

لماذا هذا مهم للممارسين

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

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

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

القيود وما يجب فعله

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

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

ما يمكن فعله الآن. ينشر الباحثون المواصفات والبرهان الخاصين بـ Signal، وهما مادة تعليمية جيدة لمن يكتبون شيفرة حرجة: المدفوعات والتشفير وبنية الثقة التحتية. وإذا كنت تعمل في هذه المجالات، فمن المفيد متابعة كيف تتحول أدوات مثل AlphaProof Code من عرض توضيحي إلى منتج، والتعلم مسبقًا كيفية صياغة خصائص الشيفرة بحيث يمكن إثباتها. فهذه المهارة، لا كتابة البراهين يدويًا، هي على الأرجح التي ستصبح ذات قيمة.