AlphaProof Code od Google DeepMind weryfikuje libsignal z Signala

Dowód zamiast testów

Zwykle bezpieczeństwo oprogramowania sprawdza się testami i audytami, co pozwala stwierdzić, że nie znaleziono błędów, ale nie, że ich nie ma. Weryfikacja formalna dowodzi matematycznie, że kod nie może naruszyć określonych właściwości, lecz jest bardzo kosztowna: weryfikacja jądra seL4 w 2009 roku pochłonęła równowartość dwudziestu lat pracy jednej osoby.

W AlphaProof Code ludzie decydują, co należy udowodnić, a agenci to robią. Badacze określili właściwości na podstawie prac naukowych o Signalu. Agenci, korzystając z modelu Gemini 4 Carbon, napisali około 6,5 mln linii dowodów w języku Lean, którego weryfikator automatycznie sprawdza każdy krok. Żaden badacz nie napisał własnoręcznie ani linii dowodu.

Dowody dotyczą mechanizmu „ratchet”, który stale odnawia klucze szyfrujące. Według artykułu technicznego atakujący, który wykradnie klucze z telefonu, nie odczyta wcześniejszych wiadomości, bo każda jest szyfrowana kluczem pochodzącym z poprzedniego, a ten jest usuwany. Rozmowa znów staje się bezpieczna, gdy obie strony wymienią nowe wiadomości, i nikt nie może podszyć się pod rozmówcę. Aby sprawdzić metodę, badacze przywrócili dwa dawno naprawione błędy libsignal, a system wykazał, że te wersje nie spełniają gwarancji.

Ograniczenia

CTO Signala Ehren Kret nazwał wynik „dużym krokiem naprzód”. Google zaznacza jednak, że dowód obejmuje tylko rozmowy dwuosobowe, zakłada poprawność podstawowych elementów kryptograficznych bez ich weryfikacji i dotyczy wersji testowej pod Linuksem, a nie aplikacji mobilnych.

Autorzy podsumowują, że skoro dowody tanieją, trudnym pytaniem staje się to, co warto dowodzić.