تستخدم Google DeepMind وكلاء الذكاء الاصطناعي للتحقق من الشيفرة الآلية الأساسية لـ Signal

قدمت Google DeepMind AlphaProof Code في 10 نوفمبر 2026، مستخدمةً فرقًا من وكلاء الذكاء الاصطناعي لإنتاج براهين Lean قابلة للتحقق آليًا بشأن خصائص أمنية محددة في شيفرة libsignal المترجمة الخاصة بـ Signal. وأنجز فريق البحث المؤلف من خمسة أشخاص أعمال الإثبات في أربعة أسابيع، وأتاح مواصفاته ومخرجات التحقق للمراجعة الخارجية.

تجاوز العمل النماذج المجردة لتصميم بروتوكول Signal، وانتقل إلى تطبيقه المترجم. أحاط الباحثون حزمتَي libsignal v0.105.4 وSPQR v1.6.0، من دون تعديلهما، بأداة صغيرة تعمل عبر سطر الأوامر، ثم استخدموا مترجم rustc القياسي لبناء ملف تنفيذي لنظام Linux بمعمارية AArch64، مرتبط ارتباطًا ساكنًا. وتصف الورقة التقنية النتيجة بأنها أول براهين أمنية على مستوى البروتوكول لشيفرة غير معدلة لتطبيق بروتوكول تشفيري واسع الانتشار.

كيف قسّم AlphaProof Code العمل

أمضى خمسة باحثين أربعة أسابيع في أعمال الإثبات، وشغّلوا الوكلاء باستمرار على محطات عملهم، بالتوازي مع العمل على براهين رمزية وحسابية. وتفيد الورقة بأن الوكلاء أنتجوا نحو 6.5 ملايين سطر من شيفرة براهين Lean القابلة للتحقق آليًا، استندت إلى نحو 26 ألف سطر من المواصفات الموثوقة ودلالات AArch64.

اختار البشر الخصائص، وحسموا أوجه الالتباس والمفاضلات الأمنية، وراجعوا المواصفات واحتفظوا بالموافقة النهائية. وصاغت الوكلاء المدعومة من Gemini 4 Carbon وClaude Opus 5.5 تلك المواصفات وراجعتها، بما في ذلك مراجعتها من نموذج ينتمي إلى عائلة مختلفة. ثم أنتجت فرق وكلاء Gemini 4 Carbon جميع شيفرات البراهين؛ ولم يكتب أي من المؤلفين شيفرةً للبراهين. واستخدمت الحملات المعتادة ما بين 40 و80 وكيلًا على جهاز واحد لمدة تتراوح بين 24 و72 ساعة، مع منسق وقادة فرق ينسقون عمل وكلاء الإثبات، فيما تولت أدوار المهندس المعماري ومتكامل الأنظمة صيانة قاعدة البراهين المشتركة.

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

التغطية الأمنية واختبارات الأخطاء التاريخية

كان الهدف الذي خضع للتحقق هو شيفرة الجلسات الفردية التي تشمل المصافحة PQXDH ومراسلات Triple Ratchet. ويذكر الباحثون أنهم توصلوا إلى حجتين مستقلتين: عشر مبرهنات رمزية في ظل افتراضات تشفيرية مثالية، وبرهان حسابي يضع حدًا لميزة المهاجم بالاستناد إلى افتراضات تشفيرية ومصطلحات إحصائية. وتشمل الخصائص السرية الأمامية، التي تحمي الرسائل السابقة إذا سُرقت الحالة الحالية؛ والمصادقة؛ وأمن ما بعد الاختراق، المتعلق بالتعافي بعد وقوع الاختراق؛ وسرية المصافحة. كما تشمل الحجة الرمزية سرية المصافحة حتى بعد اختراق لاحق لخوارزمية Diffie–Hellman.

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

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

الحدود والخطوات التالية

لا ترقى هذه الضمانات إلى حد التصديق على تطبيقات Signal كاملة. فهي تخص نسخة libsignal-cli التي أعدها الباحثون وتعمل في عملية جديدة؛ ولم يخضع توليد المفاتيح للتحقق، وأُرجئت مراسلات المجموعات إلى أعمال مستقبلية، كما تقع القنوات الجانبية وحالة الأجهزة المتعددة خارج نطاق السيناريو. وتُمثَّل المكوّنات التشفيرية منخفضة المستوى، ومجموعة مختارة من إجراءات الإخراج والمكتبات، بعقود موثوقة؛ لذلك تعتمد النتيجة أيضًا على تلك العقود، والمواصفات المعتمدة، ونواة Lean، ودلالات AArch64، والافتراضات المتعلقة بالمكوّنات التشفيرية.

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

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

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