الذكاء الاصطناعي يختبر أسرار «سيجنال».. جوجل تقترب من ثورة في حماية الرسائل

أعلنت شركة «جوجل ديب مايند» في تطوير إطار جديد للذكاء الاصطناعي يحمل اسم «AlphaProof Code»، استخدمته فرق بحثية لإثبات عدد من الخصائص الأمنية في الشيفرة البرمجية الفعلية لبروتوكول التشفير الذي يعتمد عليه تطبيق «سيجنال»، في خطوة تستهدف نقل استخدام الذكاء الاصطناعي من اكتشاف الثغرات البرمجية إلى التحقق الرياضي من سلامة الأنظمة الرقمية

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

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

كيف فحص الذكاء الاصطناعي بروتوكول سيجنال؟

يعتمد نظام «AlphaProof Code» على مجموعة من وكلاء الذكاء الاصطناعي، تعمل بالتعاون مع الباحثين البشريين لتنفيذ مراحل التحقق، بداية من تحديد الخصائص الأمنية المطلوب إثباتها، وصولًا إلى إنتاج البراهين الرياضية التي تخضع للفحص الآلي

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

واستخدم النظام لغة «Lean»، وهي لغة برمجية مخصصة لصياغة البراهين الرياضية والتحقق منها، إذ لا يكتفي البرنامج بتقديم إجابة تؤكد سلامة الشيفرة، بل يتعين عليه إنتاج برهان يمكن التحقق منه بواسطة نواة اللغة نفسها

ووفقًا للورقة البحثية المنشورة عن المشروع، شملت عملية التحقق نحو 6.5 مليون سطر من البراهين، بينما اعتمدت على مواصفات وتعريفات موثوقة يبلغ حجمها نحو 18 ألف سطر، إضافة إلى نحو 8 آلاف سطر تتعلق بدلالات تعليمات المعالجات المستخدمة في عملية التحقق

ما الخصائص الأمنية التي خضعت للاختبار؟

ركز المشروع على التحقق من خصائص أمنية أساسية في مكونات التشفير الخاصة ببروتوكول سيجنال، شملت المصافحة التشفيرية المعروفة باسم «PQXDH»، وآلية «Triple Ratchet» المستخدمة في إدارة مفاتيح التشفير وتحديثها خلال المحادثات

وشملت الخصائص التي تناولتها البراهين السرية الأمامية، وهي خاصية تهدف إلى منع الوصول إلى الرسائل السابقة حتى في حال تعرض بعض المفاتيح للاختراق لاحقًا، إلى جانب المصادقة التي تساعد على التحقق من هوية أطراف الاتصال، وأمن الرسائل بعد اختراق الجهاز مؤقتًا، فضلًا عن سرية عملية إنشاء الاتصال المشفر

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

ونقلت مجلة «The Register» البريطانية أن المشروع استخدم إطارًا متعدد الوكلاء يجمع بين التوجيه البشري وإنتاج البراهين آليًا، فيما أشارت مجلة «Wired» الأمريكية إلى أن الاختبار لم يشمل تطبيق سيجنال بالكامل، وإنما ركز على خصائص محددة في مكونات التشفير التي خضعت للتحقق

أربعة أسابيع بدلًا من سنوات في عمليات التحقق

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

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

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

وذكرت جوجل أن وكلاء الذكاء الاصطناعي أنتجوا البراهين، بينما تولى الباحثون تحديد المواصفات ومراجعتها، كما أشاروا إلى أن النظام حدد نحو 1% من الشيفرة التي احتاجت إلى مراجعة بشرية إضافية، في حين خضعت بقية البراهين للتحقق الآلي بواسطة «Lean»

حدود التقنية وإمكانية استخدامها في قطاعات أخرى

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

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

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

ويأتي إعلان «AlphaProof Code» ضمن توجه متزايد لاستخدام وكلاء الذكاء الاصطناعي في تطوير البرمجيات وفحصها، بعدما ارتبطت تطبيقات هذه التقنية خلال السنوات الأخيرة بكتابة الشيفرات واكتشاف الأخطاء، بينما تستهدف التجربة الجديدة استخدام البراهين الرياضية للتحقق من أن البرامج تنفذ الخصائص الأمنية المحددة لها