AlphaProof Code sprawdził matematycznie kluczowe elementy protokołu Signal

Kryptografia stojąca za Signalem, Google Messages i WhatsAppem po raz kolejny przeszła niezależny test — tym razem nie w laboratorium bezpieczeństwa, lecz na gruncie czystej matematyki. Badacze z Google DeepMind wykorzystali agentowe narzędzia AI, by formalnie zweryfikować szereg kluczowych gwarancji protokołu Signal. Cały eksperyment, pomyślany jako dowód koncepcji, zajął zaledwie cztery tygodnie i został opisany przez WIRED, a następnie przedrukowany przez Ars Technicę.

Na czym polega formalna weryfikacja? To podejście, w którym zamiast testować oprogramowanie na wyrywkowych przypadkach, opisuje się jego pożądane właściwości w języku logiki, a następnie dowodzi matematycznie, że kod je spełnia. Od dekad uchodzi za swego rodzaju święty Graal bezpieczeństwa — daje bowiem gwarancję, że w kodzie nie kryje się żadna istotna luka, a nie jedynie nadzieję, że testy jej nie wykryły. Problem w tym, że przygotowanie specyfikacji, przełożenie jej na formuły i wyprowadzenie dowodu było dotąd zajęciem niezwykle pracochłonnym, dostępnym tylko dla nielicznych zespołów i wąskich fragmentów kodu.

Tu właśnie wkracza nowy framework DeepMind o nazwie AlphaProof Code. Agentowe AI znacząco skraca najbardziej żmudny etap pracy — samo konstruowanie dowodu — pozostawiając człowiekowi nadzór nad celami i kluczowymi decyzjami. Jak ujął to Swarat Chaudhuri, badacz DeepMind, nie chodzi o „vibe world”, w którym AI samo wyznacza cele, samo generuje dowody i samo się ocenia. Istnieje tu pole dla współpracy człowieka z maszyną, w której agent poprawia własne błędy, ale w newralgicznych momentach nadal potrzebna jest ludzka recenzja.

Wyniki są obiecujące z dwóch powodów. Po pierwsze, analiza nie wykryła nowych podatności w zbadanych fragmentach protokołu, co stanowi dodatkowe, niezależne potwierdzenie bezpieczeństwa rozwiązań chroniących komunikację milionów użytkowników. Po drugie — i to być może ciekawsze — gdy badacze puścili AlphaProof Code na starsze wersje Signala, zawierające znane i dawno naprawione błędy, narzędzie poprawnie je zidentyfikowało i wykazało, że takiego protokołu nie da się formalnie zweryfikować. To test, który odróżnia realną analizę od efektownej demonstracji.

DeepMind nie działał jednak w pustce. Signal Foundation prowadziła wcześniej własne prace nad weryfikacją formalną, co dało badaczom solidny punkt wyjścia. Ehren Kret, dyrektor techniczny Signala, podkreśla, że o ile wcześniejsze wysiłki obejmowały mniejsze fragmenty kodu, o tyle podejście Google pozwala na istotne rozszerzenie skali. W obliczu rosnących zagrożeń napędzanych przez AI rigorowe potwierdzenie implementacji protokołu ma dawać większą pewność co do prywatności użytkowników. Zespół udostępnił opracowaną specyfikację i dowód, by ułatwić dalsze prace innym.

Entuzjazm trzeba jednak studzić. Analiza nie objęła całej aplikacji mobilnej Signala, a jedynie wybrane właściwości protokołu. Sami badacze mówią wprost: to jeden kamień milowy, a droga do weryfikacji „całego oprogramowania świata” jest jeszcze długa. Otwarte pozostaje też pytanie o koszty — DeepMind wykonał pracę bezpłatnie w ramach projektu badawczego i nie ujawnił, ile ona kosztowała, ani czy planuje komercyjny produkt. Wizja, w której banki i inne firmy mogą po prostu „udowodnić” swoje właściwości bezpieczeństwa, brzmi kusząco, ale na razie pozostaje w sferze obietnic.

Podsumowanie: Weryfikacja formalna z pomocą agentowego AI przestaje być teoretyczną ciekawostką i zaczyna wchodzić do praktyki — czterotygodniowy projekt DeepMind wokół Signala jest tego najlepszym dowodem. Zanim jednak matematyczne dowody poprawności staną się standardem w całym przemyśle, trzeba rozwiązać problemy skali, kosztów i zakresu. To ważny krok, ale nie meta.