Ten artykuł jest zgłoszeniem społeczności. Autorem jest David Tarditi, wiceprezes ds. inżynierii w CertiK, firmie audytorskiej inteligentnych kontraktów Web3.
Poglądy zawarte w tym artykule są poglądami współautora/autora i niekoniecznie odzwierciedlają poglądy Binance Academy.
TL;DR
Formalna weryfikacja inteligentnych kontraktów gwarantuje, że są one wolne od błędów, luk w zabezpieczeniach i innych niezamierzonych zachowań. Polega na tym, że ekspert przedstawia logikę inteligentnego kontraktu w postaci stwierdzeń matematycznych, a następnie przeprowadza je przez zautomatyzowany proces, który porównuje rzeczywistą logikę z modelami oczekiwanego zachowania kontraktu. Połączenie weryfikacji formalnej i audytu ręcznego zapewnia kompleksową ocenę bezpieczeństwa inteligentnego kontraktu.
Wstęp
Inteligentne kontrakty to programy komputerowe wdrażane na blockchainie, które działają automatycznie po spełnieniu określonych warunków. Mogą mieć różną skalę od prostych do niezwykle złożonych i mogą zawierać aktywa warte miliony, a nawet miliardy dolarów.
Luki w zabezpieczeniach kodu inteligentnego kontraktu mogą mieć druzgocące konsekwencje, w tym kradzież wszystkich aktywów objętych inteligentnym kontraktem. W 2021 r. automatycznemu animatorowi rynku (AMM) Uranium Finance skradziono 50 milionów dolarów z powodu jednej literówki w inteligentnej umowie.
Również w 2021 r. Compound Finance przyznała 80 milionów dolarów niezasłużonych nagród z powodu błędu w jednym znaku. W 2022 roku z mostu czasoprzestrzennego skradziono 320 milionów dolarów z powodu błędu w jednym z jego inteligentnych kontraktów.
Ważne jest, aby dobrze wdrożyć program inteligentnych kontraktów już za pierwszym razem. Inteligentne kontrakty mają charakter open source, co oznacza, że kod jest publicznie dostępny po wdrożeniu kontraktu. Jeśli haker znajdzie błąd, może natychmiast z niego skorzystać. Ponadto łatanie luk w zabezpieczeniach z biegiem czasu nie wchodzi w grę, ponieważ kodu inteligentnego kontraktu zazwyczaj nie można modyfikować po wdrożeniu.
Jak działa inteligentna weryfikacja kontraktu?
Formalna weryfikacja inteligentnych kontraktów polega na przedstawieniu logiki i pożądanego zachowania inteligentnych kontraktów w postaci stwierdzeń matematycznych. Następnie audytorzy korzystają z zautomatyzowanych narzędzi, aby sprawdzić, czy te stwierdzenia są prawidłowe.
Proces obejmuje:
Definiowanie specyfikacji i pożądanych właściwości kontraktu w języku formalnym.
Tłumaczenie kodu umowy na formalną reprezentację, taką jak modele matematyczne lub logika.
Korzystanie z automatycznych narzędzi do sprawdzania twierdzeń lub sprawdzania modeli w celu sprawdzenia specyfikacji i właściwości kontraktu.
Powtarzanie procesu weryfikacji w celu znalezienia i naprawienia ewentualnych błędów lub odchyleń od pożądanych właściwości.
Dlaczego inteligentna weryfikacja kontraktu jest ważna
Stosowanie rozumowania matematycznego pomaga zapewnić, że formalnie zweryfikowane inteligentne kontrakty są wolne od błędów, luk w zabezpieczeniach i innych niezamierzonych zachowań. Pomaga także zwiększyć zaufanie do umowy, gdyż jej właściwości zostały rygorystycznie udowodnione.
Poniżej znajduje się kilka przykładów tego, jak inteligentna weryfikacja kontraktów pomogła zapobiec znaczącym stratom finansowym i innym katastrofalnym skutkom.
Uniswap
Uniswap to dobrze znany AMM. Kiedy opracowywano inteligentną umowę Uniswap V1, została ona formalnie zweryfikowana. Przed publikacją ta formalna weryfikacja znalazła i naprawiła błędy w zaokrąglaniu, które mogły doprowadzić do wyczerpania środków z Uniswapa V1.
Stabilizator
Balancer V2 to także AMM, który został formalnie zweryfikowany. Formalna weryfikacja wykazała i naprawiła nieprawidłowe obliczenie opłaty związane z funkcją pożyczki flash w inteligentnej umowie, co mogło narazić giełdę na kradzież.
Bezpieczny Księżyc
SafeMoon V1 zawierał subtelny błąd wykryty w drodze formalnej weryfikacji po wdrożeniu. Właściciel miał możliwość zrzeczenia się własności umowy, a następnie jej ponownego nabycia, jeśli przed zrzeczeniem się własności dokonał pewnych czynności.
Ten błąd został pominięty w większości ręcznych audytów forków SafeMoon V1, ponieważ jego znalezienie wymagało przeanalizowania określonych kombinacji wartości zmiennych programu. Jest to coś, co łatwo przeoczyć ludzie i łatwo wyłapać maszyna.
Jak weryfikacja formalna i audyt ręczny współdziałają
Weryfikacja formalna zapewnia systematyczny i zautomatyzowany sposób sprawdzania logiki i zachowania umowy pod kątem jej pożądanych właściwości. Dzięki temu łatwiej jest zidentyfikować i naprawić potencjalne błędy lub błędy. Jest to szczególnie przydatne do wyszukiwania złożonych i subtelnych problemów, które mogą być trudne do wykrycia podczas ręcznej kontroli.
Ręczny audyt obejmuje ekspertyzę dotyczącą kodu, projektu i wdrożenia umowy. Audytor wykorzystuje swoje doświadczenie i wiedzę specjalistyczną do identyfikacji zagrożeń bezpieczeństwa i oceny ogólnego stanu bezpieczeństwa umowy. Mogą również potwierdzić, że proces weryfikacji formalnej został przeprowadzony prawidłowo i sprawdzić, czy nie występują problemy, które mogą nie zostać wykryte przez zautomatyzowane narzędzia.
Połączenie formalnej weryfikacji i ręcznego audytu zapewnia wszechstronną i dogłębną ocenę bezpieczeństwa inteligentnego kontraktu. Zwiększa to szanse na znalezienie i naprawienie luk. Rezultatem jest kompleksowe podejście do bezpieczeństwa, które wykorzystuje unikalne możliwości zarówno ludzi, jak i maszyn.
Zamykające myśli
Aby zapewnić bezpieczeństwo inteligentnych kontraktów, konieczne jest zastosowanie zarówno weryfikacji formalnej, jak i ręcznego audytu, aby zapewnić wszechstronną i dogłębną ocenę stanu bezpieczeństwa inteligentnego kontraktu.
Chociaż formalna weryfikacja może wymagać dużych zasobów, jest to opłacalna inwestycja w przypadku umów o dużej wartości lub czynnikach wysokiego ryzyka. Ostatecznie kluczowe znaczenie ma nadanie priorytetu bezpieczeństwu i zapewnienie, że inteligentne kontrakty są wolne od błędów, luk w zabezpieczeniach i niezamierzonych zachowań.
Dalsze czytanie
Czym są inteligentne kontrakty?
Co to jest audyt bezpieczeństwa inteligentnych kontraktów?
Zastrzeżenie i ostrzeżenie o ryzyku: Niniejsza treść jest prezentowana użytkownikowi w stanie „takim, jakim jest” wyłącznie w celach informacyjnych i edukacyjnych, bez jakichkolwiek oświadczeń ani gwarancji. Nie należy jej interpretować jako porady finansowej, prawnej lub innej profesjonalnej, ani też nie ma na celu rekomendowania zakupu jakiegokolwiek konkretnego produktu lub usługi. Powinieneś zasięgnąć porady u odpowiednich profesjonalnych doradców. Jeśli artykuł został napisany przez osobę trzecią, pamiętaj, że wyrażone poglądy należą do osoby trzeciej i niekoniecznie odzwierciedlają poglądy Binance Academy. Aby uzyskać więcej informacji, prosimy o zapoznanie się z naszym pełnym zastrzeżeniem tutaj. Ceny aktywów cyfrowych mogą być zmienne. Wartość Twojej inwestycji może spaść lub wzrosnąć, a zainwestowana kwota może nie zostać zwrócona. Ponosisz wyłączną odpowiedzialność za swoje decyzje inwestycyjne, a Binance Academy nie ponosi odpowiedzialności za jakiekolwiek straty, które możesz ponieść. Materiał ten nie powinien być interpretowany jako porada finansowa, prawna lub inna profesjonalna. Aby uzyskać więcej informacji, zapoznaj się z naszymi Warunkami użytkowania i Ostrzeżeniem o ryzyku.
