Współzałożyciel Ethereum, Vitalik Buterin, nie wierzy, że ulepszanie sztucznej inteligencji sprawi ostatecznie, iż cyberbezpieczeństwo stanie się zasadniczo nie do wygrania.
Buterin jest przekonany, że ostatecznie może stać się coś przeciwnego: AI może dać obrońcom narzędzia potrzebne do tworzenia oprogramowania, które jest znacznie trudniejsze do wykorzystania w pierwszej kolejności.
„Coraz częściej spotykane jest stanowisko, że hakerstwo z użyciem AI oznacza, że cyberbezpieczeństwo jest skazane na porażkę. Nie zgadzam się” – napisał Buterin w długim i charakterystycznie rzeczowym wpisie w mediach społecznościowych w środę w sieci X.
Zdaniem współzałożyciela Ethereum cyberbezpieczeństwo powinno naturalnie faworyzować obrońców, gdy programiści zaczną w pełni wykorzystywać weryfikację formalną.
Buterin powiązał to przekonanie także bezpośrednio z własną ekspozycją na kryptowaluty, ujawniając, że około 90% jego wartości netto pozostaje w krypto.
Twierdził, że każdy, kto nadal posiada znaczne ilości kryptowalut, domyślnie zakłada, że można zbudować wystarczająco bezpieczne systemy cyfrowe pomimo coraz bardziej wyrafinowanych atakujących.
„Jeśli AI potrafi udowodnić równania Naviera-Stokesa i WTF, to AI potrafi udowodnić stwierdzenie »ten program jest bezpieczny« jako twierdzenie matematyczne” – napisał Buterin, odnosząc się do problemu równań Naviera-Stokesa i Wielkiego Twierdzenia Fermata.
Jego argument opiera się na weryfikacji formalnej, metodzie matematycznego wykazywania, że oprogramowanie spełnia określone właściwości.
Buterin obszernie omawiał ten sam pomysł w swoim majowym eseju, w którym opisał wspomaganą przez AI weryfikację formalną jako niezwykle przełomowe narzędzie dla oprogramowania o krytycznym znaczeniu dla bezpieczeństwa. Jednak udowodnienie, że takie oprogramowanie jest bezpieczne, może okazać się trudne.
Problem z definicją
Buterin użył aplikacji do szyfrowanej komunikacji Signal jako przykładu, aby pokazać, dlaczego może to być trudne.
Atakujący może próbować fałszować wiadomości, uniemożliwiać ich dotarcie, odtwarzać stare wiadomości, przejąć serwer, manipulować procesem używanym do odkrycia klucza publicznego innego użytkownika lub wykorzystać lukę w systemie operacyjnym.
Inne problemy mogą wynikać z uszkodzonych baz danych, złośliwych bibliotek, kompilatorów, a nawet wycieków informacji na poziomie sprzętu.
Nawet jeśli treść rozmowy pozostaje zaszyfrowana, atakujący może nadal dowiedzieć się, kto się komunikuje. W rezultacie matematyczna definicja tego, co faktycznie oznacza „bezpieczny”, sama w sobie może stać się niezwykle skomplikowana.
„Więc ... nawet definicje mogą mieć ponad tysiąc linii kodu i wymagają głębokiego, starannego przemyślenia, aby je opracować” – napisał Buterin.
Atakujący i obrońca
Bez wątpienia bardziej zdolne systemy AI mogłyby ułatwić znajdowanie luk w zabezpieczeniach.
Jednak ta sama poprawa w rozumowaniu maszynowym mogłaby również dramatycznie obniżyć koszt formalnego udowodnienia, że oprogramowanie zachowuje się zgodnie ze starannie skonstruowanymi specyfikacjami bezpieczeństwa.
Obie strony będą miały AI.
