پژوهشگران گوگل دیپ‌مایند نشان داده‌اند که یک سامانه هوش مصنوعی می‌تواند ویژگی‌های امنیتی مهم پروتکل پیام‌رسانی سیگنال را به‌صورت ریاضی اثبات کند. این گروه با چارچوب تازه‌ای به نام AlphaProof Code چند تضمین رمزنگاری را به‌طور رسمی بررسی کردند. این پژوهش حدود چهار هفته طول کشید و یک پروژه تحقیقاتی بود، نه محصولی تجاری. در بخش‌هایی که بررسی شدند، باگ تازه‌ای پیدا نشد و هوش مصنوعی هنگام بررسی نسخه‌های قدیمی پروتکل، ایرادهای شناخته‌شده‌ای را که پیش‌تر رفع شده بودند به‌درستی شناسایی کرد.
راستی‌آزمایی رسمی یعنی استفاده از ریاضیات برای بررسی اینکه نرم‌افزار دقیقاً مطابق انتظار کار می‌کند و هیچ آسیب‌پذیری پنهانی ندارد. این فرایند در گذشته به متخصصانی نیاز داشت که مشخصات دقیق بنویسند، آن‌ها را به فرمول تبدیل کنند و سپس اثبات را بسازند؛ کاری پرزحمت که ممکن بود ماه‌ها طول بکشد. دیپ‌مایند با سپردن بخش زیادی از کار به هوش مصنوعی عامل‌محور (هوش مصنوعی‌ای که می‌تواند هدف‌های فرعی تعیین کند و برای رسیدن به آن‌ها تلاش کند)، این زمان را به چند هفته کاهش داد. پژوهشگران می‌گویند هوش مصنوعی همچنان در مراحل مهم به نظارت انسان نیاز داشت، اما می‌توانست خودش اثبات‌هایی پیشنهاد کند و آن‌ها را اصلاح کند.
اهرن کرت، مدیر ارشد فناوری سیگنال، خاطرنشان کرد که بررسی‌های رسمی قبلی فقط بخش‌های کوچکی از کد را پوشش می‌دادند. به گفته او، رویکرد دیپ‌مایند امکان «گسترش چشمگیر» دامنه بررسی‌ها را فراهم می‌کند. این گروه مشخصات و اثباتی را که تهیه کرده‌اند منتشر می‌کند تا گروه‌های دیگر بتوانند بر پایه آن کار کنند. با وجود امیدوارکننده بودن نتیجه، دیپ‌مایند هشدار می‌دهد که گسترش این روش به کل اپلیکیشن‌ها یا زنجیره‌های تأمین نرم‌افزار همچنان چالش‌برانگیز است و هزینه چنین راستی‌آزمایی مبتنی بر هوش مصنوعی اعلام نشده است.
چرا این موضوع اهمیت دارد
اگر هوش مصنوعی بتواند امنیت پروتکل‌های رمزنگاری را به‌طور قابل‌اعتماد اثبات کند، کاربران روزمره سیگنال، Google Messages، واتس‌اپ و اپلیکیشن‌های مشابه می‌توانند اطمینان بیشتری داشته باشند که پیام‌هایشان خصوصی می‌ماند. این فناوری در آینده می‌تواند برای کسب‌وکارهایی که به ارتباطات رمزگذاری‌شده وابسته‌اند—از جمله بانک‌ها، مراکز درمانی و روزنامه‌نگاران—تضمین‌هایی قابل استناد از نظر حقوقی فراهم کند که نرم‌افزارشان ایراد بحرانی ندارد.
چرا مهم است
برای کاربران عادی، این خبر یعنی رمزگذاری‌ای که از گفت‌وگوهایشان محافظت می‌کند اکنون با یک بررسی ریاضی دیگر هم پشتیبانی می‌شود و احتمال وجود باگ‌های پنهان کاهش می‌یابد. برای شرکت‌هایی که باید رعایت مقررات حریم خصوصی را اثبات کنند، راستی‌آزمایی با کمک هوش مصنوعی می‌تواند راه تازه‌ای برای نشان دادن امنیت، بدون ممیزی‌های دستی و زمان‌بر، باشد.
