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