AlphaProof Code من Google DeepMind يتحقق رسميًا من مكتبة libsignal

البرهان بدل الاختبار

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

في AlphaProof Code يقرر خبراء بشريون ما يجب إثباته، وتتولى مجموعة وكلاء تنفيذه. حدد الباحثون الخصائص استنادًا إلى أعمال أكاديمية حول Signal. وكتب الوكلاء، بالاعتماد على نموذج Gemini 4 Carbon، نحو 6.5 مليون سطر من البراهين بلغة Lean، التي يتحقق مدققها آليًا من كل خطوة. ولم يكتب أي باحث سطرًا واحدًا من البراهين بنفسه.

يركّز العمل على آلية «ratchet» التي تجدّد مفاتيح التشفير باستمرار. ووفق الورقة التقنية، لا يستطيع مهاجم سرق المفاتيح المخزنة في الهاتف قراءة الرسائل السابقة، لأن كل رسالة تُشفَّر بمفتاح مشتق من سابقه ثم يُمحى. وتعود المحادثة آمنة بمجرد أن يتبادل الطرفان رسائل جديدة، ولا يمكن لأحد انتحال هوية أحدهما. وللتأكد من صلاحية الطريقة، أعاد الباحثون خطأين قديمين صُحّحا في libsignal، فأظهر النظام أن هاتين النسختين لا توفران الضمانات المتوقعة.

حدود البحث

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

ويخلص المؤلفون إلى أنه مع انخفاض كلفة البراهين، يصبح السؤال الصعب هو: ماذا ينبغي إثباته؟