AlphaProof Code zweryfikował kod Signala w 4 tygodnie

Google DeepMind zaprezentował AlphaProof Code - system sztucznej inteligencji, który potrafi matematycznie udowodnić, że oprogramowanie spełnia założenia bezpieczeństwa i nie zawiera błędów. Badacze przetestowali narzędzie na protokole szyfrowania komunikatora Signal. Efekt? Praca, która zwykle pochłania lata, została wykonana w ciągu zaledwie czterech tygodni.

To przełom, ponieważ wcześniejsze próby weryfikacji zatrzymywały się na etapie projektu teoretycznego - jak wynika z wpisu na blogu naukowców DeepMind, Pushmeeta Kohliego i Swarata Chaudhuriego. Tym razem udało się potwierdzić poprawność faktycznego kodu jądra kryptograficznego, który działa na urządzeniach użytkowników.

Na czym polega weryfikacja kodu przez AlphaProof Code

Proces rozpoczyna się od zdefiniowania przez ekspertów formalnych wymagań bezpieczeństwa. Następnie agenci AI zbudowani na bazie modelu Gemini Carbon tworzą dowody matematyczne w języku Lean - narzędziu służącym do formalnej weryfikacji twierdzeń. W przypadku Signala wygenerowali ich ponad sześć milionów linii.

System nie działa w pełni autonomicznie. Około jednego procenta bazy kodu zostało oznaczone do ręcznego przeglądu przez ludzi. Co istotne, agenci nie tylko pomagają tworzyć specyfikacje - samodzielnie dowodzą też, że konkretny kod je spełnia. To dwukierunkowe podejście odróżnia AlphaProof Code od wcześniejszych rozwiązań.

Test z celowo wprowadzonymi błędami

Aby sprawdzić skuteczność systemu, badacze umieścili w kodzie dwa błędy celowo. Oba zostały wykryte natychmiast. To ważny sygnał, że narzędzie faktycznie wychwytuje problemy, a nie tylko generuje pozornie poprawne dowody.

Dlaczego to ma znaczenie dla bezpieczeństwa komunikacji

CTO Signala, Ehren Kret, podkreśla, że takie podejście wzmacnia zaufanie do ochrony prywatności danych w obliczu rosnących zagrożeń ze strony AI. Formalna weryfikacja kodu kryptograficznego to coś więcej niż audyt - to matematyczny dowód, że implementacja jest wolna od określonych klas błędów.

Podejście to wzmacnia zaufanie do prywatności danych w miarę narastania zagrożeń związanych z AI.

Tradycyjne metody weryfikacji bezpieczeństwa opierają się na testach, audytach i przeglądach kodu. Wszystkie mają ograniczenia - nie wykluczają wszystkich możliwych ścieżek wykonania programu. Dowód matematyczny eliminuje tę lukę, przynajmniej w zakresie zdefiniowanych wymagań.

Plany rozwoju i kolejne zastosowania

DeepMind nie zamierza poprzestać na komunikatorach. Zespół planuje rozszerzyć metodę na systemy energetyczne oraz urządzenia medyczne, wykorzystując narzędzia takie jak CodeMender. To obszary, w których błąd w kodzie może mieć dramatyczne konsekwencje - od awarii sieci po zagrożenie życia pacjentów.

Skala wyzwania jest jednak ogromna. Signal to stosunkowo niewielki projekt w porównaniu z infrastrukturą energetyczną czy systemami medycznymi. Nie wiadomo jeszcze, jak metoda sprawdzi się przy znacznie większych i bardziej złożonych bazach kodu. Formalna weryfikacja wymaga bowiem precyzyjnego zdefiniowania wymagań - a to często trudniejsze niż samo dowodzenie.

Rola ludzi w procesie weryfikacji

Mimo zaawansowanej automatyzacji, AlphaProof Code nie eliminuje czynnika ludzkiego. Eksperci wciąż muszą określić, co dokładnie ma być udowodnione, a część kodu wymaga ręcznego przeglądu. System wspiera specjalistów, ale nie zastępuje ich odpowiedzialności za bezpieczeństwo.

Co to oznacza dla przyszłości tworzenia oprogramowania

Demonstracja na Signal pokazuje, że formalna weryfikacja kodu przestaje być domeną akademickich eksperymentów. Jeśli czas potrzebny na dowiedzenie poprawności spadnie z lat do tygodni, może to zmienić sposób, w jaki podchodzimy do bezpieczeństwa krytycznego oprogramowania.

Pozostaje pytanie o dostępność i koszty. DeepMind nie ujawnił, czy AlphaProof Code będzie dostępny publicznie ani jakie są wymagania sprzętowe. Jedno jest pewne - w czasach, gdy AI może zarówno tworzyć, jak i łamać zabezpieczenia, matematyczne dowody poprawności kodu zyskują na znaczeniu. Weryfikacja przestaje być luksusem, a staje się koniecznością.