W tej serii blogów na temat zaawansowanej formalnej weryfikacji dowodów z wiedzą zerową omówiliśmy sposób weryfikacji instrukcji ZK oraz dogłębną analizę dwóch podatności ZK. Jak wynika z publicznych raportów i baz kodowych, formalnie weryfikując każdą instrukcję zkWasm, znaleźliśmy i naprawiliśmy każdą podatność, co pozwoliło nam w pełni zweryfikować bezpieczeństwo techniczne i poprawność całego obwodu zkWasm.
Chociaż pokazaliśmy proces weryfikacji instrukcji zkWasm i przedstawiliśmy wstępne koncepcje powiązanego projektu, czytelnicy zaznajomieni z weryfikacją formalną mogą być bardziej zainteresowani zrozumieniem weryfikacji zkVM z innymi mniejszymi systemami ZK lub innymi typami unikalności VM z kodem bajtowym NA. W tym artykule szczegółowo omówimy niektóre kwestie techniczne napotkane podczas sprawdzania poprawności podsystemu pamięci zkWasm. Pamięć jest najbardziej unikalną częścią zkVM i jej obsługa ma kluczowe znaczenie dla wszystkich innych weryfikacji zkVM.
Weryfikacja formalna: maszyna wirtualna (VM) kontra maszyna wirtualna ZK (zkVM)
Naszym ostatecznym celem jest weryfikacja poprawności zkWasm, która jest podobna do twierdzenia o poprawności zwykłych interpreterów kodu bajtowego (VM, takich jak interpreter EVM używany przez węzły Ethereum). Oznacza to, że każdy etap wykonania interpretera odpowiada etapowi prawnemu opartemu na semantyce operacyjnej języka. Jak pokazano na poniższym rysunku, jeśli bieżący stan struktury danych interpretera kodu bajtowego to SL i stan ten jest oznaczony jako stan SH w specyfikacji wysokiego poziomu maszyny Wasm, to gdy interpreter przejdzie do stanu SL', nie będzie musi być odpowiednim prawnym stanem wysokiego poziomu SH', a specyfikacja Wasm stanowi, że SH musi przejść do SH'.
Podobnie zkVM ma podobne twierdzenie o poprawności: każdy nowy wiersz w tabeli wykonania zkWasm odpowiada krokowi prawnemu opartemu na semantyce operacyjnej języka. Jak pokazano na poniższym rysunku, jeśli bieżący stan wiersza struktury danych w tabeli wykonania to SR, a stan ten jest wyrażony jako stan SH w specyfikacji wysokiego poziomu maszyny Wasm, to stan następnego wiersza tabeli wykonania SR' musi odpowiadać stanowi wysokiego poziomu SH' , a specyfikacja Wasm stanowi, że SH musi przejść do SH'.
Można zauważyć, że specyfikacja stanów wysokiego poziomu i kroków Wasm jest spójna zarówno w VM, jak i zkVM, więc może opierać się na wcześniejszych doświadczeniach weryfikacyjnych interpreterów lub kompilatorów języków programowania. Cechą szczególną weryfikacji zkVM jest rodzaj struktury danych, która stanowi stan niskiego poziomu systemu.
Po pierwsze, jak powiedzieliśmy w poprzednim poście na blogu, dowód zk jest zasadniczo operacją na liczbach całkowitych modulo dużych liczb pierwszych, podczas gdy specyfikacja Wasm i normalny interpreter obsługują 32-bitowe lub 64-bitowe liczby całkowite. Większość implementacji zkVM się z tym wiąże, dlatego podczas weryfikacji należy również wykonać odpowiednie przetwarzanie. Jest to jednak problem „lokalny”: każda linia kodu staje się bardziej złożona ze względu na operacje arytmetyczne, które musi wykonać, ale ogólna struktura kodu i dowodu nie ulega zmianie.
Kolejną istotną różnicą jest sposób obsługi struktur danych o dynamicznych rozmiarach. W zwykłym interpreterze kodu bajtowego pamięć, stos danych i stos wywołań są implementowane jako modyfikowalne struktury danych. Podobnie specyfikacja Wasm reprezentuje pamięć jako typ danych za pomocą metod get/set. Na przykład interpreter EVM Getha ma typ danych „Memory”, który jest zaimplementowany jako tablica bajtów reprezentująca pamięć fizyczną i jest zapisywany i odczytywany za pomocą metod „Set 32” i „GetPtr”. Aby zaimplementować instrukcję przechowywania pamięci, Geth wywołuje „Set 32”, aby zmodyfikować pamięć fizyczną.
func opMstore(pc *uint 64, interpreter *EVMInterpreter, zakres *ScopeContext) ([]bajt, błąd) {
// pop wartość stosu
mStart, wartość := zakres.Stack.pop(), zakres.Stack.pop()
zakres.Memory.Set 32(mStart.Uint 64(), val)
zwróć zero, zero
}
W dowodzie poprawności powyższego interpretera udowodniliśmy, że jego stan wysokiego poziomu i stan niskiego poziomu dopasowują się do siebie po przypisaniu wartości pamięci konkretnej w interpreterze i pamięci abstrakcyjnej w specyfikacji. Jest to stosunkowo łatwe.
Jednak w przypadku zkVM sytuacja staje się bardziej skomplikowana.
Tabela pamięci i warstwa abstrakcji pamięci zkWasm
W zkVM w tabeli wykonawczej znajdują się kolumny dla danych o stałym rozmiarze (podobnie jak rejestry w procesorze), ale nie można jej używać do obsługi struktur danych o dynamicznych rozmiarach, które są implementowane poprzez przeglądanie tabel pomocniczych. Tabela wykonań zkWasm posiada kolumnę EID, której wartości wynoszą 1, 2, 3... oraz posiada dwie tablice pomocnicze, tablicę pamięci i tabelę skoków, które służą odpowiednio do reprezentowania danych pamięci i stosu wywołań.
Poniżej znajduje się przykład wdrożenia programu wypłat:
saldo int, kwota;
unieważnij główny () {
saldo = 100;
ilość = 10;
saldo -= kwota; // wycofać
}
Zawartość i struktura tabeli wykonania są dość proste. Ma 6 kroków wykonawczych (EID 1 do 6), każdy krok ma linię zawierającą kod operacji (kod operacji) oraz, jeśli instrukcja jest odczytem lub zapisem pamięci, jej adres i dane:
Każdy wiersz w tabeli pamięci zawiera adres, dane, początkowy i końcowy EID. Początkowy EID to EID etapu wykonania, który zapisuje te dane pod ten adres, a końcowy EID to EID następnego kroku wykonania, który zapisze ten adres. (Zawiera również licznik, który omówimy szczegółowo później.) W przypadku obwodu instrukcji odczytu pamięci Wasm wykorzystuje on ograniczenie wyszukiwania, aby upewnić się, że w tabeli znajduje się odpowiedni wpis, taki, że EID instrukcji odczytu znajduje się w zakres od początku do końca Wewnątrz. (Podobnie każdy wiersz tabeli skoków odpowiada ramce stosu wywołań, a każdy wiersz jest oznaczony identyfikatorem EID kroku instrukcji wywołania, który go utworzył.)
Ten system pamięci bardzo różni się od zwykłego interpretera maszyny wirtualnej: tablica pamięci nie jest pamięcią zmienną, która jest stopniowo aktualizowana, ale zawiera historię wszystkich dostępów do pamięci w trakcie śledzenia wykonania. Aby ułatwić pracę programistom, zkWasm udostępnia warstwę abstrakcji, realizowaną poprzez dwie wygodne funkcje wejściowe. Oni są:
alloc_memory_table_lookup_write_cell
I
Alloc_memory_table_lookup_read_cell
Jego parametry są następujące:
Na przykład kod implementujący instrukcje przechowywania pamięci w zkWasm zawiera wywołanie funkcji „write alloc”:
niech memory_table_lookup_heap_write1 = alokator
.alloc_memory_table_lookup_write_cell_with_value(
„zapisz zapis res 1”,
kreator_ograniczeń,
eid,
przesuń |____| const_from!(LocationType::Heap jako użytkownik 64),
przesuń |metę| loading_block_index.expr(meta), // adres
przesuń |____| const_from!( 0), // jest 32-bitowy
przesuń |____| const_from!( 1), // (zawsze) włączone
);
niech store_value_in_heap1 = memory_table_lookup_heap_write1.value_cell;
Funkcja `alloc` jest odpowiedzialna za obsługę ograniczeń wyszukiwania pomiędzy tabelami i ograniczeń arytmetycznych wiążących bieżący `eid` z wpisami tabeli pamięci. Dzięki temu programiści mogą traktować te tabele jak zwykłą pamięć, a wartość `wartość_magazynu_w_stercie1` została przypisana do adresu `load_block_index` po wykonaniu kodu.
Podobnie instrukcje odczytu pamięci są implementowane przy użyciu funkcji `read_alloc`. W powyższej przykładowej sekwencji wykonania istnieje ograniczenie odczytu dla każdej instrukcji ładowania i ograniczenie zapisu dla każdej instrukcji przechowywania, a każde ograniczenie jest spełniane przez wpis w tablicy pamięci.
mtable_lookup_write(wiersz 1.eid, wiersz 1.adres_sklepu, wiersz 1.wartość_sklepu)
⇐ (wiersz 1.eid= 1 ∧ wiersz 1.store_addr=saldo ∧ wiersz 1.store_value= 100 ∧ ...)
mtable_lookup_write(wiersz 2.eid, wiersz 2.adres_sklepu, wiersz 2.wartość_sklepu)
⇐ (wiersz 2.eid= 2 ∧ wiersz 2.adres_sklepu=ilość ∧ wiersz 2.wartość_sklepu= 10 ∧ ...)
mtable_lookup_read(wiersz 3.eid, wiersz 3.load_addr, wiersz 3.load_value)
⇐ ( 2
mtable_lookup_read(wiersz 4.eid, wiersz 4.load_addr, wiersz 4.load_value)
⇐ ( 1
mtable_lookup_write(wiersz 6.eid, wiersz 6.adres_sklepu, wiersz 6.wartość_sklepu)
⇐ (wiersz 6.eid= 6 ∧ wiersz 6.store_addr=saldo ∧ wiersz 6.store_value= 90 ∧ ...)
Struktura weryfikacji formalnej powinna odpowiadać abstrakcjom stosowanym w weryfikowanym oprogramowaniu, tak aby dowód mógł kierować się tą samą logiką co kod. W przypadku zkWasm oznacza to, że musimy zweryfikować obwód tabeli pamięci i funkcje „alloc odczytu/zapisu komórki” jako modułu, który łączy się jak pamięć zmienna. Dzięki takiemu interfejsowi weryfikację każdego obwodu rozkazowego można przeprowadzić w sposób podobny do zwykłego interpretera, natomiast dodatkowa złożoność ZK jest zamknięta w module podsystemu pamięci.
Podczas weryfikacji wdrożyliśmy założenie, że „tablicę pamięci można właściwie traktować jako zmienną strukturę danych”. Oznacza to, że napisz funkcję „memory_at type”, która całkowicie przeskanuje tablicę pamięci i zbuduje odpowiednie mapowanie danych adresowych. (Zakres wartości zmiennej „type” obejmuje tutaj trzy różne typy danych pamięci Wasm: stertę, stos danych i zmienne globalne.) Następnie udowadniamy, że ograniczenia pamięci generowane przez funkcję alloc są równoważne użyciu set i get funkcje Zmiany danych dokonywane przez odpowiednie mapowanie danych adresowych. Możemy udowodnić:
Dla każdego eid, jeśli spełnione są następujące ograniczenia
wartość przesunięcia typu eid pamięci_table_lookup_read_cell
Ale
get (memory_at eid type) offset = jakaś wartość
Oraz, jeśli spełnione są następujące ograniczenia
wartość przesunięcia typu eid pamięci_table_lookup_write_cell
Ale
memory_at (eid+ 1) type = set (memory_at eid type) wartość przesunięcia
Następnie weryfikacja każdej instrukcji może opierać się na operacjach get i set na mapie danych adresowych, podobnie jak w przypadku interpreterów kodu bajtowego innych niż ZK.
Mechanizm zliczania zapisu w pamięci zkWasm
Jednakże powyższy uproszczony opis nie ujawnia całej zawartości tablicy pamięci i tabeli skoków. W ramach zkVM tabele te mogą zostać zmanipulowane przez atakujących, którzy mogą z łatwością manipulować instrukcjami ładowania pamięci i zwracać dowolne wartości poprzez wstawienie wiersza danych.
Biorąc za przykład program wypłaty, osoba atakująca ma możliwość wprowadzenia fałszywych danych do salda konta, fałszując operację zapisu do pamięci o wartości 110 dolarów przed operacją wypłaty. Proces ten można osiągnąć poprzez dodanie wiersza danych do tabeli pamięci i modyfikację wartości istniejących komórek w tabeli pamięci i tabeli wykonania. Spowoduje to „bezpłatne” wypłaty, ponieważ po operacji saldo konta będzie nadal wynosić 100 USD.
Aby mieć pewność, że tablica pamięci (i tabela skoków) zawiera tylko prawidłowe wpisy wygenerowane przez faktycznie wykonane instrukcje zapisu (oraz wywołania i powrotu) do pamięci, zkWasm wykorzystuje specjalny mechanizm zliczający do monitorowania liczby wpisów. W szczególności tabela pamięci ma dedykowaną kolumnę, która śledzi całkowitą liczbę wpisów zapisanych w pamięci. Jednocześnie tablica wykonań zawiera także licznik liczący liczbę operacji zapisu do pamięci oczekiwanych dla każdej instrukcji. Upewnij się, że oba liczniki są spójne, ustawiając ograniczenie równości. Logika tej metody jest bardzo intuicyjna: za każdym razem, gdy wykonywana jest operacja zapisu w pamięci, zostanie ona zliczona raz i w tabeli pamięci powinien znajdować się odpowiedni rekord. Dlatego atakujący nie może wstawić żadnych dodatkowych wpisów do tablicy pamięci.
Powyższe logiczne stwierdzenie jest nieco niejasne i w procesie zmechanizowanego dowodu wymaga doprecyzowania. Najpierw musimy zrewidować stwierdzenie lematu dotyczącego zapisu w pamięci wspomnianego powyżej. Definiujemy funkcję `mops_at eid type` do zliczania wpisów tablicy pamięci o danym `eid` i `type` (większość instrukcji utworzy 0 lub 1 wpisów w eid ). Pełne stwierdzenie twierdzenia ma dodatkowy warunek wstępny stwierdzający, że nie ma fałszywych wpisów w tabeli pamięci:
Jeśli spełnione są następujące ograniczenia
(wartość przesunięcia typu eid pamięci_table_lookup_write_cell)
Ustanawia się następujące nowe ograniczenia
(typ eid mops_at) = 1
Ale
(typ pamięci_at(eid+ 1)) = ustaw wartość przesunięcia (typ pamięci_at eid)
Wymaga to, aby nasza weryfikacja była bardziej precyzyjna niż w poprzednim przypadku. Samo wyprowadzenie z ograniczenia równości, że całkowita liczba wpisów w tablicy pamięci jest równa całkowitej liczbie zapisów do pamięci w wykonaniu, nie wystarczy do zakończenia weryfikacji. Aby udowodnić poprawność instrukcji, musimy wiedzieć, że każda instrukcja odpowiada właściwej liczbie wpisów w tablicy pamięci. Na przykład musimy wykluczyć, czy atakujący mógłby pominąć wpis w tablicy pamięci dla instrukcji w sekwencji wykonawczej i utworzyć nowy, złośliwy wpis w tabeli pamięci dla innej niepowiązanej instrukcji.
Aby to udowodnić, stosujemy podejście odgórne, aby ograniczyć liczbę wpisów w tablicy pamięci odpowiadających danej instrukcji, co składa się z trzech kroków. W pierwszej kolejności szacujemy liczbę wpisów, jakie należy utworzyć dla instrukcji w sekwencji wykonawczej w zależności od typu instrukcji. Oczekiwaną liczbę zapisów od i-tego kroku do końca wykonania nazywamy „instructions_mops i”, a odpowiednią liczbę wpisów w tablicy pamięci od i-tej instrukcji do końca wykonania „cum_mops (eid i) `. Analizując ograniczenia wyszukiwania każdej instrukcji, możemy wykazać, że tworzy ona nie mniej wpisów niż oczekiwano, co prowadzi do wniosku, że każdy śledzony segment [i... numRows] tworzy nie mniej wpisów niż oczekiwano:
Lemat cum_mops_bound': forall n i,
0 ≤ ja ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≥ instrukcje_mops' i n.
Po drugie, jeśli potrafisz wykazać, że w tabeli nie ma więcej wpisów niż oczekiwano, to ma ona dokładnie odpowiednią liczbę wpisów, co jest oczywiste.
Lemat cum_mops_equal': forall n i,
0 ≤ ja ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≤ instrukcje_mops' i n ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) = instrukcje_mops' i n.
Teraz przejdź do kroku trzeciego. Nasze twierdzenie o poprawności stwierdza, że dla dowolnego n cum_mops i instrukcje_mops są zawsze spójne od wiersza n do końca tabeli:
Lemat cum_mops_equal : dla wszystkich n,
0 <= Z.of_nat n < etable_numRow ->
MTable.cum_mops (etable_values eid_cell (Z.of_nat n)) (max_eid+ 1) = instrukcje_mops (Z.of_nat n)
Weryfikację kończy podsumowanie n. Pierwszy wiersz w tabeli to ograniczenie równości zkWasm, wskazujące, że całkowita liczba wpisów w tabeli pamięci jest prawidłowa, czyli cum_mops 0 = instrukcje_mops 0 . Dla następujących linii hipoteza indukcyjna mówi nam:
cum_mops n = instrukcje_mops n
i mamy nadzieję to udowodnić
cum_mops (n+ 1) = instrukcje_mops (n+ 1)
Zwróć uwagę tutaj
cum_mops n = mop_at n + cum_mops (n+ 1)
I
instrukcje_mops n = instrukcje_mops n + instrukcje_mops (n+ 1)
Dlatego możemy uzyskać
mops_at n + cum_mops (n+ 1) = instrukcja_mops n + instrukcje_mops (n+ 1)
Wcześniej pokazaliśmy, że każda instrukcja utworzy nie mniej niż oczekiwaną liczbę wpisów, np.:
mops_at n ≥ instrukcja_mops n.
Można więc stwierdzić
cum_mops (n+ 1) ≤ instrukcje_mops (n+ 1)
Tutaj musimy zastosować drugi lemat powyżej.
(Korzystając z podobnego lematu w celu sprawdzenia tabeli skoków, można wykazać, że każda instrukcja wywołania może dokładnie wygenerować wpis w tabeli skoku, więc ta technika sprawdzająca ma ogólne zastosowanie. Jednakże nadal potrzebujemy dalszych prac weryfikacyjnych, aby udowodnić, że zwrot Poprawność instrukcja. Zwrócony eid różni się od eid instrukcji wywołującej, która utworzyła ramkę wywołania, dlatego potrzebujemy również dodatkowej właściwości niezmiennej, aby zadeklarować, że wartość eid jest zwiększana w jednym kierunku podczas sekwencji wykonania.)
Tak szczegółowe opisanie procesu sprawdzającego jest typowe dla weryfikacji formalnej i dlatego weryfikacja konkretnego fragmentu kodu często zajmuje więcej czasu niż jego napisanie. Ale czy warto? W tym przypadku było to opłacalne, ponieważ podczas sprawdzania znaleźliśmy krytyczny błąd w mechanizmie zliczania tabeli przeskoków. Błąd ten został szczegółowo opisany w poprzednim artykule - podsumowując, starsze wersje kodu uwzględniały zarówno instrukcje wywołania, jak i powrotu, a atakujący mógł wykonać fałszywy skok, dodając dodatkowe instrukcje powrotu do sekwencji wykonania, aby zrobić miejsce . Chociaż nieprawidłowy mechanizm zliczania może zaspokoić intuicję, że liczy się każda instrukcja wywołania i powrotu, problemy pojawiają się, gdy próbujemy udoskonalić tę intuicję w bardziej precyzyjnym stwierdzeniu twierdzenia.
Spraw, aby proces sprawdzania był modułowy
Z powyższej dyskusji widzimy, że istnieje cykliczna zależność pomiędzy dowodem dotyczącym obwodu każdej instrukcji a dowodem dotyczącym kolumny licznika w tabeli wykonania. Aby udowodnić poprawność obwodu instrukcji, musimy wnioskować o zapisach w nim pamięci, to znaczy musimy znać liczbę wpisów tablicy pamięci przy określonym EID i musimy udowodnić, że operacje zapisu do pamięci się liczą; tabela wykonania jest poprawna; i to Należy również udowodnić, że każda instrukcja wykonuje co najmniej minimalną liczbę zapisów do pamięci.
Ponadto należy wziąć pod uwagę jeszcze jeden czynnik. Projekt zkWasm jest dość duży, dlatego prace weryfikacyjne muszą być podzielone na moduły, aby wielu inżynierów zajmujących się weryfikacją mogło je podzielić. Dlatego przy dekonstrukcji dowodu mechanizmu zliczania należy zwrócić szczególną uwagę na jego złożoność. Przykładowo dla instrukcji LocalGet istnieją dwa twierdzenia:
Twierdzenie opcode_mops_correct_local_get : forall i,
0 <= i ->
etable_values eid_cell i > 0 ->
opcode_mops_correct LocalGet tj.
Twierdzenie LocalGetOp_correct : dla wszystkich i st y xs,
0 <= i ->
etable_values enabled_cell i = 1 ->
mops_at_correct i ->
etable_values (ops_cell LocalGet) i = 1 ->
state_rel i st ->
wasm_stack st = xs ->
(etable_values offset_cell i) > 1 ->
nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = Niektóre y ->
state_rel (i+ 1) (update_stack (incr_iid st) (y :: xs)).
Pierwsze stwierdzenie twierdzenia
opcode_mops_correct LocalGet i
Po rozwinięciu oznacza to, że instrukcja tworzy co najmniej jeden wpis tablicy pamięci w linii i (liczba 1 jest podana w specyfikacji kodu operacji LocalGet zkWasm).
Drugie twierdzenie jest twierdzeniem o całkowitej poprawności instrukcji, na które się powołuje
mops_at_correct i
Hipotetycznie oznacza to, że instrukcja tworzy dokładnie jeden wpis w tablicy pamięci.
Inżynier weryfikujący może niezależnie udowodnić te dwa twierdzenia, a następnie połączyć je z dowodem dotyczącym tabeli wykonania, aby wykazać poprawność całego systemu. Warto zaznaczyć, że wszelkie dowody poszczególnych instrukcji można przeprowadzić na poziomie ograniczeń odczytu/zapisu bez znajomości konkretnej implementacji tablicy pamięci. Dlatego projekt został podzielony na trzy części, które można realizować niezależnie.
Podsumować
Weryfikacja obwodów ZKVM linia po linii nie różni się zasadniczo od weryfikacji aplikacji ZK w innych dziedzinach, ponieważ obie wymagają podobnego rozumowania dotyczącego ograniczeń arytmetycznych. Z perspektywy wysokiego poziomu weryfikacja zkVM wymaga wielu takich samych formalnych metod weryfikacji, jakie są stosowane w przypadku interpreterów i kompilatorów języków programowania. Główną różnicą jest tutaj stan maszyny wirtualnej o dynamicznym rozmiarze. Jednakże wpływ tych różnic można zminimalizować, starannie konstruując strukturę weryfikacji tak, aby pasowała do warstwy abstrakcji użytej w implementacji, umożliwiając implementację każdej instrukcji jako niezależnego modułu w oparciu o interfejs get-set, tak jak w przypadku zwykłego interpretera chemicznego weryfikacja.
