Ten artykuł jest zgłoszeniem społeczności. Autorem jest David Tarditi, VP of Engineering w CertiK, firmie zajmującej się audytem smart kontraktów Web3.
TL;DR
Formalna weryfikacja smart kontraktów zapewnia, że są one wolne od błędów, luk w zabezpieczeniach i innych niezamierzonych zachowań. Wiąże się to z przedstawieniem przez eksperta logiki smart kontraktu w postaci twierdzeń matematycznych, a następnie poddaniem ich automatycznemu procesowi, który sprawdza rzeczywistą logikę z modelami oczekiwanego zachowania kontraktu. Połączenie formalnej weryfikacji i ręcznego audytu, zapewnia kompleksową ocenę bezpieczeństwa smart kontraktu.
Wprowadzenie
Smart kontrakty to programy komputerowe wdrożone na blockchainie, które uruchomiają się automatycznie, gdy spełnione są określone warunki. Mogą być prostymi do niezwykle skomplikowanych i mogą przechowywać aktywa warte miliony, a nawet miliardy dolarów.
Luki w zabezpieczeniach w kodzie smart kontraktu mogą mieć katastrofalne skutki, w tym kradzież wszystkich aktywów przechowywanych przez smart kontrakt. W 2021 roku, automatycznemu animatorowi rynku (AMM) Uranium Finance, skradziono 50 milionów $, z powodu pojedynczej literówki w smart kontrakcie.
Również w 2021, Compound Finance rozdał 80 milionów $ niezdobytych nagród, z powodu błędu jednego znaku. W 2022 roku z Wormhole Bridge skradziono 320 milionów $, z powodu błędu w jednym z jego smart kontraktów.
Ważne jest, aby program smart kontraktu był poprawny za pierwszym razem. Smart kontrakty są open-source, co oznacza, że po wdrożeniu kontraktu kod jest publicznie dostępny. Jeśli haker znajdzie błąd, może go natychmiast wykorzystać. Ponadto, łatanie luk w zabezpieczeniach w czasie nie jest możliwe, ponieważ kod smart kontraktu zazwyczaj nie może być modyfikowany po wdrożeniu.
Jak Działa Weryfikacja Smart Kontraktu?
Formalna weryfikacja smart kontraktów, działa poprzez przedstawienie logiki i pożądanego zachowania smart kontraktów jako twierdzeń matematycznych. Następnie audytorzy wykorzystują zautomatyzowane narzędzia do sprawdzenia, czy te stwierdzenia są poprawne.
Proces ten obejmuje:
Definiowanie specyfikacji i pożądanych właściwości kontraktu w języku formalnym.
Tłumaczenie kodu kontraktu na formalną reprezentację, taką jak modele matematyczne lub logika.
Używanie automatycznych dowódców twierdzeń lub sprawdzających modele, do walidacji specyfikacji i właściwości kontraktu.
Powtarzanie procesu weryfikacji, w celu znalezienia i naprawienia wszelkich błędów lub odchyleń od pożądanych właściwości.
Dlaczego Weryfikacja Smart Kontraktu Jest Ważna
Zastosowanie rozumowania matematycznego pomaga zapewnić, że formalnie zweryfikowane smart kontrakty są wolne od błędów, luk w zabezpieczeniach i innych niezamierzonych zachowań. Pomaga to również zwiększyć zaufanie do kontraktu, ponieważ jego właściwości zostały rygorystycznie udowodnione jako poprawne.
Poniżej przedstawiamy kilka przykładów tego, jak weryfikacja smart kontraktów pomogła zapobiec, znacznym stratom finansowym i innym katastrofalnym rezultatom.
Uniswap
Uniswap to dobrze znany AMM. Kiedy powstał smart kontrakt Uniswap V1, został on formalnie zweryfikowany. Przed wydaniem, ta formalna weryfikacja znalazła i naprawiła błędy dotyczące zaokrągleń, które mogły doprowadzić do pozbawienia Uniswap V1 funduszy.
Balancer
Balancer V2 to również AMM, który został formalnie zweryfikowany. Formalna weryfikacja znalazła i naprawiła nieprawidłową kalkulację opłat, obejmującą funkcjonalność flash loan w smart kontrakcie, co mogło sprawić, że giełda byłaby podatna na kradzież.
SafeMoon
SafeMoon V1 zawierał subtelny błąd, znaleziony przez formalną weryfikację po jego wdrożeniu. Właścicielowi udało się zrzec własności kontaktu, a następnie jego ponowne nabycie, gdyż przed zrzeczeniem się własności dokonano pewnych czynności.
Ten błąd został przeoczony w większości ręcznych audytów forków SafeMoon V1, ponieważ jego znalezienie wymagało przeanalizowania konkretnych kombinacji wartości zmiennych programu. Jest to coś, co łatwo jest przeoczyć człowiekowi, a co łatwo jest wychwycić maszynie.
W Jaki Sposób Formalna Weryfikacja i Audyt Manualny Działają Razem
Formalna weryfikacja zapewnia systematyczny i zautomatyzowany sposób sprawdzania logiki i zachowania kontraktu, pod kątem jego pożądanych właściwości. Dzięki temu łatwiej jest zidentyfikować i naprawić ewentualne błędy lub usterki. Jest to szczególnie przydatne do znajdowania złożonych i subtelnych problemów, które mogą być trudne do wykrycia poprzez manualną inspekcję.
Audyt manualny polega na eksperckim przeglądzie kodu, projektu i wdrożenia kontraktu. Audytor wykorzystuje swoje doświadczenie i wiedzę do identyfikacji zagrożeń bezpieczeństwa i oceny ogólnego stanu bezpieczeństwa kontraktu. Może również potwierdzić, że proces weryfikacji formalnej został wykonany poprawnie, a także sprawdzić, czy nie ma problemów, które mogą nie być wykrywalne przez zautomatyzowane narzędzia.
Połączenie formalnej weryfikacji i manualnego audytu, zapewnia kompleksową ocenę bezpieczeństwa smart kontraktu. Zwiększa to szanse na znalezienie i naprawienie wszelkich luk w zabezpieczeniach. Wynikiem tego jest podejście do bezpieczeństwa typu "defense-in-depth", które wykorzystuje unikalne możliwości zarówno ludzi jak i maszyn.
Wnioski Końcowe
Aby zapewnić bezpieczeństwo smart kontraktów, konieczne jest zastosowanie zarówno formalnej weryfikacji jak i ręcznego audytu, w celu zapewnienia kompleksowej i dokładnej oceny postawy bezpieczeństwa smart kontraktu.
Chociaż formalna weryfikacja może pochłaniać sporo zasobów, jest to inwestycja, którą warto ponieść, szczególnie w przypadku kontraktów o dużej wartości lub czynnikach wysokiego ryzyka. Ostatecznie, priorytetem jest bezpieczeństwo i zapewnienie, że smart kontrakty są wolne od błędów, luk w zabezpieczeniach i niezamierzonych zachowań.
Dalsza Lektura
Wyłączenie Odpowiedzialności i Ostrzeżenie o Ryzyku: Niniejsza treść jest prezentowana "w stanie jakim jest", wyłącznie w celach informacyjnych i edukacyjnych, bez jakichkolwiek gwarancji. Nie należy jej interpretować jako porady finansowej, ani nie ma ona charakteru zachęty do zakupu jakiegokolwiek konkretnego produktu lub usługi. Ceny aktywów cyfrowych mogą być zmienne. Wartość Twojej inwestycji może spaść lub wzrosnąć i możesz nie odzyskać zainwestowanej kwoty. Ponosisz wyłączną odpowiedzialność za swoje decyzje inwestycyjne, a Akademia Binance nie ponosi odpowiedzialności za jakiekolwiek straty, jakie możesz ponieść. Ten materiał nie powinien być traktowany jako porada finansowa.