Szyfrowanie Signala przeszło matematyczny dowód AI na 6,5 mln linii

Kod szyfrujący Signal ma teraz coś, czym może się pochwalić niewiele powszechnie używanych programów: matematyczny dowód, że działa zgodnie z obietnicą. Zespół agentów AI przeanalizował libsignal, bibliotekę obsługującą protokół Signal, i wykazał, że rozmowy indywidualne pozostają tajne, pozwalają potwierdzić tożsamość rozmówcy i ponownie odcinają napastnika od komunikacji po kradzieży klucza. Nie znaleziono żadnych nowych luk.

To ważne nie tylko dla użytkowników Signala. Protokół jest światowym standardem szyfrowanych od końca do końca komunikatorów, a jego odmiany chronią rozmowy w WhatsAppie, Messengerze i Google Messages. Tak szczegółowa weryfikacja rzeczywistego, wdrożonego kodu była dotąd tak czasochłonna, że prawie nikt się jej nie podejmował: jeden z największych sukcesów w tej dziedzinie, zweryfikowane jądro systemu operacyjnego, wymagał pracy dwudziestu osób przez dwadzieścia lat. To zadanie zajęło cztery tygodnie.

Narzędzie stworzone przez Google DeepMind nosi nazwę AlphaProof Code. Najpierw eksperci i modele AI przełożyli cele bezpieczeństwa Signala na formalne twierdzenia zapisane w Lean — języku programowania stworzonym z myślą o dowodach matematycznych — a każde z nich sprawdził człowiek. Następnie zespoły liczące od 40 do 80 agentów, napędzane przez Gemini Carbon, opracowywały dowody, pracując jednorazowo przez 24–72 godziny na jednej maszynie. W rezultacie powstało około 6,5 miliona linijek kodu Lean.

Nie trzeba ufać tym milionom linijek. Jądro Lean sprawdza każdy krok i odrzuca każdy niepoprawny dowód, więc nie ma znaczenia, który model go napisał ani ile razy po drodze popełnił błąd. Zaufania wymagają znacznie mniejsze elementy: około 26 tysięcy linijek specyfikacji oraz model opisujący, jak procesor ARM wykonuje kod.

Dowody obejmują elementy Signala, które chronią rozmowę: uzgadnianie kluczy PQXDH, inicjujące czat, oraz Triple Ratchet, który zmienia klucz dla każdej wiadomości, w tym warstwę postkwantową mającą stawić opór przyszłym komputerom kwantowym. W praktyce oznacza to, że kradzież aktualnych kluczy z telefonu nie pozwala odczytać starszych wiadomości, a złodziej ponownie traci dostęp, gdy obie strony wymienią świeże klucze.

Aby pokazać, że system potrafi odróżnić dobry kod od złego, badacze ponownie wprowadzili do libsignal dwa dawne błędy, które zostały już naprawione. Jeden z nich sprawiał, że biblioteka zachowywała kopię tajnego klucza, którą powinna była usunąć. W obu przypadkach AlphaProof Code wygenerował sprawdzony maszynowo dowód, że wersja z błędem była niebezpieczna.

Ograniczenia są jednak istotne. Dowód obejmuje wyłącznie rozmowy indywidualne, a DeepMind wymienia komunikację grupową jako obszar przyszłych prac. Dotyczy wersji libsignal 0.105.4, skompilowanej standardowym kompilatorem Rusta dla systemu ARM Linux wewnątrz niewielkiego programu testowego, a nie pełnych aplikacji Signal na iPhone’a, Androida czy komputery. Przyjęto, że podstawowe elementy kryptograficzne działają bezpiecznie — nie zostały one dowiedzione. Błąd w specyfikacjach zatwierdzonych przez ludzi osłabiłby gwarancję, a WhatsApp i pozostałe aplikacje korzystają z własnych wersji protokołu, więc wynik nie odnosi się do nich automatycznie. Google odmówiło również przekazania serwisowi Wired informacji o kosztach analizy i o tym, czy planuje oferować ją jako usługę.

Signal z zadowoleniem przyjął ten wynik. „W obliczu rosnących zagrożeń dla bezpieczeństwa ze strony AI rygorystyczna weryfikacja implementacji protokołu Signal daje nam jeszcze większą pewność co do gwarancji prywatności naszego kodu” — powiedział w oświadczeniu Ehren Kret, dyrektor ds. technologii w Signal. Swarat Chaudhuri, badacz z DeepMind, zachował większą ostrożność. W rozmowie z Wired stwierdził, że do wykorzystania tej metody „w odniesieniu do całego oprogramowania na świecie” jest „jeszcze daleka droga”.

Użytkownicy Signala nie muszą niczego instalować ani zmieniać żadnych ustawień. Dowód dotyczy kodu, który już znajduje się w aplikacji.

DeepMind opublikowało wyniki 10 listopada wraz z artykułem technicznym, a specyfikacje i dowody udostępniło jako otwarte oprogramowanie w serwisie GitHub. Projekt dotyczący Signala opisuje jako ważny krok w stronę ambitnego wyzwania z zakresu weryfikacji formalnej, ogłoszonego w kwietniu. Wśród systemów, które chce poddać sprawdzeniu w następnej kolejności, wymienia oprogramowanie układowe urządzeń medycznych i systemów energetycznych.

Chaudhuri wyznaczył też granicę temu, jak dużą część pracy powinny wykonywać maszyny. „Nie chcemy świata w stylu vibe, w którym AI wyznacza cele i AI tworzy dowody” — powiedział Wired. To ludzie nadal decydują, co uznaje się za bezpieczne; AI ma jedynie to udowodnić.

Tagi: cyberbezpieczeństwo, Google DeepMind, AlphaProof Code, libsignal, Signal, szyfrowanie end-to-end