Google DeepMind formalnie zweryfikował część protokołu Signal — Ars Technica
Google DeepMind za pomocą agentowej sztucznej inteligencji matematycznie potwierdził szereg kluczowych gwarancji kryptograficznych protokołu Signal. Trwający cztery tygodnie projekt badawczy miał charakter demonstracyjny i wykorzystywał nowy framework AI AlphaProof Code, informuje Ars Technica.
Weryfikacja właściwości kryptograficznych
Weryfikacja formalna to matematyczne sprawdzenie, czy oprogramowanie spełnia określone właściwości i nie zawiera krytycznych podatności. Przed pojawieniem się AI proces ten zajmował dużo czasu: specjaliści musieli opisać właściwości programu, przekształcić je we wzory i zbudować matematyczny dowód.
Według publikacji agentowa AI może znacząco skrócić czas potrzebny na stworzenie takiego dowodu. Jednocześnie badanie DeepMind miało ograniczony zakres: nie obejmowało całej mobilnej aplikacji Signal, lecz dotyczyło poszczególnych części protokołu.
Podczas analizy badacze nie wykryli nowych podatności w zweryfikowanych częściach protokołu Signal. Gdy AlphaProof Code zastosowano do starszych wersji Signal ze znanymi i dawno naprawionymi problemami, system prawidłowo wykrył te podatności i wykazał, że przy ich obecności protokołu nie można formalnie zweryfikować.
Więcej aktualnych wiadomości na kanale UA.News w Telegramie Telegram.
Ograniczenia badania
W DeepMind podkreślono, że wynik jest jedynie jednym etapem szerszych prac. Skalowanie formalnej weryfikacji z pomocą AI na duże ilości kodu programowego i wszystkie systemy oprogramowania nadal wymaga dalszego rozwoju.
Badacze zaznaczyli również, że szybszą analizę ułatwiły wcześniejsze prace Signal Foundation nad formalną weryfikacją poszczególnych części kodu. DeepMind publikuje specyfikację i dowód stworzone na potrzeby analizy Signal, aby mogły zostać wykorzystane w innych badaniach nad weryfikacją formalną.
Firma przeprowadziła projekt bezpłatnie jako projekt badawczy, nie ujawniając jego kosztu. Google nie poinformował również, czy planuje uruchomić komercyjny produkt lub usługę do weryfikacji formalnej.
W DeepMind opisano to podejście jako współpracę człowieka i AI: agenci mogą pomagać na różnych etapach i poprawiać własną pracę, jednak na kluczowych etapach przewidziano wkład i kontrolę człowieka.
