Badacze z Google DeepMind użyli agentowej sztucznej inteligencji, by formalnie udowodnić część kluczowych gwarancji kryptograficznych protokołu Signal. Projekt, który miał charakter pilotażowy, zajął zaledwie cztery tygodnie i może być ważnym krokiem zarówno dla bezpieczeństwa komunikatorów, jak i dla samej technologii AI.

Na czym polegała weryfikacja formalna

Weryfikacja formalna to metoda, w której za pomocą matematyki sprawdza się, czy oprogramowanie działa dokładnie tak, jak zakładano. Dzięki temu można wykazać, że w analizowanym fragmencie kodu nie ma krytycznych podatności. Specjaliści od bezpieczeństwa od dawna traktują ją jako swego rodzaju świętego Graala ochrony oprogramowania.

Problem w tym, że dotąd była to praca niezwykle żmudna. Ludzie musieli opisać cechy programu, które chcą udowodnić, przełożyć ten opis na formuły, a na końcu przeprowadzić samo dowodzenie. Właśnie ten ostatni etap agentowa AI potrafi dziś znacząco skrócić. DeepMind wykorzystał do tego nowy framework o nazwie AlphaProof Code.

Co udało się ustalić

Analiza nie wykryła żadnych nowych luk w badanych fragmentach protokołu Signal. Mimo to wynik ma wartość: to kolejne niezależne potwierdzenie, że kryptografia chroniąca ogromne ilości codziennej komunikacji działa poprawnie. Z protokołu korzystają nie tylko sam Signal, lecz także Google Messages i WhatsApp.

Badacze sprawdzili też, jak narzędzie radzi sobie ze starszymi wersjami Signala, w których występowały znane, dawno naprawione błędy. AlphaProof Code poprawnie je wskazał i pokazał, że takiego protokołu nie da się formalnie zweryfikować. To ważny test, bo dowodzi, że system nie tylko „zatwierdza” kod, ale potrafi też wychwycić realne problemy.

Zespół udostępnia specyfikację i dowód opracowane na potrzeby analizy Signala, aby pomóc innym badaczom zajmującym się weryfikacją formalną.

Ograniczenia i skala

Autorzy podkreślają, że zakres pracy był ograniczony. Nie objęła ona na przykład całej aplikacji mobilnej Signal, a jedynie wybrane elementy protokołu. Niejasne jest również, jak praktyczne okaże się podejście oparte na AI przy weryfikowaniu dużych ilości kodu.

Swarat Chaudhuri, badacz z DeepMind, powiedział w rozmowie z WIRED: „Jesteśmy bardzo zadowoleni z tego wyniku, ale przed nami daleka droga, zanim będziemy w stanie przeskalować to na całe oprogramowanie świata”.

Co to oznacza dla użytkowników w Polsce

Dla przeciętnego użytkownika komunikatora nic się nie zmienia z dnia na dzień: nie trzeba niczego aktualizować ani konfigurować. Wynik jest raczej dodatkowym argumentem za zaufaniem do szyfrowania end-to-end, z którego korzystają miliony osób także w Polsce, choćby w WhatsAppie czy Signalu.

Warto jednak pamiętać, że formalna weryfikacja protokołu nie oznacza bezpieczeństwa całej aplikacji ani telefonu. Błędy mogą się pojawić w innych warstwach oprogramowania, a bezpieczeństwo zależy też od zachowania użytkownika, na przykład od ochrony urządzenia czy uważności na próby wyłudzeń. Jeśli metody takie jak ta okażą się skalowalne, w przyszłości mogą jednak podnieść poziom zaufania do oprogramowania używanego w bankowości, administracji czy infrastrukturze, także w krajach UE.

Źródło: Ars Technica – „Google DeepMind just mathematically verified key parts of Signal”