Google DeepMind می‌گوید از AlphaProof Code برای بررسی ریاضیِ برخی ویژگی‌های امنیتی مهم در libsignal استفاده کرده است؛ پیاده‌سازی مرجع پروتکل پیام‌رسانی Signal. این کار چهار هفته طول کشید. به گفته DeepMind، چنین بررسی‌هایی در گذشته معمولاً سال‌ها زمان می‌برد و به گروهی از متخصصان نیاز داشت.
این سامانه پژوهشگران انسانی را با عامل‌های هوش مصنوعی همراه کرد. پژوهشگران و هوش مصنوعی به تبدیل اهداف امنیتی Signal به مشخصات ریاضی کمک کردند و افراد این مشخصات را بازبینی کردند. سپس عامل‌هایی که Gemini Carbon آن‌ها را تقویت می‌کرد، حدود 6.5 میلیون خط کد اثبات به زبان Lean تولید کردند. Lean زبان برنامه‌نویسی‌ای است که بررسی‌گر آن می‌تواند بسنجد آیا یک اثبات ریاضی از قواعد پیروی می‌کند یا نه. عامل‌ها حدود یک درصد از کد را برای بررسی انسانی علامت‌گذاری کردند.
این اثبات چه چیزهایی را پوشش می‌دهد؟
پژوهشگران کد ماشینِ کامپایل‌شده libsignal را برای دست‌دهیِ پساکوانتومی PQXDH و Triple Ratchet بررسی کردند. آن‌ها ویژگی‌های مشخصی، از جمله محرمانگی پیشرو، احراز هویت و حفاظت پس از به‌خطر‌افتادن یک دستگاه را اثبات کردند. مقاله پژوهشی می‌گوید کد با یک کامپایلر استاندارد و از Rust دست‌نخورده کامپایل شد و سپس به‌عنوان کد ماشین AArch64 بررسی شد.
این کار از اثبات امن‌بودن یک طرح انتزاعی فراتر می‌رود: تضمین‌های امنیتیِ مشخص‌شده را به کد کامپایل‌شده پیوند می‌دهد. DeepMind می‌گوید این نخستین راستی‌آزمایی صوریِ پیاده‌سازی یک پروتکل رمزنگاریِ پرکاربرد در چنین سطحی است. گروه همچنین دو باگِ رفع‌شده در گذشته را به نسخه‌ای ایزوله از کد بازگرداند؛ سامانه اثبات‌هایی تولید کرد که نشان می‌داد نسخه‌های دارای باگ، ویژگی‌های امنیتیِ تعیین‌شده را برآورده نمی‌کنند.
این اثبات محدودیت‌هایی دارد
این کار تضمین ریاضی نمی‌دهد که تمام بخش‌های Signal یا همه برنامه‌هایی که از این پروتکل استفاده می‌کنند، عاری از مشکل امنیتی باشند. اثبات، ویژگی‌های منتخب libsignal را پوشش می‌دهد، نه کل برنامه را. همچنین به مشخصات تأییدشده، بررسی‌گر Lean و قراردادهایی برای روال‌های رمزنگاریِ سطح پایین متکی است. The Register اشاره می‌کند که این نتیجه محرمانگی محاسباتیِ بایت‌های واقعی پیام را اثبات نمی‌کند؛ مقاله DeepMind از اثبات‌هایی در مدل‌های نمادین و محاسباتی سخن می‌گوید که به فرض‌هایی درباره زیربنای الگوریتم‌های رمزنگاری وابسته‌اند.
DeepMind می‌گوید مواد مربوط به راستی‌آزمایی را در دسترس دیگران قرار می‌دهد تا از آن استفاده کنند. این شرکت امیدوار است رویکرد را در حوزه‌هایی مانند میان‌افزار دستگاه‌های پزشکی و نرم‌افزار شبکه برق به کار بگیرد، اما می‌گوید گسترش این روش به پژوهش بیشتری نیاز دارد. این کار گامی به‌سوی بررسی کدهای بیشتری در دنیای واقعی است، نه مدرکی دال بر راستی‌آزمایی آن سامانه‌های دیگر.
چرا مهم است
برای کاربران Signal، این کار اثباتی را که با ماشین بررسی شده، به برخی ویژگی‌های امنیتی مشخص در پیاده‌سازی پروتکل اصلی آن اضافه می‌کند. اما ثابت نمی‌کند که کل برنامه بدون باگ است و اثبات به فرض‌هایی درباره مؤلفه‌های رمزنگاری وابسته است.
