Google DeepMind i AlphaProof Code. Agenci AI sprawdzili protokół Signal

Co dokładnie zrobił Google DeepMind

Zespół Google DeepMind sprawdził protokół Signal metodą weryfikacji formalnej. Polega ona na zapisaniu oczekiwanych właściwości oprogramowania w postaci formuł matematycznych i przeprowadzeniu dowodu, który sprawdza program komputerowy. Jeśli dowód przejdzie, dana właściwość jest spełniona dla wszystkich możliwych przypadków, także tych, których nikt nie przetestował.

Według Wired badacze udowodnili w ten sposób szereg podstawowych gwarancji kryptograficznych protokołu. Magazyn nie wymienia, które dokładnie elementy objęła analiza, a Google DeepMind do chwili sprawdzenia źródeł nie opublikował własnego opisu ani pracy naukowej. Specyfikacja i dowód mają zostać udostępnione innym zespołom zajmującym się weryfikacją.

Jak działa AlphaProof Code

AlphaProof Code to nowe narzędzie Google DeepMind oparte na agentach AI. Nazwa nawiązuje do AlphaProof, systemu tej firmy do dowodzenia twierdzeń matematycznych. Najbardziej czasochłonną częścią weryfikacji formalnej było dotąd ręczne pisanie dowodów i to ten etap agenci skracają najbardziej.

Swarat Chaudhuri z DeepMind opisuje metodę jako współpracę ludzi z AI. Agenci proponują i samodzielnie poprawiają kolejne kroki, a ludzie zatwierdzają cele i przeglądają wyniki w ważnych momentach. Badacz w rozmowie z Wired odcina się od podejścia, w którym AI sama wyznacza cele, sama pisze dowody i sama ocenia własne testy.

• Czas trwania projektu - cztery tygodnie.
• Nowe luki w sprawdzanych fragmentach - nie znaleziono.
• Test kontrolny - starsze wersje ze znanymi błędami nie przeszły weryfikacji.
• Zakres - wybrane gwarancje protokołu, bez całej aplikacji mobilnej.
• Koszt - nieujawniony, analiza wykonana nieodpłatnie jako projekt badawczy.

Jak wynik oceniają Signal i Google

Ehren Kret, dyrektor techniczny Signal, w oświadczeniu dla Wired zauważył, że wcześniejsze prace weryfikacyjne obejmowały mniejsze fragmenty kodu, a podejście DeepMind pozwala znacząco poszerzyć zakres. Badacze przyznają, że mieli ułatwiony start, bo Signal Foundation prowadziła już wcześniej własne prace nad formalną weryfikacją protokołu.

Pushmeet Kohli, wiceprezes DeepMind ds. badań, widzi zastosowanie w bankach i firmach, które muszą wykazać poprawność krytycznego oprogramowania. To deklaracja producenta, a nie zapowiedź produktu. Google odmówił komentarza w sprawie ewentualnej usługi komercyjnej.

Ograniczenia i otwarte pytania

Dowód formalny jest tak dobry jak specyfikacja, na której się opiera. Jeśli zapisane właściwości pomijają jakiś scenariusz ataku, dowód go nie obejmie. Dlatego publikacja specyfikacji ma duże znaczenie, bo pozwoli kryptografom sprawdzić, co dokładnie udowodniono.

Wynik nie został jeszcze opisany w recenzowanej pracy naukowej, a informacje pochodzą z relacji Wired i wypowiedzi badaczy. Otwarte pozostaje też pytanie o skalę i koszt. Sami badacze mówią, że do weryfikacji całego oprogramowania na świecie jest jeszcze bardzo daleko. Formalnej weryfikacji z pomocą AI próbują też inni gracze, na przykład projekt Signal Shot fundacji Beneficial AI Foundation, Signal i Lean FRO, ogłoszony w kwietniu 2026 roku.

Co to oznacza dla użytkowników w Polsce

Dla osób korzystających z WhatsAppa, Signal czy Google Messages wynik oznacza dodatkowe, niezależne potwierdzenie, że szyfrowanie end-to-end opiera się na poprawnym protokole. Nie wymaga to żadnej aktualizacji ani zmiany ustawień. Bezpieczeństwo rozmów nadal zależy też od telefonu, kopii zapasowych i tego, kto ma dostęp do odblokowanego urządzenia.

Dla polskich firm tworzących oprogramowanie ważniejszy jest kierunek. Unijny akt o cyberodporności (Cyber Resilience Act) od grudnia 2027 roku wymaga od producentów produktów z elementami cyfrowymi wykazania bezpieczeństwa w całym cyklu życia produktu. W naszej ocenie tańsza weryfikacja formalna z pomocą AI może stać się jednym ze sposobów dokumentowania tego bezpieczeństwa, zwłaszcza w bankowości, energetyce i administracji.

Źródła i metoda

Tekst opieramy na artykule Lily Hay Newman w Wired z 10 listopada 2026 roku, który odczytaliśmy w całości. Na blogu Google DeepMind ani na blogu Signal nie znaleźliśmy w chwili publikacji osobnego komunikatu. Informacje o projekcie Signal Shot pochodzą ze strony Beneficial AI Foundation. Źródła sprawdziliśmy 10 listopada 2026 roku.