Osegi
Bezpieczeństwo·1 min czytania

Google DeepMind: AlphaProof Code zweryfikował bezpieczeństwo Signala

Google DeepMind twierdzi, że AlphaProof Code formalnie zweryfikował postkwantowy handshake PQXDH i Triple Ratchet w Signalu, łącząc gwarancje protokołu z kodem.

Abstract illustration of a padlock and lines of code representing formal verification of Signal's encrypted messaging protocol.
Zdjęcie: theregister
SUMODialoediviewergiftdetect

Badacze Google DeepMind zakończyli formalną weryfikację zabezpieczeń komunikatora Signal. Jak twierdzą, to pierwszy przypadek, w którym AI pomogła stworzyć dowód łączący gwarancje bezpieczeństwa na poziomie protokołu z szeroko używaną implementacją kryptograficzną.

Do pracy użyto AlphaProof Code, wieloagentowego systemu do formalnej specyfikacji i weryfikacji oprogramowania. Agent prowadzony przez człowieka pisze specyfikację w języku Lean, ocenia semantykę kodu maszynowego i tworzy dowód, który jądro Lean sprawdza względem specyfikacji. Zweryfikowano postkwantowy handshake PQXDH oraz Triple Ratchet, co potwierdza projekt libsignal pod kątem poufności z wyprzedzeniem (forward secrecy), uwierzytelniania, bezpieczeństwa po kompromitacji i tajności handshake'u.

Ludzie decydują, co dowodzić

Najpierw zespół z pomocą różnych modeli przełożył cele bezpieczeństwa Signala na matematyczną specyfikację sprawdzoną przez ludzi. Następnie agenci Gemini Carbon wygenerowali kod Lean dowodzący poprawności libsignal. Powstało 6,5 mln linii, po czym przeprowadzono audyt, który wskazał fragmenty wymagające przeglądu przez człowieka.

Wynik ma charakter teoretyczny: zakłada idealną kryptografię i nie gwarantuje obliczeniowej tajności bajtów. Mimo to jest istotnym potwierdzeniem poprawności. Prace są krokiem w stronę wyzwania, które w kwietniu ogłosiła Beneficial AI Foundation: formalnej weryfikacji protokołu i aplikacji Signal w Lean.

– To system zbudowany z myślą o współpracy człowieka i AI – powiedział Swarat Chaudhuri z Google DeepMind i University of Texas at Austin. Jego zdaniem trudnością nie jest już samo skalowanie weryfikacji, lecz ustalenie, co weryfikować.

Koszt i dalsze plany

Wcześniej weryfikacja formalna wymagała ogromnego wysiłku: mikrojądro seL4 zajęło 20 osobo-lat, a kompilator CompCert C sześć lat. Projekt Signala zajął pięcioosobowemu zespołowi cztery tygodnie i, jak przyznano, „sporo tokenów”.

Chaudhuri wskazuje, że kolejnym krokiem jest stosowanie tej technologii już na etapie projektowania oprogramowania, nie tylko w protokołach kryptograficznych. Według niego przyszłą granicą będzie nie dowodzenie, lecz specyfikacja – opisanie, przed czym kod ma być chroniony.

Aplikacje warte uwagi

SUMO: łamigłówka liczbowa

Wybierz właściwe pola, dodaj je i trafiaj w cel. Łatwa do nauczenia, trudna do opanowania. Za darmo, dla każdego wieku.

Tagi:google deepmindsignalalphaproof codeformal verificationpost-quantumlean

Więcej z tego dnia

Zobacz wszystkie →

Więcej w kategorii: Bezpieczeństwo

Zobacz wszystkie →