AlphaProof Code od Google DeepMind formalnie weryfikuje protokół kryptograficzny Signalu

Google DeepMind oświadcza, że osiągnął kamień milowy w bezpieczeństwie oprogramowania, długo uznawany za wyzwanie klasy grand challenge: jego badacze poprowadzili agentów AI do matematycznego udowodnienia kluczowych właściwości bezpieczeństwa rzeczywistego kodu leżącego u podstaw protokołu Signal — technologii, która chroni miliardy prywatnych rozmów w aplikacjach takich jak Signal i Google Messages, szyfrując wiadomości end-to-end tak, że tylko nadawca i zamierzony odbiorca mogą je odczytać. Ogłoszenie opublikowano na blogu Google DeepMind; autorami są Pushmeet Kohli i Swarat Chaudhuri.

Rezultat osiągnięto dzięki AlphaProof Code — nowemu agentowemu frameworkowi do formalnej weryfikacji na bezprecedensową głębokość, łączącemu ludzką wiedzę z agentami AI. Formalna weryfikacja — matematyczne dowodzenie, że kod działa poprawnie, bez błędów — to najwyższy standard zapewnienia bezpieczeństwa, ale jest trudna i często pracochłonna. Konwencjonalne testowanie próbkują zachowanie programu; formalny dowód wyklucza błędy we wszystkich możliwych wykonaniach — poziom pewności tak kosztowny w uzyskaniu, że rzadko obejmował szeroko wdrożone oprogramowanie.

Według firmy to pierwszy przypadek użycia AI do formalnej weryfikacji szeroko wdrożonego protokołu kryptograficznego na tej głębokości. To również pierwszy przypadek formalnej weryfikacji implementacji takiego protokołu jakąkolwiek metodą — z AI lub bez.

Jak Google DeepMind zweryfikował Signal

AlphaProof Code to agentowy framework oparty na wielu LLM-ach, który dzieli pracę formalnej weryfikacji tak, jak zrobiłby to zespół badawczy: eksperci ludzcy wspólnie z AI decydują, co udowodnić, a grupa agentów AI wykonuje dowody.

Najpierw badacze Google DeepMind we współpracy z mieszanką modeli przetłumaczyli cele bezpieczeństwa Signalu na formalne specyfikacje matematyczne, przy czym każdy z nich był przeglądany przez eksperta. Następnie dowody wykonały agenty napędzane przez Gemini Carbon, generując ponad sześć milionów linii Lean — języka komputerowego, który matematycznie dowodzi poprawności kodu.

Agenty następnie poddały dowód audytowi i wskazały obszary wymagające ponownego spojrzenia człowieka — zaledwie jeden procent bazy kodu, co firma opisuje jako ogromną oszczędność czasu. Ponieważ Lean automatycznie sprawdza resztę, eksperci mogli skupić przegląd tam, gdzie osąd ludzki ma największe znaczenie.

Dowodzenie bezpieczeństwa aż do działającego kodu

Protokoły kryptograficzne stanowią fundament niemal całej komunikacji cyfrowej — od bankowości internetowej po przeglądanie sieci — a pojedyncza wada może narazić miliony osób jednocześnie. Dlatego eksperci od dziesięcioleci formalnie je analizują, choć większość weryfikacji protokołów zatrzymuje się na poziomie projektu.

Agenty Google DeepMind poszły dalej: udowodniły, że skompilowany kod spełnia kluczowe właściwości bezpieczeństwa — takie jak ochrona wiadomości przed i po tym, jak urządzenie zostanie tymczasowo skompromitowane, gwarancje znane kryptografom jako forward secrecy i post-compromise security — aż do dokładnego kodu działającego na urządzeniach. Rzeczywiste luki w zabezpieczeniach często kryją się w przestrzeni między projektem a implementacją, a zmostkowanie tej przestrzeni czyni takie dowody znacznie bardziej złożonymi.

Mimo tej złożoności proces weryfikacji zajął zaledwie cztery tygodnie — zadanie, które według firmy historycznie zajmuje zespołom ekspertów lata — potwierdzając, że podstawowy kod kryptograficzny Signalu zapewnia zabezpieczenia określone przez badaczy.

Aby potwierdzić, że AlphaProof Code potrafi odróżnić poprawny kod od wadliwego, zespół ponownie wprowadził dwa rzeczywiste, wcześniej naprawione błędy do odizolowanej wersji kodu Signalu. W obu przypadkach system wygenerował dowód zweryfikowany maszynowo, że wersja z błędami była niebezpieczna — test istotny, ponieważ weryfikator niezdolny do wykrycia wadliwego kodu dawałby fałszywe poczucie bezpieczeństwa.

W AlphaProof Code agenty AI pomagają użytkownikom napisać specyfikację, a następnie autonomicznie dowodzą, że implementacja jej spełnia. Każdy dowód jest sprawdzany przez Lean w celu weryfikacji pracy agentów.

Reakcja Signalu

„Podczas gdy wcześniejsza formalna weryfikacja koncentrowała się na mniejszych fragmentach kodu, podejście Google DeepMind umożliwia znaczącą rozszerzenie” — powiedział Ehren Kret, dyrektor techniczny (CTO) Signalu. „Wykorzystanie agentów AI do tłumaczenia działającego kodu na poprawne twierdzenia Lean to duży przełom. W miarę wzrostu zagrożeń bezpieczeństwa napędzanych przez AI rygorystyczna weryfikacja implementacji protokołu Signal daje nam jeszcze większą pewność, że nasz kod gwarantuje prywatność.”

Przyszłość bezpieczeństwa

Google DeepMind argumentuje, że pokonanie tego wieloletniego wyzwania pokazuje, jak AI może zapewnić najwyższy poziom zapewnienia bezpieczeństwa firmom, rządom i infrastrukturze krytycznej, pomagając bronić się przed cyberzagrożeniami napędzanymi przez agentów. Weryfikacja podstawowej kryptografii Signalu, zgodnie z firmą, przygotowuje grunt pod zabezpieczenie innych kluczowych systemów — od oprogramowania układowego urządzeń medycznych po oprogramowanie sieci elektroenergetycznych.

Skalowanie tych technik wymaga dalszych badań. W połączeniu z automatycznymi agentami obronnymi, takimi jak CodeMender, formalna weryfikacja może pomóc sprostać tempu i skali współczesnych cyberzagrożeń oraz tworzyć oprogramowanie z matematycznym dowodem skuteczności jego zabezpieczeń.

Google DeepMind udostępnia artefakty formalnej weryfikacji jako otwarte oprogramowanie dla społeczności, hostowane pod adresem google-deepmind.github.io/code-verification. Pełny artykuł techniczny jest dostępny jako PDF. Dla społeczności badaczy bezpieczeństwa publikacja ta umożliwia bezpośredni wgląd w dowody zweryfikowane maszynowo i metodykę — a zakres, w jakim weryfikacja na tej głębokości rozprzestrzeni się poza Signal, w systemy medyczne, przemysłowe i infrastrukturalne wymienione przez firmę, to kolejny rozwój, który warto obserwować.

Podziękowania

Badania zostały opracowane przez Swarata Chaudhuriego, Andrew Ferraiuolo, Antona Kovsharova, Teja Chajeda, Sama Schlesingera, Karna Setha, Jonathana Katza, Charlesa Suttona i Pushmeeta Kohli.

Zespół podziękował Ericowi Wieserowi za pomoc w udostępnieniu kodu jako otwartego oprogramowania, Owenowi Jonesowi za wsparcie zarządzania programem oraz Martínowi Abadiemu, Christopherowi Hensonowi, Katerinie Hristovej, Henrykowi Michalewskiemu, Jonathanowi Protzence i George'owi Tsoukalasowi za pomocne dyskusje. Badacze podziękowali również Rolfe'owi Schmidtowi, Michaelowi Rosenbergowi i Ehrenowi Kretowi z Signalu za uwagi do metodyki, a także Tulsee Doshi, Fourowi Flynnowi, Kate Olszewskiej, Alicji Huang, Andy'emu Liu, Benoitowi Schillingsowi, Ralucej Adzie Popie, Melvinowi Johnsonowi, Korayowi Kavukcuoglu, Demisowi Hassabisowi i Sundarowi Pichai za wsparcie projektu.