محققان گوگل دیپمایند (Google DeepMind) با بهرهگیری از هوش مصنوعی عاملمحور (Agentic AI)، موفق به اثبات ریاضی یا همان «تایید رسمی» (Formal Verification) تعدادی از تضمینهای رمزنگاری (Cryptographic) کلیدی در پروتکل سیگنال (Signal Protocol) شدهاند. این پیشرفت، نقطه عطفی برای حوزه رمزنگاری و همچنین خودِ فناوری هوش مصنوعی محسوب میشود.
این پروژه که به عنوان یک اثبات مفهوم (Proof-of-Concept) تنها در چهار هفته انجام شد، از دو جنبه حائز اهمیت است: نخست، این کار یک اعتبارسنجی مستقل برای رمزنگاریهایی است که حجم عظیمی از ارتباطات جهانی را در پلتفرمهایی مانند اپلیکیشن سیگنال، گوگل مسجز (Google Messages) و واتساپ (WhatsApp) محافظت میکنند. دوم، این پروژه توانمندیهای تایید رسمی گوگل دیپمایند را با استفاده از چارچوب جدید هوش مصنوعی به نام AlphaProof Code به نمایش میگذارد.
تایید رسمی (Formal Verification) مدتهاست که به عنوان «جام مقدس» امنیت نرمافزار شناخته میشود؛ زیرا از ریاضیات برای بررسی و تایید این موضوع استفاده میکند که آیا نرمافزار دقیقاً طبق هدف طراحیشده عمل میکند یا خیر، و به عبارت دیگر، آیا فاقد آسیبپذیریهای (Vulnerabilities) حیاتی هست یا نه. پیش از عصر هوش مصنوعی، توصیف ویژگیهای نرمافزار، تبدیل آنها به فرمولهای ریاضی و سپس توسعه اثبات، فرآیندی بسیار زمانبر بود. اما هوش مصنوعی عاملمحور میتواند این زمان را به شدت کاهش دهد.
تحلیلهای انجام شده توسط دیپمایند، هیچ آسیبپذیری جدیدی در بخشهای بررسیشده از پروتکل سیگنال پیدا نکرد. با این حال، زمانی که محققان از AlphaProof Code برای بررسی نسخههای قدیمیتر سیگنال استفاده کردند که حاوی آسیبپذیریهای شناختهشده و اصلاحشده بودند، ابزار مذکور بهدرستی آنها را شناسایی کرد. این موضوع نشاندهنده دقت بالای این روش در تشخیص نقصهای ساختاری است.
اگرچه این تحلیل محدود بود و کل اپلیکیشن موبایل سیگنال را شامل نمیشد، اما گام مهمی در جهت مقیاسپذیری این فناوری برای کل زنجیره تأمین نرمافزار (Software Supply Chain) و زیرساختهای حیاتی است. در آینده، توانایی تایید رسمی تمام پایگاههای کد میتواند اطمینان خاطر بالایی برای بخشهایی مانند بانکها و شرکتهای حساس فراهم کند.
در نهایت، رویکرد مورد استفاده در این تحقیق بر پایه همکاری انسان و هوش مصنوعی (Human-AI Collaboration) استوار است. هدف این نیست که هوش مصنوعی بهطور کاملاً خودکار اهداف و اثباتها را تولید کند، بلکه ایجاد یک تعامل میان این دو است که در آن عاملهای هوش مصنوعی در مراحل مختلف مشارکت و خوداصلاحی انجام میدهند، در حالی که نظارت و بازبینی انسانی در نقاط کلیدی حفظ میشود.