Współzałożyciel Ethereum Vitalik Buterin twierdzi, że wzrost hakowania wspieranego przez AI nie czyni cyberbezpieczeństwa walką bez szans na wygraną, wskazując zamiast tego na weryfikację formalną jako sposób na udowodnienie bezpieczeństwa oprogramowania. Zamiast polegać na odkrywaniu podatności, argumentuje, deweloperzy mogą matematycznie wykazać, że programy spełniają zdefiniowane wymagania bezpieczeństwa.

W wpisie na blogu z 18 maja, który udostępnił na X, Buterin stwierdził, że AI mogłaby uczynić taką weryfikację praktyczną na dużą skalę — podejście, które według niego ma największe znaczenie dla systemów krytycznych, w tym kryptografii, protokołów komunikatów i oprogramowania blockchain.

Bezpieczeństwo musi zostać zdefiniowane, zanim będzie można je udowodnić

Buterin powiedział, że udowodnienie bezpieczeństwa programu wymaga najpierw zdefiniowania, co bezpieczeństwo właściwie oznacza. Przywołał zaszyfrowany komunikator Signal jako przykład, zaznaczając, że samo szyfrowanie nie obejmuje wszystkich kwestii bezpieczeństwa. Kompletna definicja może musieć uwzględniać fałszowanie wiadomości, błędy dostarczania, odtwarzane wiadomości, zhakowane urządzenia i wycieki kluczy.

Sprzęt dodaje kolejne komplikacje. Sygnały fizyczne mogą przeciekać informacjami, a szczegóły takie jak rozmiar wiadomości, tożsamość nadawcy i czas wysłania mogą same w sobie być ujawniające. Razem te uwagi mogą sprawić, że definicje bezpieczeństwa przekroczą 1 000 linii kodu. Mimo to Buterin argumentował, że definicje pozostają mniejszym celem do weryfikacji niż sama implementacja.

Weryfikacja formalna obejmuje cały program

Weryfikacja formalna to nie nowy pomysł: od dawna jest stosowana w dziedzinach krytycznych dla bezpiestwa, takich jak oprogramowanie lotnicze i medyczne, gdzie koszt awarii jest wysoki, ale wymagany wysiłek sprawiał, że była rzadkością w rozwoju oprogramowania ogólnego przeznaczenia. Historycznie deweloperzy weryfikowali jedynie fragmenty, które sami uznali za krytyczne dla bezpieczeństwa, głównie dlatego, że weryfikacja wymagała znacznych nakładów. Buterin argumentował, że AI mogłaby zmienić tę równania, czyniąc weryfikację całego programu bardziej praktyczną i rozszerzając zakres na bazy danych, warstwy sieciowe, cache i inne komponenty.

Oprawił cel jako odmienny od tradycyjnego modelu, w którym obrońcy ścigają się z atakującymi w odkrywaniu podatności. W jego podejściu oprogramowanie staje się bardziej odporne poprzez udowodnienie, że spełnia wymagania bezpieczeństwa. Definicje mogą być również łączone, gdy różne grupy ustalają oddzielne wymagania, powiedział, a tam gdzie dwie definicje nie mogą współistnieć, deweloperzy mogą wyizolować leżący u podstaw konflikt projektowy. Przyznał jednak, że niektóre interfejsy użytkownika pozostają trudniejsze do obsłużenia.

Złożone potrzeby weryfikacyjne oprogramowania Ethereum

Buterin wskazał protokoły przesyłania komunikatów, piaskownice, SNARK-i — kompaktowe dowody kryptograficzne, że obliczenie zostało wykonane poprawnie — oraz w pełni homomorficzne szyfrowanie, które pozwala na obliczenia bezpośrednio na zaszyfrowanych danych, jako obszary, w których rozróżnienie między definicjami a implementacjami może mieć znaczenie. Powiązał to podejście bezpośrednio z kierunkiem rozwoju Ethereum, mówiąc, że blockchainy potrzebują silniejszego bezpieczeństwa oprogramowania, szczególnie w systemach dążących do skalowalności i prywatności.

Kontekst podkreśla stawkę: oprogramowanie blockchain jest open-source, a sieci, które obsługuje, bezpośrednio przechowują aktywa, więc ten sam kod znajduje się na oczach atakujących i obrońców — warunki, w których gwarancje niezależne od tego, kto pierwszy znajdzie lukę, mają szczególną wagę.

Jego argument koncentruje się na weryfikacji matematycznej, a nie tylko na odkrywaniu podatności. Weryfikacja, jak powiedział, musi wykraczać poza wybrane fragmenty kodu: definicja wymaga starannej pracy, podczas gdy implementacja pozostaje poddana formalnemu sprawdzaniu. Jego zdaniem AI mogłaby udźwignąć skalę tego procesu, obejmującego bazy danych, sieci, cache i inne komponenty. Pytaniem do obserwacji jest, czy narzędzia wspomagane przez AI przeniosą weryfikację całego programu do rutynowej praktyki na skalę produkcyjną, w tym interfejsy użytkownika, które wskazał jako najtrudniejsze przypadki.