تقول Google DeepMind إنها استخدمت AlphaProof Code للتحقق رياضيًا من خصائص أمنية أساسية في libsignal، التطبيق المرجعي لبروتوكول المراسلة Signal. استغرق العمل أربعة أسابيع. وتقول DeepMind إن فرق الخبراء كانت تحتاج تاريخيًا إلى سنوات لإجراء تحقق مماثل.
جمع النظام بين باحثين بشريين ووكلاء ذكاء اصطناعي. وساعد الباحثون والذكاء الاصطناعي في تحويل أهداف Signal الأمنية إلى مواصفات رياضية راجعها البشر. ثم أنشأ وكلاء يعملون بنموذج Gemini Carbon نحو 6.5 مليون سطر من شيفرة البراهين بلغة Lean. وهي لغة برمجة يستطيع مدقّقها التحقق من التزام البرهان الرياضي بقواعدها. وأحال الوكلاء نحو واحد في المئة من قاعدة الشيفرة إلى المراجعة البشرية.
ما الذي شمله البرهان؟
تحقق الباحثون من الشيفرة الآلية المترجمة لمصافحة PQXDH ما بعد الكمومية وبروتوكول Triple Ratchet في libsignal. وأثبتوا خصائص محددة، منها السرية الأمامية والمصادقة والحماية بعد اختراق أحد الأجهزة. وتقول الورقة البحثية إن الشيفرة جُمّعت من Rust من دون تعديل، باستخدام مُصرّف قياسي، ثم دُققت بوصفها شيفرة آلية لمعمارية AArch64.
يتجاوز ذلك إثبات أمان تصميم نظري، إذ يربط ضمانات أمنية محددة بالشيفرة المترجمة. وتصف DeepMind هذا بأنه أول تحقق رسمي بهذا العمق من تنفيذ بروتوكول تشفير واسع الاستخدام. كما أعاد الفريق إدخال ثغرتين سبق إصلاحهما في نسخة معزولة من الشيفرة؛ فأنتج النظام براهين تُظهر أن النسخ التي تحتوي على الثغرتين أخفقت في استيفاء الخصائص الأمنية المحددة.
للبرهان حدود
لا يقدم هذا العمل ضمانًا رياضيًا بأن كل مكونات Signal، أو كل تطبيق يستخدم البروتوكول، خالية من المشكلات الأمنية. فالبرهان يغطي خصائص مختارة في libsignal، لا التطبيق بأكمله. كما يعتمد على مواصفات معتمدة ومدقّق Lean وعقود تحكم الروتينات التشفيرية منخفضة المستوى. وتشير The Register إلى أن النتيجة لا تثبت السرية الحاسوبية لبايتات الرسائل الفعلية؛ فيما تصف ورقة DeepMind براهين ضمن نماذج رمزية وحاسوبية، تعتمد على افتراضات بشأن بدائيات التشفير الأساسية.
تقول DeepMind إنها تتيح مواد التحقق للآخرين لاستخدامها. وتأمل في تطبيق النهج على مجالات مثل البرمجيات الثابتة للأجهزة الطبية وبرمجيات شبكات الكهرباء، لكنها تشير إلى أن توسيع نطاق الطريقة يتطلب مزيدًا من البحث. ويمثل هذا العمل خطوة نحو التحقق من مزيد من الشيفرات المستخدمة في العالم الحقيقي، لا دليلًا على التحقق من تلك الأنظمة الأخرى.
لماذا يهم
بالنسبة إلى مستخدمي Signal، يضيف هذا العمل برهانًا مدققًا آليًا على خصائص أمنية محددة في تنفيذ البروتوكول الأساسي. لكنه لا يثبت خلو التطبيق بأكمله من الأخطاء، كما يعتمد البرهان على افتراضات بشأن المكونات التشفيرية.
