Google DeepMind wykorzystuje agentów AI do weryfikacji kluczowego kodu maszynowego Signal

Google DeepMind zaprezentowało AlphaProof Code 10 listopada 2026 r., wykorzystując zespoły agentów AI do tworzenia weryfikowanych maszynowo dowodów w Lean dla określonych właściwości bezpieczeństwa skompilowanego kodu biblioteki libsignal należącej do Signal. Pięcioosobowy zespół badawczy ukończył prace nad dowodami w ciągu czterech tygodni i udostępnił specyfikacje oraz artefakty weryfikacyjne do zewnętrznej oceny.

Prace wykroczyły poza abstrakcyjny model projektu protokołu Signal i objęły jego skompilowaną implementację. Badacze opakowali niezmodyfikowane pakiety libsignal v0.105.4 i SPQR v1.6.0 w niewielki program obsługiwany z wiersza poleceń, a następnie użyli standardowego kompilatora rustc do zbudowania statycznie linkowanego pliku wykonywalnego dla systemu Linux na architekturze AArch64. W artykule technicznym opisano wynik jako pierwsze dowody bezpieczeństwa na poziomie protokołu dla niezmodyfikowanego kodu powszechnie wdrożonej implementacji protokołu kryptograficznego.

Jak AlphaProof Code podzielił zadania

Pięciu badaczy poświęciło cztery tygodnie na prace nad dowodami, nieprzerwanie uruchamiając agentów na swoich stacjach roboczych i równolegle opracowując dowody symboliczne oraz obliczeniowe. Według artykułu agenci wygenerowali około 6,5 miliona wierszy weryfikowanego maszynowo kodu dowodów w Lean, opartego na około 26 000 wierszy zaufanych specyfikacji i semantyki AArch64.

Ludzie wybierali właściwości, rozstrzygali niejasności i kwestie kompromisów w zakresie bezpieczeństwa, sprawdzali specyfikacje oraz zachowali ostateczne prawo do zatwierdzania. Agenci oparte na Gemini 4 Carbon i Claude Opus 5.5 przygotowywały projekty tych specyfikacji i je sprawdzały, w tym z udziałem modelu z innej rodziny. Następnie zespoły agentów Gemini 4 Carbon wygenerowały cały kod dowodów; żaden z autorów nie napisał kodu dowodów. Typowe kampanie obejmowały od 40 do 80 agentów działających na jednej maszynie przez 24–72 godziny. Orkiestratorzy i liderzy zespołów koordynowali pracę agentów opracowujących dowody, a osoby pełniące funkcje architekta i integratora utrzymywały wspólną bazę dowodów.

Bramka kontrolna akceptowała dowód dopiero po sprawdzeniu go przez jądro weryfikujące Lean i potwierdzeniu przez narzędzie porównujące, że dowód odpowiada odłożonej, zatwierdzonej przez człowieka specyfikacji — wraz ze wszystkimi definicjami osiągalnymi przechodnio — i opiera się wyłącznie na standardowych aksjomatach Lean. Gdy dowody ujawniały problemy ze specyfikacją, agenci mogli proponować drobne zmiany, ale modyfikacje zaufanych założeń wymagały zgody człowieka lub polityki określonej przez użytkownika, a także były rejestrowane wraz z uzasadnieniem. Mechanizm ten ogranicza udokumentowane ryzyko związane z dowodami generowanymi przez agentów: specyfikacja może zostać pośrednio osłabiona przez jedną z jej definicji.

Zakres weryfikacji bezpieczeństwa i testy historycznych błędów

Weryfikacja objęła kod sesji indywidualnych obsługujący uzgadnianie kluczy PQXDH i wymianę wiadomości w protokole Triple Ratchet. Badacze przedstawiają dwa niezależne uzasadnienia: dziesięć twierdzeń symbolicznych opartych na wyidealizowanych założeniach kryptograficznych oraz dowód obliczeniowy ograniczający przewagę atakującego z uwzględnieniem założeń kryptograficznych i składników statystycznych. Wśród badanych właściwości znalazły się poufność w przód, która chroni wcześniejsze wiadomości po kradzieży bieżącego stanu; uwierzytelnianie; bezpieczeństwo po naruszeniu, dotyczące odzyskiwania bezpieczeństwa po włamaniu; oraz poufność uzgadniania kluczy. Argument symboliczny obejmuje ponadto poufność uzgadniania kluczy po późniejszym złamaniu Diffiego–Hellmana.

Aby sprawdzić, czy specyfikacje pozwolą wykrywać rzeczywiste błędy, zespół cofnął poprawki dotyczące dwóch wcześniej naprawionych błędów libsignal, znanych jako „słaby stan” i „mała podgrupa”, a następnie ponownie skompilował zmienione pliki binarne. W obu przypadkach uzyskano dowody w Lean na to, że twierdzenie o bezpieczeństwie symbolicznym nie zachodzi. Publiczne repozytorium weryfikacyjne oddziela materiały dotyczące dowodów obliczeniowych, symbolicznych, wspólnego pliku binarnego i semantyki AArch64 oraz opisuje, jak ponownie zbudować dowody i niezależnie je sprawdzić.

Dyrektor ds. technologii Signal, Ehren Kret, powiedział, że praca ta «daje nam jeszcze większą pewność co do gwarancji prywatności naszego kodu».

Ograniczenia i dalsze kroki

Gwarancje te w żadnym razie nie oznaczają certyfikacji wszystkich aplikacji Signal. Dotyczą przygotowanej przez badaczy kompilacji libsignal-cli działającej jako nowy proces; nie zweryfikowano generowania kluczy, obsługę wiadomości grupowych pozostawiono na przyszłość, a kanały boczne i stan wielu urządzeń nie wchodzą w zakres analizowanego scenariusza. Niskopoziomowe prymitywy kryptograficzne oraz wybrane procedury wyjściowe i biblioteczne opisano za pomocą zaufanych kontraktów. Wynik zależy więc również od tych kontraktów, zatwierdzonych specyfikacji, jądra Lean, semantyki AArch64 i założeń dotyczących prymitywów.

W artykule zaznaczono, że żaden z tych dwóch argumentów nie dowodzi odporności postkwantowej, którą ma zapewniać SPQR: twierdzenie obliczeniowe obejmuje atakujących dysponujących klasycznymi metodami, natomiast twierdzenia symboliczne dotyczące ratchetu pozwalają atakującemu wybierać klucze SPQR. Model obliczeniowy ogranicza także kilka działań atakującego, a przy dostatecznie dużej liczbie wiadomości i sesji staje się pusty. Te ograniczenia wyznaczają zakres elementów, którym zewnętrzny recenzent musi zaufać, zanim uzna dowody zweryfikowane maszynowo za gwarancję bezpieczeństwa konkretnego wdrożenia.

Badacze planują w dalszej kolejności wzmocnić twierdzenia, ograniczyć zaufaną bazę przez weryfikację większej liczby podłączonych procedur i powiązanie kontraktów kryptograficznych ze zweryfikowanymi implementacjami, a także rozszerzyć zakres prac o wiadomości grupowe, Sealed Sender i protokoły po stronie serwera. Ich celem jest weryfikowanie nowych wydań libsignal przed ich udostępnieniem, ale jest to założenie badawcze, a nie zapowiedziane wdrożenie.

Bezpośrednie znaczenie tego wyniku polega na pokazanym podziale zadań: agenci zajęli się konstruowaniem dowodów, natomiast wiarygodność nadal opiera się na specyfikacjach sprawdzonych przez ludzi i jawnych założeniach. Udostępnienie dowodów i procedur weryfikacji umożliwia zewnętrznym recenzentom sprawdzenie tych podstaw, podczas gdy badacze pracują nad włączeniem tego procesu do dalszego rozwoju libsignal.