AlphaProof Code: agenci AI formalnie zweryfikowali kod Signala

10 listopada Google DeepMind przedstawił AlphaProof Code, wieloagentowy system do weryfikacji formalnej oprogramowania, i razem z nim pracę, w której agenci AI udowodnili własności bezpieczeństwa libsignal, czyli referencyjnej implementacji protokołu Signal. Dowód dotyczy skompilowanego kodu maszynowego, a nie projektu protokołu na papierze.

Co dokładnie udowodnił AlphaProof Code?

Zespół wziął niezmieniony kod Rust (libsignal v0.105.4 i bibliotekę spqr), skompilował go zwykłym kompilatorem rustc do programu na AArch64 i Linuksa, a potem dowodził twierdzeń o tym pliku wykonywalnym. To około 560 KB kodu, czyli mniej więcej 140 tys. instrukcji procesora.

Twierdzenia obejmują uzgadnianie kluczy PQXDH (to ta część Signala, która ma chronić także przed przyszłym komputerem kwantowym) oraz Triple Ratchet. Według pracy dowody ustanawiają m.in. tzw. „forward secrecy” i „post-compromise security”, czyli ochronę wiadomości wysłanych przed chwilowym przejęciem urządzenia i po nim, oraz uwierzytelnienie stron.

Liczby z pracy:

1. Około 6,5 mln linii dowodów w Lean, z czego 5,3 mln dotyczy samego pliku binarnego.
2. Pracę wykonał pięcioosobowy zespół w cztery tygodnie. Dla porównania, które przytaczają autorzy: weryfikacja mikrojądra seL4 zajęła dwadzieścia osobolat.
3. Jedna kampania dowodowa to zwykle 40 do 80 agentów na jednej maszynie przez 24 do 72 godzin.
4. Żeby uwierzyć w wynik, trzeba przeczytać około 18 tys. linii definicji i twierdzeń oraz około 8 tys. linii semantyki AArch64. Resztę sprawdza Lean.

Co ciekawe, kompilator Rusta nie należy do rzeczy, którym trzeba zaufać. Skoro dowód dotyczy kodu maszynowego, błąd kompilatora, który psułby dowodzone własności, sprawiłby, że dowód by się nie udał.

Kto pisał dowody, a kto specyfikacje?

Dowody w całości napisali agenci oparci na Gemini 4 Carbon i, jak czytamy w pracy, żaden z autorów nie napisał ani linii kodu dowodu. Ludzie zajmowali się czym innym: ustalali, co ma zostać udowodnione.

Specyfikacje powstawały w rozmowie ludzi z agentami opartymi na Gemini 4 Carbon i Claude Opus 5.5. Szkic pisał jeden agent, a recenzował go agent z innej rodziny modeli, po czym człowiek zatwierdzał wynik. Autorzy piszą wprost, że większość ich wysiłku poszła w specyfikacje, a nie w dowody.

Osobny agent, tzw. „gatekeeper”, przyjmuje dowód tylko wtedy, gdy jądro Lean go zaakceptuje, a narzędzie comparator potwierdzi, że dowodzi on dokładnie zatwierdzonej specyfikacji, której kopię trzymano poza zasięgiem agentów. Powód jest prozaiczny: agenci pod presją potrafią osłabić cel, żeby szybciej skończyć (autorzy przywołują przypadek z innego eksperymentu, w którym agent zdefiniował warunek z hipotezy jako fałsz, a reszta roju to podchwyciła).

Zespół sprawdził też, czy specyfikacje łapią prawdziwe błędy. Do kopii kodu przywrócono dwa naprawione wcześniej błędy libsignal i w obu przypadkach powstał dowód w Lean, że taki program nie spełnia twierdzeń o bezpieczeństwie.

Jest też efekt uboczny. Przenosząc do Lean modele bezpieczeństwa z literatury, zespół znalazł piętnaście luk i błędów w opublikowanej analizie Double Ratchet, a także pomyłki w zapytaniach ProVerif z innej pracy o Signalu. Formalizacja okazała się testem dla samych publikacji naukowych.

Czy to coś nowego w świecie AI?

W październiku Anthropic i Theorem pokazali weryfikację formalną 123 bibliotek open source z Claude, również na poziomie kodu maszynowego. Tam specyfikacja powstawała automatycznie i mówiła, że program nie ulegnie awarii ani nie naruszy pamięci. DeepMind cytuje tę pracę i odróżnia od niej swoją: tutaj dowodzone są własności całego protokołu w starciu z aktywnym atakującym, a specyfikację trzeba było napisać ręcznie na podstawie literatury kryptograficznej.

Czyli mamy dwa podejścia. Jedno jest szerokie i płytsze (wiele bibliotek, jedna prosta własność), drugie wąskie i głębokie (jedna biblioteka, bogate twierdzenia). Oba pojawiły się w odstępie niecałych trzech tygodni.

Ehren Kret, CTO Signala, nazwał tłumaczenie działającego kodu na poprawne twierdzenia Lean przez agentów AI dużym przełomem (cytując „a major breakthrough”).

Na co zwrócić uwagę?

Po pierwsze, na zakres. Dowód obejmuje rozmowy jeden na jeden między dwiema uczciwymi stronami. Wiadomości grupowe, stan wielu urządzeń i ataki typu side channel zostały poza nim, a sama aplikacja Signal to znacznie więcej niż libsignal.

Po drugie, na założenia. Niskopoziomowe procedury kryptograficzne nie są weryfikowane, tylko opisane kontraktami, którym trzeba zaufać, podobnie jak semantyce AArch64 i samym specyfikacjom.

Po trzecie, na komputery kwantowe. Część obliczeniowa dowodu nie daje gwarancji wobec atakującego kwantowego. Tajność uzgadniania kluczy wobec przyszłego komputera kwantowego pokazano tylko w modelu symbolicznym, który zakłada idealną kryptografię.

Wszystkie te ograniczenia autorzy sami wypisują w pracy.

FAQ

Czy AlphaProof Code można wypróbować?

Nie jako produkt. DeepMind nie podał ceny ani terminu udostępnienia. Opublikowane są specyfikacje i dowody w Lean, które każdy może sprawdzić samodzielnie.

Czy dowód dotyczy też WhatsAppa i Messengera?

Nie bezpośrednio. W pracy czytamy, że warianty protokołu Signal działają w WhatsAppie, Messengerze i Google Messages, ale twierdzenia dotyczą konkretnego pliku binarnego zbudowanego z libsignal v0.105.4.