وسعت جوجل الوصول إلى Gemini 4 Carbon وأشارت إلى أن وكلاء تم بناؤهم على هذا النموذج ساهموا في التحقق رسميًا من ضمانات أمان جوهرية في كود بروتوكول Signal.
يمكن للمطورين والشركات الدافعين الآن استخدام Carbon عبر واجهة برمجة تطبيقات Gemini و Gemini for business، كما أن مشتركي Google AI Ultra لديهم وصول إليه أيضًا. تنطبق أسعار ترويجية بقيمة 2 دولار و 10 دولارات لكل مليون وحدة رمزية للإدخال والإخراج حتى 30 نوفمبر، قبل أن تتضاعف. الوحدة الرمزية (token) هي وحدة نصية يعالجها النموذج لقراءة أو إنتاج المحتوى.
حتى الآن، كان بإمكان عدد محدود من المدافعين عن الأمن السيبراني الأعضاء في برنامج Fairwind التابع لجوجل فقط استخدام Carbon. لا يزال يتعين عليهم الانتماء إلى هذا البرنامج للوصول إلى Carbon for cyber، وهو إصدار تقدمه جوجل باعتباره في الصدارة في المعايير الرئيسية للكشف عن الثغرات واستغلالها وتصحيحها.
تطبيقات في الأمن السيبراني
وفقًا لجوجل، استخدمت شركة Wiz إصدار Carbon for cyber للعثور على ثغرات من نوع « zero-day » لدى اثنين من كبار مزودي البرمجيات كخدمة (SaaS)، في غضون ساعتين. من جانبها، استخدم فريق Cloud Vulnerability Research (CVR) التابع لجوجل النموذج لتأكيد أن اثنين من الأخطاء في مشروع مفتوح المصدر شهير كانا قابلين للاستغلال، بشدة مماثلة لـ PHP2Shell، وهي زوج من الثغرات في PHP تم استغلالهما بالفعل من قبل مهاجمين.
«باستخدام Carbon لبناء نموذج أولي للإثبات، ساعد فريق CVR القائمين على المشروع في إعادة تصنيف الخطأ على أنه حرج ونشر تصحيح بسرعة»، كما ذكرت جوجل.
فحص كود Signal
من ناحية أخرى، قدمت Google DeepMind أداة AlphaProof Code، التي تجمع بين خبراء بشريين ووكلاء ذكاء اصطناعي للتحقق رسميًا من البرمجيات، أي لإثبات رياضيًا أنها تلتزم بمتطلبات محددة. طبق الفريق الأداة على libsignal، التنفيذ المرجعي لبروتوكول Signal. تعمل إصدارات من هذا البروتوكول أيضًا في WhatsApp وGoogle Messages.
عمل بشر مع وكلاء تم تشغيلهم على Carbon وعلى Claude Opus 5.5 لكتابة المواصفات التي تصف ما يجب إثباته. بعد ذلك، قامت وكلاء مبنية على Carbon بتوليد جميع ما يقرب من 6.5 مليون سطر من البراهين المكتوبة بلغة Lean، وهي أداة مساعدة للبراهين ترفض تلك غير الصالحة. وفقًا لجوجل، فإن الضمانات المثبتة، والتي تشمل السرية الدائمة (forward secrecy)، والأمان بعد الاختراق، والمصادقة، تنطبق على كود الآلة المترجم، في حين أن معظم عمليات التحقق من البروتوكولات تركز فقط على التصميم.
أنجز خمسة باحثين عمل الإثبات في أربعة أسابيع، وهو عمل تقول جوجل إنه كان تقليديًا حكرًا على المتخصصين لسنوات. للتحقق من أن الطريقة تكتشف ثغرات حقيقية، أعاد الفريق إدخال خطأين قديمين في libsignal، تم تصحيحهما بالفعل، وأثبت أن هذه الإصدارات لم تعد تلتزم بضمانات الأمان.
النتائج تنطبق على إصدار الكود الذي قامت جوجل بتجميعه، والذي يتم تشغيله عبر أداة صغيرة في سطر الأوامر، وليس على «تطبيقات Signal نفسها». كما تم استبعاد بعض قنوات التسريب الجانبية من أجزاء من التحليل. «تشير النتائج إلى أن الذكاء الاصطناعي يمكنه جعل التحقق الرسمي، الذي كان تاريخيًا مكلفًا للغاية بالنسبة لمعظم البرمجيات، عمليًا للأنظمة الواقعية»، كما كتب الباحثون. من جانبه، قال إيرين كريت، المدير التقني لـ Signal: «بينما تتكاثر التهديدات الأمنية المرتبطة بالذكاء الاصطناعي، فإن التحقق الدقيق من تنفيذ بروتوكول Signal يمنحنا ثقة أكبر في ضمانات الخصوصية لكودنا». تنشر جوجل أيضًا المواصفات والبراهين.
