Testowanie symboliczne z Halmosem: Wykorzystanie istniejących testów do weryfikacji formalnej

Weryfikacja formalna — proces polegający na wykorzystaniu metod matematycznych do „kontroli” programu lub inteligentnej umowy na dowolnej liczbie danych wejściowych — jest ogólnie postrzegana jako bardziej zwięzła, bardziej wszechstronna alternatywa dla tradycyjnego testowania, umożliwiająca pisanie wyższej jakości i bezpieczniejszego kodu. Jednak w rzeczywistości weryfikacja formalna jest procesem otwartym i interaktywnym. Podobnie jak w przypadku testów jednostkowych, programiści muszą dynamicznie definiować formalne specyfikacje i nakładać je na nie, powtarzając swoje podejście w miarę ewolucji kodu i analiz. Co więcej, formalna weryfikacja jest tak skuteczna, jak jej specyfikacje, których napisanie może być czasochłonne (i często wiąże się ze stromą krzywą uczenia się). 

Dla wielu programistów, dla których ten proces jest zniechęcający, testy jednostkowe są często bardziej opłacalną i oszczędzającą czas drogą do ustalenia poprawności programu. W praktyce weryfikacja formalna nie jest bardziej kompleksową alternatywą dla testów jednostkowych, ale uzupełnieniem. Procesy te mają różne mocne strony i ograniczenia, zapewniając jeszcze większą pewność, gdy są stosowane razem. Deweloperzy zawsze będą musieli pisać testy jednostkowe — a co by było, gdybyśmy mogli użyć tych samych właściwości do formalnej weryfikacji?

Halmosa, nasze narzędzie do formalnej weryfikacji typu open source, umożliwia programistom ponownie te same właściwości zapisane dla testów jednostkowych dla specyfikacji formalnych poprzez testowanie symboliczne. Zamiast tworzyć solidny zestaw właściwości od samego początku, programiści mogą uniknąć powielania pracy i ulepszać swoje testy o kilka specyfikacji na raz, bez rozpoczynania od zera. Zaprojektowaliśmy to narzędzie do użytku wraz z innymi w procesie weryfikacji formalnej, jako wstęp do weryfikacji formalnej; programiści mogą zacząć od kilku analiz przy minimalnym wysiłku, zanim dodadzą więcej w późniejszym czasie.

W tym poście omawiamy wyzwania związane z weryfikacją formalną oraz potencjał wypełnienia luki między testami jednostkowymi a weryfikacją formalną za pomocą testów symbolicznych. Następnie przeglądamy wersję demonstracyjną Halmosa przy użyciu istniejącego kodu inteligentnej umowy i przyjrzymy się innym formalnym narzędziom do weryfikacji (wiele z nich ma otwarte oprogramowanie) dostępnym dla programistów.

Weryfikacja formalna vs testowanie

Formalna weryfikacja — generalnie preferowany przez programistów blockchain ze względu na jego rygor i kompleksowość — to proces udowadniania poprawności programu poprzez sprawdzenie, czy spełnia on określone właściwości poprawności. Właściwości, które są specyficzne dla programu, są zwykle dostarczane z zewnątrz i wyrażane przy użyciu języka formalnego lub notacji obsługiwanej przez używane narzędzie weryfikacyjne. Deweloperzy często postrzegają weryfikację formalną jako rozwiązanie umożliwiające automatyczne testowanie właściwości we wszystkich możliwych scenariuszach, ale w rzeczywistości weryfikacja formalna może być procesem pracochłonnym i wysoce interaktywnym.

Podobnie jak weryfikacja formalna, testy jednostkowe obejmują ocenę, czy program działa zgodnie z oczekiwaniami; Testowanie jednak sprawdza tylko zachowanie programu kilka danych wejściowych, podczas gdy weryfikacja formalna może to sprawdzić cała kolekcja możliwe dane wejściowe. Zarówno testowanie, jak i weryfikacja formalna wymagają opisu oczekiwanego zachowania programu (z przypadkami testowymi używanymi w testowaniu i specyfikacjami formalnymi używanymi w weryfikacji formalnej). Ale użyte razem mogą zapewnić dokładniejsze badanie programu. Na przykład testowanie jest skuteczne w znajdowaniu prostych błędów i błędów, ale generalnie jest szybsze i łatwiejsze do wykonania. Formalna weryfikacja, choć bardziej kłopotliwa w użyciu, jest wystarczająco skuteczna, aby udowodnić brak błędów lub ujawnić subtelne błędy, które łatwo przeoczyć podczas testowania lub przeglądu kodu.

Specyfikacja narzutu

Jednym z głównych wyzwań weryfikacji formalnej jest narzut związany z pisaniem i utrzymywaniem formalnych specyfikacji. Proces ten często wiąże się z czasochłonnym zadaniem ręcznego pisania specyfikacji przy użyciu specjalistycznego języka (którego wielu programistów będzie musiało się najpierw nauczyć). Proces ten jest również stopniowy i zazwyczaj zaczyna się od napisania prostych właściwości i ich weryfikacji, a następnie stopniowego dodawania bardziej złożonych właściwości. Podobnie jak testowanie, jest to proces otwarty, bez wyraźnego punktu zatrzymania i można dodać tylko tyle właściwości, ile to możliwe w dostępnych ramach czasowych. Ponadto, gdy programiści zmieniają kod w trakcie jego weryfikacji, muszą również zaktualizować swoje istniejące specyfikacje, co prowadzi do dodatkowych prac konserwacyjnych. Czynniki te mogą sprawić, że weryfikacja formalna będzie zniechęcającym zadaniem dla niektórych programistów, którzy wahają się, czy ponieść dodatkowe koszty ogólne.

I chociaż testowanie i weryfikacja formalna mogą poprawić jakość kodu, gdy są używane razem, oba wymagają (czasem podobnych) opisów oczekiwanego zachowania programu w różnych językach i formatach. Pisanie i utrzymywanie tych opisów jest pracochłonne, a utrzymywanie dwóch różnych form tego samego opisu może sprawiać wrażenie powielania wysiłków. Rodzi to następujące pytanie: czy możliwe jest opisanie oczekiwanego zachowania w sposób, który programiści mogą wykorzystać zarówno do testowania, jak i weryfikacji?

Wypełnienie luki między testowaniem a weryfikacją formalną za pomocą testów symbolicznych i Halmos

Testowanie symboliczne, praktyka przeprowadzania testów z symbolicznymi danymi wejściowymi, jest efektywną metodą weryfikacji formalnej, która zmniejsza narzut związany ze specyfikacją. Takie podejście umożliwia wykorzystanie tych samych przypadków testowych zarówno do testowania, jak i weryfikacji formalnej. W przeciwieństwie do tradycyjnego testowania, które weryfikuje, czy program działa poprawnie dla ograniczonego zestawu danych wejściowych, testowanie symboliczne sprawdza program pod kątem wszystkich możliwych danych wejściowych, dlatego program, który pomyślnie przejdzie testy symboliczne, można uznać za formalnie zweryfikowany.

Halmos to narzędzie do weryfikacji formalnej przeznaczone do testowania symbolicznego. Zamiast wymagać osobnych specyfikacji lub uczyć się nowego języka, Halmos wykorzystuje istniejące testy jako formalne specyfikacje. Przeprowadzanie testów przez Halmos automatycznie zweryfikuje, czy przeszły pomyślnie wszystkie możliwe dane wejściowe lub dostarczy kontrprzykłady. To nie tylko eliminuje potrzebę pisania dodatkowej specyfikacji, ale także pozwala na ponowne wykorzystanie testów napisanych do testów jednostkowych lub fuzzingu do celów weryfikacji formalnej.

Deweloperzy mają zatem większą elastyczność w wyborze spośród szeregu opcji zapewniania jakości, w tym testów jednostkowych, fuzzingu i weryfikacji formalnej, w zależności od bieżących potrzeb. Na przykład testy mogą szybko wykryć proste błędy, być może za pomocą fuzzera, który generuje losowe dane wejściowe, a następnie Halmos może jeszcze bardziej zwiększyć zaufanie do poprawności programu we wszystkich danych wejściowych.

Przykład: Testowanie isPowerOfTwo() funkcjonować

Jako przykład rozważmy następujące isPowerOfTwo() funkcja, która określa, czy dana liczba jest potęgą dwójki. Ta funkcja wykorzystuje a algorytm manipulacji bitami dla wydajności, ale udowodnienie jej poprawności może być trudne, szczególnie w przypadku, gdy dane wejściowe nie są potęgą dwójki.

Wyobraź sobie następujący test dla isPowerOfTwo() funkcja: porównuje rzeczywiste wyjście funkcji z oczekiwanym wyjściem dla danego wejścia. Jest to test sparametryzowany (znany również jako test oparty na właściwościach), co oznacza, że ​​można go łatwo uruchomić z różnymi wartościami wejściowymi, prawdopodobnie za pomocą narzędzi fuzzujących, takich jak Foundry.

Możesz użyć tego testu do zbadania isPowerOfTwo() poprzez testy jednostkowe lub testy rozmyte, uruchamiając je z wybranymi wejściami. Testy takie jak te nie mogą formalnie udowodnić poprawności funkcji, ponieważ przeprowadzenie testu dla każdego możliwego wejścia jest obliczeniowo niewykonalne.

Halmos pozwala jednak programistom na ponowne wykorzystanie tych wcześniej istniejących testów do formalnej weryfikacji przy niewielkim dodatkowym wysiłku. Narzędzie sprawdza, czy testy wypadły pomyślnie dla wszystkich możliwych danych wejściowych, wykonując symboliczne wykonanie testu, a następnie sprawdzając, czy asercja nigdy nie została naruszona (lub, jeśli asercja is łamane, podając kontrprzykład). Oznacza to, że jeśli test Halmosa przejdzie pomyślnie, poprawność funkcji jest formalnie weryfikowana, co oznacza, że ​​algorytm jest poprawnie zaimplementowany i został dokładnie przetłumaczony przez kompilator na kod bajtowy.

Ograniczenie: ograniczone wykonanie symboliczne

Zasadniczo nie jest możliwe przeprowadzenie w pełni automatycznego, kompletnego testowania symbolicznego, ponieważ wymagałoby to rozwiązania problemu problem z zatrzymaniem, o czym wiadomo nierozstrzygalny. Jednym z powodów jest to, że często niemożliwe jest automatyczne określenie, ile razy pętla powinna wykonać symboliczną iterację. W rezultacie w pełni automatyczna weryfikacja formalna jest generalnie nierozstrzygalna.

Biorąc pod uwagę te fundamentalne ograniczenia, Halmos przedkłada automatyzację nad kompletność. W tym celu Halmos jest przeznaczony do wykonywania ograniczonego wnioskowania symbolicznego dla nieograniczonych pętli (gdzie liczba iteracji zależy od danych wejściowych programu) lub tablic o zmiennej długości (w tym łańcuchów). Poświęca to pewną kompletność, ale pozwala Halmosowi uniknąć wymagania od użytkownika dostarczenia dodatkowych adnotacji, takich jak niezmienniki pętli.

Rozważmy na przykład następującą iteracyjną wersję isPowerOfTwo() funkcja, która zawiera nieograniczoną pętlę while, w której liczba iteracji pętli jest określona przez minimalną liczbę bitów wymaganych do reprezentacji liczby wejściowej.

Halmos symbolicznie iteruje tę nieograniczoną pętlę tylko do określonej granicy. Na przykład, jeśli ograniczenie jest ustawione na 3, Halmos wykona iterację pętli najwyżej 3 razy i nie weźmie pod uwagę wartości wejściowych, które spowodowałyby iterację pętli więcej niż 3 razy (tj. wartości większe lub równe 2^3 ). W tym konkretnym przypadku ustawienie ograniczenia na 256 lub więcej pozwoliłoby na ukończenie Halmosa.

Demo: Formalna weryfikacja ERC721A z Halmosem

Aby zademonstrować możliwości Halmosa, użyliśmy go do symbolicznego przetestowania i formalnej weryfikacji ERC721A, wysoce zoptymalizowana pod kątem gazu implementacja standardu ERC721, która umożliwia bicie seryjne przy prawie takim samym koszcie jak bicie pojedyncze. ERC721A zawiera kilka innowacyjnych optymalizacje aby osiągnąć tę wydajność; na przykład gaz można zaoszczędzić, opóźniając aktualizacje danych własności tokena do momentu przeniesienia tokena, a nie w momencie bicia. Wymaga to użycia złożonych struktur danych i algorytmów w celu wydajnego pobierania informacji o własności z leniwej struktury danych. I chociaż ta optymalizacja poprawia wydajność gazu, zwiększa również złożoność kodu i utrudnia udowodnienie poprawności implementacji. To sprawia, że ​​ERC721A jest dobrym kandydatem do formalnej weryfikacji, ponieważ może zwiększyć zaufanie do wdrożenia i przynieść korzyści potencjalnym użytkownikom.

Symboliczne właściwości testowe

Ponieważ istniejące testy dla ERC721A zostały napisane w JavaScript z Hardhatem (który obecnie nie jest obsługiwany przez Halmos), napisaliśmy nowe testy w Solidity dla głównych funkcji punktu wejścia: mint(), burn(), transfer(). Testy te sprawdziły, czy każda funkcja prawidłowo aktualizuje własność i saldo tokena oraz wpływa tylko na odpowiednich użytkowników bez zmiany salda lub własności innych użytkowników. To ostatnie jest nietrywialne do udowodnienia ze względu na zastosowanie algorytmu leniwej struktury danych w ERC721A. Na przykład poniższy test sprawdza, czy plik transfer() funkcja poprawnie aktualizuje własność określonego tokena:

Kolejny test sprawdza, czy transfer() funkcja nie zmienia równowagi dla innych adresów, co jest trudne do udowodnienia, jak wspomniano wcześniej:

Wyniki weryfikacji

Przeprowadziliśmy eksperyment weryfikacyjny przy użyciu Halmosa na smart kontrakcie ERC721A, pisząc w sumie Test 19. Testy przeprowadzono przez Halmos z ograniczeniem rozwijania pętli równym 3, co zajęło 16 minut. Podział czasu weryfikacji można zobaczyć w poniższej tabeli. Eksperyment przeprowadzono na MacBooku Pro z chipem M1 Pro i 16 GB pamięci.

Testowanie	Czas (s)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdBez zmian	1.40
testBurnOtherRównowagaZachowanie	5.69
testBurnOtherWłasnośćKonserwacja	189.70
testBurnOwnershipUpdate	3.81
Wymagania testoweBurn	71.95
test MintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMennicaInneSaldoKonserwacja	0.26
testMennicaInneWłasnośćZachowanie	5.74
testMintWłasnośćAktualizacja	1.38
testMintWymagania	0.09
testTransferSaldoBez zmian	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdBez zmian	4.47
testTransferInneSaldoZachowanie	19.57
testTransferInneWłasnośćZachowanie	430.61
testTransferOwnershipUpdate	18.71
Testowe wymagania dotyczące transferu	149.18

Podczas gdy większość testów została ukończona w ciągu kilku sekund, niektóre z nich trwały kilka minut. Te czasochłonne testy były trudne do zweryfikowania ze względu na złożony charakter rozpatrywanych przypadków i były ściśle związane z poprawnością algorytmu leniwej struktury danych.

Ogólnie rzecz biorąc, wyniki tego eksperymentu wskazują, że Halmos jest w stanie skutecznie zweryfikować poprawność kodu inteligentnego kontraktu. Zapewnia większe zaufanie do integralności kodu, pomimo złożoności i potencjalnych przypadków brzegowych inteligentnego kontraktu.

Eksperymentuj z wstrzykniętymi błędami

Aby zademonstrować skuteczność ograniczonego rozumowania Halmosa, użyliśmy go do wykrycia błędów w poprzedniej wersji kontraktu ERC721A. Ta wersja miała problem, który nieprawidłowo obsługiwał przepełnienie arytmetyczne i potencjalnie pozwalał na wybijanie wsadowe dużej liczby tokenów, co mogło naruszyć integralność leniwej struktury danych i spowodować utratę własności tokena przez niektórych użytkowników (problem zdecydowany w obecnej wersji). Przeprowadziliśmy ten sam zestaw 19 testów dla ERC721A w wersji buggy i Halmos był w stanie znaleźć kontrprzykład dla właściwości mint() funkcjonować. W szczególności firma Halmos dostarczyła wartości wejściowych, które doprowadziły do ​​opisanego powyżej scenariusza wykorzystania luk w zabezpieczeniach. Wyniki tego eksperymentu wskazują, że pomimo swojej niekompletności ograniczone rozumowanie Halmosa może być skutecznym sposobem wykrywania i zapobiegania możliwym do wykorzystania błędom w inteligentnych kontraktach.

Powiązana praca

Różne zespoły opracowały formalne narzędzia do weryfikacji kodu bajtowego inteligentnego kontraktu Ethereum. Narzędzia te, w tym Halmos, mogą pomóc w zapewnieniu bezpieczeństwa i poprawności inteligentnych kontraktów. Porównanie i zrozumienie różnych funkcji, możliwości i ograniczeń tych narzędzi może pomóc programistom wybrać najbardziej odpowiednie dla ich unikalnych potrzeb.

Chociaż Halmos jest cennym dodatkiem do zestawu narzędzi dostępnych do inteligentnej weryfikacji kontraktów, ma on uzupełniać (nie zastępować) istniejące narzędzia. Deweloperzy mogą łączyć Halmos z innymi narzędziami, aby osiągnąć wyższy poziom pewności w swoich umowach. Poniżej porównujemy Halmosa z kilkoma wybranymi formalnymi narzędziami obsługującymi kod bajtowy EVM.

• K to potężna formalna struktura weryfikacji, która umożliwia weryfikację dedukcyjną i interaktywne dowodzenie twierdzeń. Jego podstawowa teoria i implementacja zapewniają wysoki poziom wyrazistości, dzięki czemu nadaje się do weryfikacji złożonych programów i algorytmów. Należy jednak zauważyć, że K nie został zaprojektowany z dużym naciskiem na automatyczną weryfikację i brakuje mu pewnych funkcji automatyzacji, które mogą wymagać większego nakładu pracy ręcznej podczas procesu weryfikacji. Aby korzystać z platformy K, formalne specyfikacje są napisane w języku K, którego należy się nauczyć przed użyciem. Jego siła jest szczególnie przydatna w weryfikacji złożonych systemów, których analiza przy użyciu zautomatyzowanego wnioskowania może być trudna.
• Certora to formalne narzędzie do weryfikacji inteligentnych kontraktów, które koncentruje się na automatycznej weryfikacji i obsługuje ograniczone sprawdzanie modeli, podobnie jak Halmos. Aby korzystać z Certora, programiści muszą nauczyć się nowego języka, cvl rozszerzenie, w celu napisania specyfikacji. Język ten pozwala na zwięzły opis wielu krytycznych właściwości za pomocą niezmienników kontraktu, funkcji, której Halmos obecnie nie obsługuje. Pomimo tego, że jest zastrzeżonym narzędziem o zamkniętym źródle, Certora zapewnia solidne narzędzie do weryfikacji formalnej, z ciągłym rozwojem i dobrym wsparciem dla użytkowników.
  
  Z kolei Halmos to narzędzie typu open source, które jest mniejsze i obecnie nie ma niektórych funkcji zapewnianych przez Certorę, ale ma służyć jako dobro publiczne i ma być rozwiązaniem niszowym do szybkiej weryfikacji inteligentnych kontraktów bez konieczność obszernej konfiguracji i konserwacji.
• HEVM to kolejne formalne narzędzie do weryfikacji, które jest podobne do Halmosa. Wcześniej był częścią DappTools, który jest prekursorem Foundry. Zarówno HEVM, jak i Halmos mają tę cechę, że nie wymagają oddzielnej specyfikacji i mogą symbolicznie wykonywać istniejące testy w celu identyfikacji naruszeń asercji. Dzięki temu użytkownicy mogą używać obu narzędzi zamiennie lub uruchamiać je równolegle do tych samych testów, zapewniając im wiele opcji testowania symbolicznego.
  
  Warto zauważyć, że pomimo podobieństw HEVM i Halmos zostały opracowane niezależnie i różnią się szczegółami implementacji; zwłaszcza w zakresie optymalizacji i strategii wnioskowania symbolicznego. Dodatkowo HEVM jest napisany w Haskell, podczas gdy Halmos jest napisany w Pythonie, zapewniając dostęp do bogatego ekosystemu Pythona. Możliwość korzystania z obu narzędzi daje użytkownikom większą elastyczność i możliwości zapewnienia bezpieczeństwa i poprawności smart kontraktów.

Halmosa jest open source i obecnie znajduje się w fazie beta. Aktywnie pracujemy nad nowymi cechy i funkcjonalność, w tym kody do Foundry i kilka innych kluczowych funkcji użyteczności. Bylibyśmy bardzo wdzięczni za przemyślenia, które funkcje są najważniejsze, i mile widziane wszelkie opinie, sugestie i wkład, aby uczynić Halmos lepszym narzędziem dla wszystkich.

**

Wyrażone tutaj poglądy są poglądami poszczególnych cytowanych pracowników AH Capital Management, LLC („a16z”) i nie są poglądami a16z ani jej podmiotów stowarzyszonych. Niektóre informacje w nim zawarte zostały pozyskane ze źródeł zewnętrznych, w tym od spółek portfelowych funduszy zarządzanych przez a16z. Chociaż pochodzą ze źródeł uważanych za wiarygodne, a16z nie zweryfikowało niezależnie takich informacji i nie składa żadnych oświadczeń dotyczących aktualnej lub trwałej dokładności informacji lub ich adekwatności w danej sytuacji. Ponadto treści te mogą zawierać reklamy osób trzecich; a16z nie przeglądał takich reklam i nie popiera żadnych zawartych w nich treści reklamowych.

Te treści są udostępniane wyłącznie w celach informacyjnych i nie należy ich traktować jako porady prawnej, biznesowej, inwestycyjnej lub podatkowej. Powinieneś skonsultować się w tych sprawach z własnymi doradcami. Odniesienia do jakichkolwiek papierów wartościowych lub aktywów cyfrowych służą wyłącznie celom ilustracyjnym i nie stanowią rekomendacji inwestycyjnej ani oferty świadczenia usług doradztwa inwestycyjnego. Ponadto treść ta nie jest skierowana ani przeznaczona do użytku przez jakichkolwiek inwestorów lub potencjalnych inwestorów iw żadnym wypadku nie można na nich polegać przy podejmowaniu decyzji o zainwestowaniu w jakikolwiek fundusz zarządzany przez a16z. (Oferta inwestycji w fundusz a16z zostanie złożona wyłącznie na podstawie memorandum dotyczącego oferty prywatnej, umowy subskrypcyjnej i innej odpowiedniej dokumentacji takiego funduszu i należy ją przeczytać w całości.) Wszelkie inwestycje lub spółki portfelowe wymienione, wymienione lub opisane nie są reprezentatywne dla wszystkich inwestycji w pojazdy zarządzane przez a16z i nie można zapewnić, że inwestycje będą opłacalne lub że inne inwestycje dokonane w przyszłości będą miały podobne cechy lub wyniki. Lista inwestycji dokonanych przez fundusze zarządzane przez Andreessena Horowitza (z wyłączeniem inwestycji, w przypadku których emitent nie wyraził zgody na publiczne ujawnienie przez a16z oraz niezapowiedzianych inwestycji w aktywa cyfrowe będące w obrocie publicznym) jest dostępna pod adresem https://a16z.com/investments /.

Wykresy i wykresy zamieszczone w niniejszym dokumencie służą wyłącznie celom informacyjnym i nie należy na nich polegać przy podejmowaniu jakichkolwiek decyzji inwestycyjnych. Wyniki osiągnięte w przeszłości nie wskazują na przyszłe wyniki. Treść mówi dopiero od wskazanej daty. Wszelkie prognozy, szacunki, prognozy, cele, perspektywy i/lub opinie wyrażone w tych materiałach mogą ulec zmianie bez powiadomienia i mogą się różnić lub być sprzeczne z opiniami wyrażanymi przez innych. Dodatkowe ważne informacje można znaleźć na stronie https://a16z.com/disclosures.