W poprzednim artykule omawialiśmy zaawansowaną weryfikację formalną dowodów o wiedzy zerowej: jak zweryfikować instrukcję ZK. Weryfikując formalnie każdą instrukcję zkWasm, jesteśmy w stanie w pełni zweryfikować bezpieczeństwo techniczne i poprawność całego układu zkWasm. W tym artykule skupimy się na perspektywie wykrywania podatności, analizując konkretne podatności wykryte podczas procesu audytu i weryfikacji, a także doświadczenia i wnioski z nich wyciągnięte. Ogólne omówienie zaawansowanej formalnej weryfikacji łańcuchów bloków odpornych na wiedzę zerową (ZKP) można znaleźć w artykule Zaawansowana formalna weryfikacja łańcuchów bloków odpornych na wiedzę zerową.

Zanim omówimy luki w ZK, przyjrzyjmy się najpierw, w jaki sposób CertiK przeprowadza formalną weryfikację ZK. W przypadku złożonych systemów, takich jak Maszyna Wirtualna ZK (zkVM), pierwszym krokiem weryfikacji formalnej (FV) jest wyjaśnienie, co wymaga weryfikacji i jej charakteru. Wymaga to kompleksowego przeglądu projektu systemu ZK, implementacji kodu i konfiguracji testów. Proces ten pokrywa się z regularnym audytem, ​​z tą różnicą, że cele i charakter weryfikacji należy ustalić po przeglądzie. W CertiK nazywamy to audytem zorientowanym na weryfikację. Wysiłki związane z audytem i weryfikacją są często zintegrowane. Dla zkWasm przeprowadziliśmy zarówno audyt, jak i weryfikację formalną.

Czym jest podatność ZK?

Podstawową cechą systemu dowodu z wiedzą zerową jest to, że umożliwia on wykonanie krótkiego dowodu kryptograficznego obliczenia (takiego jak transakcja typu blockchain) w trybie offline lub prywatnie do walidatora dowodu z wiedzą zerową oraz sprawdzenie i potwierdzenie przez niego aby mieć pewność, że obliczenia rzeczywiście zostały wykonane zgodnie z deklarowaną sytuacją. W związku z tym luka w zabezpieczeniach ZK umożliwiłaby hakerom przesłanie fałszywych dowodów ZK używanych do udowodnienia fałszywych transakcji i zaakceptowanie ich przez osoby sprawdzające dowód ZK.

W przypadku programu ZKVM proces sprawdzający ZK obejmuje uruchomienie programu, wygenerowanie rekordu wykonania każdego kroku i konwersję danych rekordu wykonania na zestaw tabel numerycznych (proces ten nazywany jest „arytmetyzacją”). Pomiędzy tymi liczbami musi być spełniony zestaw ograniczeń (tj. „obwód”), który obejmuje równania łączące między określonymi komórkami tabeli, stałe stałe, ograniczenia wyszukiwania w bazie danych między tabelami oraz wymaganą odległość między każdą parą sąsiednich wierszy tabeli równanie wielomianowe (tj. „bramka”). Weryfikacja na łańcuchu może potwierdzić, że rzeczywiście istnieje tabela spełniająca wszystkie ograniczenia, zapewniając jednocześnie, że określone liczby w tabeli nie będą widoczne.

Tablica arytmetyczna zkWasm

Dokładność każdego ograniczenia jest krytyczna. Błąd w jakimkolwiek ograniczeniu, słabym lub brakującym, może pozwolić hakerowi na przedstawienie wprowadzającego w błąd dowodu, który wydaje się przedstawiać prawidłową realizację inteligentnej umowy, podczas gdy w rzeczywistości tak nie jest. Nieprzejrzysty charakter transakcji ZkVM wzmacnia te luki w porównaniu z tradycyjnymi maszynami wirtualnymi. W sieciach innych niż ZK szczegóły kalkulacji transakcji są publicznie rejestrowane w blokach; zkVM nie przechowuje tych szczegółów w łańcuchu. Ten brak przejrzystości utrudnia określenie konkretnych okoliczności ataku, a nawet tego, czy do ataku doszło.

Obwód ZK wykonujący reguły instrukcji zkVM jest niezwykle złożony. W przypadku zkWasm implementacja obwodu ZK obejmuje ponad 6000 linii kodu Rust i setki ograniczeń. Ta złożoność często oznacza, że ​​na odkrycie może czekać wiele luk w zabezpieczeniach.

Architektura obwodu zkWasm

Rzeczywiście, podczas audytu i formalnej weryfikacji zkWasm odkryliśmy wiele takich luk. Poniżej omawiamy dwa reprezentatywne przykłady i omawiamy różnice między nimi.

Luka w kodzie: atak polegający na wstrzykiwaniu danych Load8

Pierwsza luka dotyczy instrukcji Load8 programu zkWasm. W zkWasm odczyt pamięci sterty odbywa się poprzez zestaw instrukcji LoadN, gdzie N jest rozmiarem danych do załadowania. Przykładowo Load64 powinien odczytać 64-bitowe dane z adresu pamięci zkWasm. Load8 powinien odczytać 8 bitów danych (tj. jeden bajt) z pamięci i uzupełnić go prefiksem 0, aby utworzyć wartość 64-bitową. zkWasm wewnętrznie reprezentuje pamięć jako tablicę 64-bitowych bajtów, więc musi „wybrać” część tablicy pamięci. Wykorzystywane są do tego cztery zmienne pośrednie (u16_cells), które razem tworzą pełną 64-bitową wartość obciążenia.

Ograniczenia dla tych instrukcji LoadN są zdefiniowane w następujący sposób:

To ograniczenie jest podzielone na trzy sytuacje: Obciążenie32, Obciążenie16 i Obciążenie8. Load64 nie ma żadnych ograniczeń, ponieważ jednostka pamięci jest 64-bitowa. W przypadku Load32 kod zapewnia, że ​​górne 4 bajty (32 bity) jednostki pamięci muszą mieć wartość zero.

W przypadku Load16 górne 6 bajtów (48 bitów) jednostki pamięci musi wynosić zero.

W przypadku Load8 powinno być wymagane, aby górne 7 bajtów (56 bitów) w jednostce pamięci wynosiło zero. Niestety w kodzie tak nie jest.

Jak widać, tylko górne 9 do 16 bitów jest ograniczonych do zera. Pozostałe górne 48 bitów może mieć dowolną wartość i nadal być zamaskowane jako „odczytane z pamięci”.

Wykorzystując tę ​​lukę, haker może manipulować dowodem ZK dotyczącym prawidłowej sekwencji wykonania, powodując wykonanie instrukcji Load8 w celu załadowania tych nieoczekiwanych bajtów, co skutkuje uszkodzeniem danych. Co więcej, staranne uporządkowanie otaczającego kodu i danych może spowodować fałszywe operacje i transfery, a w rezultacie kradzież danych i zasobów. Takie fałszywe transakcje mogą przejść kontrolę zkWasm i zostać błędnie uznane przez blockchain za autentyczne.

Naprawienie tej luki jest w rzeczywistości dość proste.

Ta luka reprezentuje klasę luk ZK znanych jako „błędy w kodzie”, ponieważ powstają one podczas pisania kodu i można je łatwo naprawić za pomocą niewielkich lokalnych modyfikacji kodu. Jak zapewne się zgodzisz, luki te są również stosunkowo łatwe do zauważenia.

Luka w projekcie: sfałszowany atak powrotny

Przyjrzyjmy się kolejnej podatności, tym razem dotyczącej połączeń i zwrotów zkWasm. Wywołanie i powrót to podstawowe instrukcje maszyny wirtualnej, które pozwalają jednemu działającemu kontekstowi (takemu jak funkcja) wywołać inny i wznowić wykonywanie kontekstu wywołującego po zakończeniu jego wykonywania przez osobę wywołującą. Oczekuje się, że każde połączenie zostanie ponownie uruchomione później. Dane dynamiczne śledzone przez zkWasm podczas cyklu życia połączeń i zwrotów nazywane są „ramkami wywołań”. Ponieważ zkWasm wykonuje instrukcje sekwencyjnie, wszystkie ramki wywołań można uporządkować według czasu ich wystąpienia podczas przebiegu. Poniżej znajduje się przykład kodu wywołania/powrotu działającego na zkWasm.

Użytkownicy mogą wywołać funkcję buy_token(), aby kupić token (być może płacąc lub przekazując coś innego wartościowego). Jednym z jego podstawowych kroków jest faktyczne zwiększenie salda konta tokenowego o 1 poprzez wywołanie funkcji add_token(). Ponieważ sam tester ZK nie obsługuje struktury danych ramki wywołań, konieczne jest użycie tabeli wykonania (E-Table) i tabeli skoków (J-Table) do rejestrowania i śledzenia pełnej historii tych ramek wywołań.

Powyższy rysunek ilustruje działający proces buy_token() wywołujący add_token() oraz proces powrotu z add_token() do buy_token(). Jak widać saldo konta tokenowego wzrosło o 1. W tabeli wykonania każdy krok wykonania ma jeden wiersz, który zawiera numer ramki wywołującej w bieżącym wykonaniu, nazwę bieżącej funkcji kontekstowej (tutaj tylko dla ilustracji), numer aktualnie wykonywanej instrukcji w ramach funkcji oraz zapisany numer w tabeli. Aktualna dyrektywa (użyta tutaj wyłącznie w celach ilustracyjnych). W tabeli skoku każda ramka wywołania zajmuje jeden wiersz, a tabela przechowuje numer ramki wywołującej, nazwę kontekstu funkcji wywołującej (tylko w celu wyjaśnienia) i pozycję następnej instrukcji ramki wywołującej (tak możliwość zwrotu ramek). W obu tabelach znajduje się kolumna jops, która śledzi, czy bieżąca instrukcja jest wywołaniem/powrotem (w tabeli wykonania) i całkowitą liczbę instrukcji wywołania/powrotu, które wystąpiły w tej ramce (w tabeli skoku).

Jak można się spodziewać, każde wywołanie powinno mieć odpowiedni zwrot, a na ramkę powinno przypadać tylko jedno wywołanie i jeden powrót. Jak pokazano na powyższym rysunku, wartość jops ramki 1 w tabeli skoków wynosi 2, co odpowiada wierszom 1 i 3 w tabeli wykonania, gdzie wartość jops wynosi 1. Wszystko wydaje się w porządku jak na razie.

Ale tak naprawdę jest tu problem: chociaż jedno wywołanie i jeden powrót dadzą ramce liczbę skoków równą 2, dwa wywołania lub dwa powroty również dadzą jej liczbę 2. Posiadanie dwóch wywołań lub dwóch zwrotów na ramkę może wydawać się śmieszne, ale należy pamiętać, że właśnie to próbują osiągnąć hakerzy, przekraczając oczekiwania.

Być może jesteś teraz trochę podekscytowany, ale czy naprawdę znaleźliśmy problem?

Okazuje się, że dwa wywołania nie stanowią problemu, ponieważ ograniczenia tabeli wykonań i tabeli wywołań uniemożliwiają zakodowanie dwóch wywołań w tym samym wierszu ramki, ponieważ każde wywołanie wygeneruje nowy numer ramki, który jest bieżącym wywołaniem numer ramki plus 1.

Przypadek podwójnych zwrotów nie jest zbyt szczęśliwy: ponieważ po powrocie nie jest tworzona żadna nowa ramka, haker rzeczywiście może uzyskać tabelę wykonania i tabelę wywołań legalnej działającej sekwencji i wstrzyknąć fałszywy powrót (i odpowiednią ramkę). Na przykład poprzedni przykład wywołania metody buy_token() add_token() w tabeli wykonania i tabeli wywołań może zostać zmodyfikowany przez hakera w następującej sytuacji:

Haker wstrzyknął dwa fałszywe zwroty pomiędzy pierwotnym wywołaniem a powrotem do tabeli wykonania i dodał nowy wiersz fałszywej ramki do tabeli wywołań (oryginalny powrót i numer bieżącego kroku kolejnej instrukcji znajdują się w tabeli wykonania Należy dodać 4 ). Ponieważ każdy wiersz w tabeli wywołań ma liczbę jopsów równą 2, ograniczenie jest spełnione i moduł sprawdzający zkWasm zaakceptuje „dowód” tej fałszywej sekwencji wykonania. Jak widać na rysunku, saldo konta tokenowego wzrosło 3 razy zamiast 1 raz. Tym samym hakerowi udało się pozyskać 3 tokeny w cenie płacenia 1 tokena.

Istnieje kilka sposobów rozwiązania tego problemu. Oczywistym podejściem jest oddzielne śledzenie wywołań i zwrotów i upewnienie się, że na ramkę przypada dokładnie jedno wywołanie i jeden powrót.

Być może zauważyłeś, że jak dotąd nie pokazaliśmy ani jednej linijki kodu opisującej tę lukę. Głównym powodem jest to, że nie ma problemu z żadną linijką kodu, a implementacja kodu jest w pełni zgodna z tabelą i projektem ograniczeń. Problemem jest sam projekt, ale także rozwiązanie.

Można by pomyśleć, że ta luka powinna być oczywista, ale tak nie jest. Dzieje się tak, ponieważ istnieje przerwa między słowami „dwa wywołania lub dwa zwroty również spowodują, że liczba jopsów będzie wynosić 2” a „w rzeczywistości możliwe są dwa powroty”. To drugie wymaga szczegółowej i pełnej analizy różnych ograniczeń związanych z tabelą wykonania i tabelą wywołań, a przeprowadzenie pełnego nieformalnego rozumowania jest trudne.

Porównanie dwóch podatności

Jeśli chodzi o „lukę umożliwiającą wstrzykiwanie danych Load8” i „lukę umożliwiającą sfałszowane zwroty”, mogą one umożliwiać hakerom manipulowanie dowodami ZK, tworzenie fałszywych transakcji, oszukiwanie programów sprawdzających oraz kradzież lub porwanie. Ale ich natura i sposób, w jaki je odkryto, były zupełnie inne.

Podczas audytu zkWasm wykryto „lukę umożliwiającą wstrzykiwanie danych Load8”. Nie było to łatwe zadanie, ponieważ musieliśmy przejrzeć setki ograniczeń za pomocą ponad 6000 linii kodu Rust i setek instrukcji zkWasm. Mimo to lukę stosunkowo łatwo było wykryć i potwierdzić. Ponieważ luka ta została naprawiona przed rozpoczęciem formalnej weryfikacji, nie stwierdzono jej w trakcie procesu weryfikacji. Jeżeli podatność nie zostanie wykryta w trakcie audytu, możemy spodziewać się jej wykrycia podczas weryfikacji instrukcji Load8.

Podczas formalnej weryfikacji po audycie wykryto „lukę w zabezpieczeniach związaną z fałszywymi zwrotami”. Jednym z powodów, dla których nie wykryliśmy tego podczas audytu, jest to, że zkWasm posiada mechanizm bardzo podobny do jopów zwany „mopsem”, który śledzi instrukcje dostępu do pamięci odpowiadające danym historycznym każdej jednostki pamięci podczas działania zkWasm. Ograniczenie liczby mopów jest rzeczywiście poprawne, ponieważ śledzi tylko jeden typ instrukcji pamięci, zapisuje pamięć; a dane historyczne każdej jednostki pamięci są niezmienne i zostaną zapisane tylko raz (liczba mopów wynosi 1). Ale nawet jeśli zauważymy tę potencjalną lukę podczas audytu, bez rygorystycznego formalnego uzasadnienia wszystkich istotnych ograniczeń, nadal nie będziemy w stanie łatwo potwierdzić lub wykluczyć każdej możliwości, ponieważ żaden wiersz kodu nie jest w rzeczywistości błędem.

Podsumowując, te dwie luki należą odpowiednio do „luk w kodzie” i „luk w projektowaniu”. Luki w kodzie są stosunkowo powierzchowne, łatwiejsze do znalezienia (zły kod) i łatwiejsze do uzasadnienia i potwierdzenia; błędy projektowe mogą być bardzo subtelne, trudniejsze do znalezienia (brak „złego” kodu) oraz trudniejsze do uzasadnienia i potwierdzenia.

Najlepsze praktyki odkrywania podatności ZK

W oparciu o nasze doświadczenie w audytowaniu i formalnej weryfikacji ZKVM oraz innych łańcuchów ZK i innych niż ZK, oto kilka sugestii, jak najlepiej chronić systemy ZK:

Sprawdź kod i projekt

Jak wspomniano wcześniej, w kodzie i projekcie ZK mogą występować luki. Obydwa rodzaje podatności mogą prowadzić do naruszenia bezpieczeństwa systemów ZK, dlatego należy je wyeliminować przed uruchomieniem systemu. Jednym z problemów związanych z systemami ZK w porównaniu z systemami innymi niż ZK jest to, że wszelkie ataki są trudniejsze do ujawnienia i przeanalizowania, ponieważ szczegóły ich obliczeń nie są ujawniane ani przechowywane w łańcuchu. Zatem ludzie mogą wiedzieć, że doszło do włamania, ale od strony technicznej nie mają możliwości dowiedzenia się, jak do tego doszło. To sprawia, że ​​koszt jakiejkolwiek luki w zabezpieczeniach ZK jest bardzo wysoki. Odpowiednio, wartość zapewnienia bezpieczeństwa systemu ZK z wyprzedzeniem jest również bardzo wysoka.

Przeprowadzanie audytów i weryfikacji formalnej

Dwie luki, które tutaj przedstawiamy, zostały wykryte odpowiednio w drodze audytu i formalnej weryfikacji. Niektórym może się wydawać, że jeśli stosuje się weryfikację formalną, nie ma potrzeby przeprowadzania audytu, ponieważ wszystkie luki zostaną wykryte w drodze weryfikacji formalnej. W rzeczywistości zalecamy wykonanie obu tych czynności. Jak wyjaśniono na początku tego artykułu, wysokiej jakości formalna weryfikacja rozpoczyna się od dokładnego przeglądu, inspekcji i nieformalnego uzasadnienia kodu i projektu, a sam wysiłek ten pokrywa się z audytem. Ponadto znajdowanie i rozwiązywanie prostszych luk w zabezpieczeniach podczas audytów sprawi, że formalna weryfikacja stanie się prostsza i skuteczniejsza.

Jeśli system ZK ma być poddany zarówno audytowi, jak i formalnej weryfikacji, najlepiej jest to zrobić jednocześnie, aby audytorzy i inżynierowie weryfikacji formalnej mogli efektywnie współpracować (możliwe, że zostanie wykrytych więcej podatności, ponieważ Przedmioty i cele weryfikacji formalnej wymagają wysokiej jakości wkładu audytowego).

Jeśli Twój projekt ZK był audytowany (jak) lub audytowany wielokrotnie (jak), sugerujemy przeprowadzenie formalnej weryfikacji obwodu w oparciu o wyniki poprzednich audytów. Nasze doświadczenie z audytami i weryfikacją formalną w ZKVM i innych projektach ZK i innych niż ZK wielokrotnie pokazało, że weryfikacja często wyłapuje luki, które nie są łatwo wykryte podczas audytów. Ze względu na specyfikę ZKP, choć system ZK powinien zapewniać lepsze bezpieczeństwo i skalowalność blockchain niż rozwiązania inne niż ZK, to jego własne bezpieczeństwo i poprawność są znacznie ważniejsze niż tradycyjne systemy spoza ZK. Dlatego wartość wysokiej jakości weryfikacji formalnej systemów ZK jest również znacznie większa niż systemów innych niż ZK.

Zapewnij bezpieczeństwo obwodów i inteligentnych kontraktów

Aplikacje ZK zwykle składają się z dwóch części: obwodów i inteligentnych kontraktów. W przypadku aplikacji opartych na zkVM istnieją ogólne obwody ZkVM i aplikacje inteligentnych kontraktów. W przypadku aplikacji innych niż zkVM na drugim końcu łańcucha lub mostu L1 wdrożono specyficzne dla aplikacji obwody ZK i odpowiadające im inteligentne kontrakty.

Inteligentny kontrakt obwodu aplikacji ZK oparty na aplikacji ZKVM Aplikacja ZkVM nie oparty na łańcuchu/mostku L1 specyficznym dla aplikacji ZKVM

Nasze prace audytowe i weryfikacyjne formalne dotyczące zkWasm obejmowały wyłącznie obwody zkWasm. Z punktu widzenia ogólnego bezpieczeństwa aplikacji ZK bardzo istotny jest także audyt i formalna weryfikacja jego inteligentnych kontraktów. W końcu po włożeniu tak dużego wysiłku w zapewnienie bezpieczeństwa obwodów szkoda byłoby, gdybyśmy opuścili naszą czujność, jeśli chodzi o inteligentne kontrakty, a aplikacja zostałaby w rezultacie zagrożona.

Na szczególną uwagę zasługują dwa rodzaje inteligentnych kontraktów. Pierwszy to inteligentny kontrakt, który bezpośrednio obsługuje dowody ZK. Chociaż mogą nie być bardzo duże, ryzyko związane z nimi jest bardzo wysokie. Drugi typ to duże i średnie inteligentne kontrakty działające na platformie ZkVM. Wiemy, że czasami mogą być bardzo złożone, a najcenniejsze z nich powinny zostać poddane audytowi i weryfikacji, zwłaszcza, że ​​szczegółów ich wykonania nie można zobaczyć w łańcuchu. Na szczęście, po latach rozwoju, formalna weryfikacja inteligentnych kontraktów jest teraz praktyczna i gotowa do odpowiednich celów o dużej wartości.

Podsumujmy wpływ weryfikacji formalnej (FV) na systemy ZK i ich komponenty poprzez poniższe wyjaśnienie.