AlphaProof Code من Google DeepMind يتحقق من أمان Signal

البشر يحددون ما يجب إثباته

بدأ الفريق بتحويل أهداف الأمان في Signal، بمساعدة نماذج مختلفة، إلى مواصفة رياضية يراجعها البشر. بعد ذلك أنتجت وكلاء Gemini Carbon شيفرة Lean تثبت صحة تنفيذ libsignal، وبلغ حجمها 6.5 مليون سطر، ثم أُجريت جولة تدقيق حددت الأجزاء التي تحتاج إلى مراجعة بشرية.

النتيجة نظرية، إذ تفترض تشفيرًا مثاليًا ولا تضمن السرية الحسابية للبايتات، لكنها تبقى تأكيدًا مهمًا للصحة. وتمثل خطوة نحو التحدي الذي أطلقته Beneficial AI Foundation في أبريل للتحقق الرسمي من بروتوكول Signal وتطبيقه باستخدام Lean.

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

التكلفة والخطوة التالية

كان التحقق الرسمي يتطلب جهودًا هائلة؛ فنواة seL4 استغرقت 20 سنة-شخص، ومترجم CompCert C ست سنوات. أما مشروع Signal فاستغرق من خمسة أشخاص أربعة أسابيع، مع «عدد لا بأس به من الرموز (tokens)» بحسب الباحثين.

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