ديب مايند: وكلاء ذكاء اصطناعي يثبتون رياضياً أمان شيفرة بروتوكول سيغنال

الملخص

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

خبر

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

تفصيل

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

خلفية

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

بين السطور

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

ماذا بعد؟

المؤشر القابل للتتبع هو ما إذا كانت ديب مايند ستنشر البراهين المولَّدة بلغة لين لمراجعة مستقلة، وما إذا كان الإطار سيُطبَّق على بروتوكولات تشفير أخرى واسعة الانتشار.

المصدر: مدونة غوغل ديب مايند