AlphaProof Code يُثبت صحة نواة التشفير في Signal خلال 4 أسابيع بدلًا من سنوات

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

ما الذي عرضته DeepMind

قدّم الفريق AlphaProof Code، وهو نظام يُثبت بلا أخطاء أن البرنامج يطابق مواصفات الأمان الخاصة به. وجرى العرض التوضيحي على نواة بروتوكول التشفير في Signal. ووفق الباحثين Pushmeet Kohli وSwarat Chaudhuri في مدونة DeepMind، يستغرق مثل هذا العمل عادةً سنوات، أما هنا فقد كفت أربعة أسابيع.

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

كيف يعمل ذلك في مثال بسيط

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

تنقسم العملية إلى مرحلتين:

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

وفي المجموع كتب الوكلاء أكثر من ستة ملايين سطر بلغة Lean. وقد وسم النظام نحو 1% من قاعدة الشيفرة للتحقق اليدوي من قبل البشر. وللمراقبة، زرع الباحثون في الشيفرة خطأين، وجرى التقاطهما فورًا. ويقول المدير التقني لـ Signal، Eren Kret، إن هذا النهج يعزز الثقة بخصوصية البيانات في ظل تزايد التهديدات المرتبطة بالذكاء الاصطناعي.

ما ينبغي أن نضعه في الحسبان

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

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

ثالثًا: يبدو 1% من الشيفرة تحت المراجعة البشرية متواضعًا، لكن الحديث هنا عن التشفير، حيث قد يُبطل جزء واحد غير مُتحقَّق منه قيمة الباقي. ووسم مثل هذه المواضع جزء من الطريقة، لا ضعف فيها.

ماذا يعني ذلك عمليًا

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

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

وتخطط DeepMind لتعميم الطريقة على شبكات الطاقة والأجهزة الطبية عبر أنظمة مثل CodeMender. وثمن الخطأ هناك لا يقل عنه في تطبيق المراسلة، والمتطلبات غالبًا أشد صرامة. ويبقى أن نتحقق من تكرار النتيجة في مشاريع أخرى ومن تأكيد متخصصين مستقلين لها.