Ten artykuł został opublikowany przez członka społeczności. Autorem jest David Tarditi, wiceprezes ds. inżynierii w CertiK, firmie audytującej inteligentne kontrakty Web3.

Streszczenie

Formalna weryfikacja inteligentnych kontraktów chroni je przed błędami, podatnościami i innymi niekorzystnymi warunkami. W tym procesie eksperci przekształcają logikę inteligentnego kontraktu w stwierdzenia matematyczne, a następnie wykorzystują zautomatyzowany proces do sprawdzenia rzeczywistej logiki z modelem oczekiwanego zachowania kontraktu. Łącząc weryfikację formalną i audyt manualny, możemy przeprowadzić kompleksową ocenę bezpieczeństwa inteligentnych kontraktów.

Wstęp

Inteligentne kontrakty to programy komputerowe wdrażane w łańcuchu bloków, które uruchamiają się automatycznie po spełnieniu określonych warunków. Inteligentne kontrakty mogą być bardzo proste lub niezwykle złożone i mogą zawierać aktywa warte miliony, a nawet miliardy dolarów.

Jeśli w kodzie inteligentnego kontraktu występują luki w zabezpieczeniach, może to mieć katastrofalne skutki, takie jak kradzież wszystkich aktywów znajdujących się w posiadaniu przestępców. W 2021 r. skradziono 50 milionów dolarów automatycznemu animatorowi rynku (AMM) Uranium Finance z powodu literówki w inteligentnej umowie.

Również w 2021 r. firma Compound Finance omyłkowo przyznała nagrody w wysokości 80 mln dolarów z powodu pojedynczego błędu w kodowaniu. W 2022 roku z Wormhole Bridge skradziono 320 milionów dolarów z powodu błędu w inteligentnej umowie.

Dlatego ważne jest, aby od samego początku wdrożyć program inteligentnych kontraktów. Inteligentne kontrakty wykorzystują model open source, co oznacza, że ​​po wdrożeniu kontraktu kod zostaje upubliczniony. Jeśli haker odkryje błąd, może go natychmiast wykorzystać. Ponadto normalna praktyka polegająca na łataniu luk w zabezpieczeniach z biegiem czasu jest nieskuteczna, ponieważ kodu inteligentnych kontraktów często nie można modyfikować po wdrożeniu.

Jak działa inteligentna weryfikacja kontraktu?

Formalną weryfikację inteligentnych kontraktów osiąga się poprzez przedstawienie logiki i oczekiwanego zachowania inteligentnego kontraktu w postaci stwierdzeń matematycznych. Następnie audytorzy korzystają z zautomatyzowanych narzędzi, aby sprawdzić, czy te stwierdzenia są prawidłowe.

Proces obejmuje:

  1. Zdefiniuj specyfikacje i oczekiwane cechy zamówienia w języku formalnym.

  2. Przekształć kod umowy w formalne oświadczenie, takie jak model matematyczny lub logika.

  3. Weryfikuj specyfikacje i właściwości kontraktu, korzystając z automatycznego dowodzenia twierdzeń lub sprawdzania modelu.

  4. Powtórz proces walidacji, aby znaleźć i naprawić wszelkie błędy lub odchylenia od oczekiwanych cech.

Dlaczego inteligentna weryfikacja kontraktu jest ważna

Stosując rozumowanie matematyczne, pomaga upewnić się, że formalnie zweryfikowane inteligentne kontrakty są wolne od błędów, podatności i innych niekorzystnych sytuacji. Weryfikacja pomaga również zwiększyć zaufanie do umowy, ponieważ jej właściwości zostały rygorystycznie przetestowane i są prawidłowe i niezawodne.

Poniższe przykłady pokazują, jak inteligentna weryfikacja umów może pomóc w zapobieganiu znaczącym stratom finansowym i innym katastrofalnym konsekwencjom.

Uniswap

Uniswap to dobrze znany AMM. Inteligentny kontrakt Uniswap V1 przeszedł formalną weryfikację w procesie rozwoju. Przed wydaniem ta formalna weryfikacja znalazła i naprawiła pewne błędy zaokrągleń, zapobiegając wyczerpaniu środków Uniswap V1.

Stabilizator

Balancer V2 to także sprawdzony AMM. Formalna weryfikacja odkryła i naprawiła błąd w obliczaniu opłaty w funkcji pożyczki flash w inteligentnej umowie, który narażał platformę transakcyjną na kradzież.

Bezpieczny Księżyc

Po wdrożeniu SafeMoon V1 w wyniku formalnej weryfikacji wykryto bardzo mały błąd. Jeżeli błąd nie został wykryty, a właściciel umowy wykonał pewne operacje przed zrzeczeniem się własności, właściciel umowy mógłby go odzyskać po zrzeczeniu się umowy.

Większość ręcznych audytów forka SafeMoon V1 pomija ten błąd, ponieważ aby go znaleźć, należy przeanalizować określone kombinacje wartości zmiennych programu. Ludzie mogą łatwo przeoczyć ten problem, ale maszyny mogą go wychwycić na czas.

Jak weryfikacja formalna i audyt ręczny współdziałają ze sobą

Weryfikacja formalna zapewnia systematyczny i zautomatyzowany sposób sprawdzenia logiki i zachowania umowy pod kątem jej oczekiwanych cech. Dzięki temu łatwiej jest zidentyfikować i naprawić potencjalne błędy lub luki w zabezpieczeniach. Jest to szczególnie przydatne w przypadku złożonych, subtelnych problemów, które byłyby trudne do wykrycia poprzez ręczną kontrolę.

Audyt ręczny obejmuje ekspertów przeglądających kod, projekt i wdrożenie kontraktu. Audytorzy wykorzystują 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órych zautomatyzowane narzędzia mogłyby nie wykryć.

Łącząc weryfikację formalną i audyt manualny, możemy przeprowadzić kompleksową ocenę bezpieczeństwa inteligentnych kontraktów. Zwiększa to szanse na znalezienie i naprawienie luk. W ten sposób przyjmujemy podejście do bezpieczeństwa obejmujące głęboką obronę, które łączy wiedzę ludzi i maszyn.

Wniosek

Aby zapewnić bezpieczeństwo inteligentnych kontraktów, należy połączyć weryfikację formalną i ręczny audyt, aby zapewnić kompleksową i dogłębną ocenę stanu bezpieczeństwa inteligentnych kontraktów.

Chociaż weryfikacja formalna wymaga większych zasobów, jest to opłacalna inwestycja w przypadku umów o dużej wartości lub czynnikach wysokiego ryzyka. W końcu bezpieczeństwo jest ważniejsze niż cokolwiek innego. Upewnij się, że priorytetowo traktujesz bezpieczeństwo i upewnij się, że inteligentne kontrakty są wolne od błędów, luk w zabezpieczeniach i niepożądanych, nieoczekiwanych zachowań.

Dalsza lektura

  • Czym jest inteligentny kontrakt?

  • Czym jest audyt bezpieczeństwa inteligentnych kontraktów?

Zastrzeżenie i ostrzeżenie o ryzyku: Treść tego artykułu stanowi fakty i służy wyłącznie celom informacyjnym i edukacyjnym i nie stanowi żadnego oświadczenia ani gwarancji. Tego artykułu nie należy interpretować jako porady finansowej i nie zaleca zakupu żadnego konkretnego produktu lub usługi. Ceny aktywów cyfrowych mogą się zmieniać. Wartość Twojej inwestycji może zarówno spaść, jak i wzrosnąć, a Ty możesz nie odzyskać zainwestowanego kapitału. Ponosisz wyłączną odpowiedzialność za swoje własne decyzje inwestycyjne, a Binance Academy nie ponosi odpowiedzialności za jakiekolwiek straty, które możesz ponieść. Niniejszy materiał nie stanowi porady finansowej.