W czerwcu 2016 r. panowało wielkie podekscytowanie faktem, że „The DAO”, zbudowany na blockchainie Ethereum, miał stać się pierwszym na świecie w pełni cyfrowym, zdecentralizowanym funduszem inwestycyjnym.
Jednak w ciągu kilku tygodni stał się plakatowym przykładem hacków DeFi po tym, jak napastnicy ukradli mu eter o wartości 50 milionów dolarów.
Aby złamać DAO, osoba atakująca wykorzystała tak zwaną lukę w zabezpieczeniach umożliwiającą współbieżność, w której wywoływana jest jedna metoda konkretnego inteligentnego kontraktu, podczas gdy inna metoda jest nadal wykonywana, a DAO jest jedynie częścią długoterminowego rozwoju Inteligentny kontrakt zawiera takie błędy.
Do wybitnych następców należą Uniswap/Lendf.Me, któremu w 2020 r. skradziono 25 mln dolarów, CREAM, któremu w 2021 r. skradziono 18 mln dolarów, oraz Fei, któremu w 2022 r. skradziono 80 mln dolarów.
Powodem, dla którego te błędy się utrzymują, jest to, że mogą obejmować nieoczekiwane interakcje z kodem rozproszone po całym inteligentnym kontrakcie, a czasem nawet w całkowicie różnych inteligentnych kontraktach. Liczba takich interakcji z kodem może być bardzo duża, co utrudnia ludziom wykrycie i wyeliminowanie niezamierzonych inteligentnych kontraktów wymagany kod.
Co więcej, interakcje te są często trudne do automatycznego i systematycznego testowania.
TLA+: Eksterminator
Enter Temporal Logic of Actions (TLA+), język służący do specyfikowania i sprawdzania złożonych systemów. TLA+ nie tylko znajduje błędy, ale także weryfikuje ich istnienie.
Jak to możliwe, pytasz? TLA+ posiada zestaw narzędzi do lekkiej weryfikacji formalnej w postaci tzw. sprawdzania modelowego. Poprzez sprawdzanie modelu wyczerpująco bada wszystkie możliwe współbieżne interakcje modelu kodu – czyli te same obszary, które są trudne do przetestowania – i znajduje błędy.
Wyobraź sobie eksterminatora, który oświetla każdy zakamarek, aby odsłonić i wyeliminować niechciane szkodniki ukrywające się w ciemnych zakamarkach, które często są pomijane lub ignorowane. Co ważne, po zbudowaniu modelu kodu sprawdzenie modelu nie wymaga prawie żadnego udziału człowieka, co czyni go bardzo opłacalnym.
Aby zilustrować to kilkoma wymyślonymi liczbami: jeśli standardowe praktyki branżowe, takie jak testowanie i przeglądy bezpieczeństwa, eliminują 80% błędów, a „ciężka” formalna weryfikacja eliminuje 99%, użycie TLA+ eliminuje 90% za pomocą tylko jednego. Niewielka liczba ciężkich prób weryfikacyjnych.
TLA+ i komputery internetowe
Nasz zespół inżynierów wykorzystuje TLA+ do analizowania wszystkich aspektów przetwarzania danych w Internecie, w tym inteligentnych kontraktów o krytycznym znaczeniu dla bezpieczeństwa, które działają na platformie. Chociaż komputery Ethereum i komputery internetowe mają różne modele wykonywania, błędy ponownego wejścia mogą pojawić się w inteligentnych kontraktach w obu łańcuchach bloków.
W rzeczywistości, ze względu na wysoką przepustowość, komputery internetowe umożliwiają wiele jednoczesnych wywołań pojedynczego inteligentnego kontraktu, co wymaga od autorów inteligentnych kontraktów większej ostrożności w celu wyeliminowania niepożądanych jednoczesnych interakcji. Ponieważ bezpieczeństwo ma kluczowe znaczenie dla powodzenia komputerów w Internecie, w wielu inteligentnych kontraktach stosuje się TLA+ w celu wykrywania błędów na etapie programowania.
Niedawno przeprowadzono analizę kontenera TLA+ (inteligentne kontrakty dla komputerów w Internecie) na nowo wydanym Bitcoinie Chain-Key (ckBTC), którego wynikami podzielę się poniżej.
Inteligentny kontrakt ckBTC
Aby porozmawiać o analizie TLA+ ckBTC, zacznijmy od ogólnego przeglądu ckBTC. ckBTC to natywny token komputera internetowego, bezpiecznie wspierany przez Bitcoin (BTC) w stosunku 1:1.
Księga ckBTC to inteligentny kontrakt kontenerowy w internetowym łańcuchu bloków komputera, który śledzi, ile ckBTC posiada każdy użytkownik końcowy. Ta sama księga umożliwia użytkownikom końcowym przesyłanie swoich ckBTC innym użytkownikom końcowym szybciej i taniej niż przesyłanie BTC w sieci Bitcoin.
Aby przekonwertować ckBTC na BTC i odwrotnie, użytkownicy końcowi korzystają z innego inteligentnego kontraktu, ckBTC minter.
Na wysokim poziomie operacja konwersji z BTC na ckBTC wygląda następująco:
Kroki, aby uzyskać ckBTC:
1. Użytkownik końcowy najpierw przekazuje część BTC na specyficzny dla użytkownika adres depozytu Bitcoin, wszystkie adresy depozytu są w pełni kontrolowane przez kod inteligentnego kontenera ckBTC minter ze względu na podpis klucza ECDSA klucza łańcuchowego, który tworzy nowy UTXO będący własnością depozytu adres;
2. Użytkownik końcowy powiadamia inteligentną umowę ckBTC mint o nowo zdeponowanym UTXO, prosząc mennicę o aktualizację salda użytkownika;
3. Inteligentny kontrakt Minter wykorzystuje następnie integrację Bitcoin z komputerami internetowymi, aby pobrać wszystkie UTXO należące do kontrolowanego przez Minter, ale specyficznego dla użytkownika adresu depozytu. Minter następnie wybiera nowe UTXO z sieci Bitcoin, wysyłając je do kontroli krzyżowej wewnętrzną listę księgową przetwarzanych przez siebie UTXO;
4. Na koniec minter instruuje księgę, aby wybiła nowe ckBTC dla wszystkich nowych UTXO w stosunku 1:1, a po zakończeniu dodaje nowo odkryte UTXO do listy przetworzonych UTXO.
Zastrzeżenie: Powyższy proces dla uproszczenia pomija proces KYT (Know Your Transaction).
Inteligentna umowa ckBTC spełnia wymogi TLA+
Przedstawiony powyżej ogólny obraz w rzeczywistości kryje subtelny problem ze współbieżnością, a dobrą wiadomością jest to, że możemy wykryć problem za pomocą zestawu narzędzi TLA+.
Zanim jednak TLA+ będzie mógł cokolwiek wykryć, musimy najpierw zapewnić mu dwie rzeczy:
Stwórz model naszego systemu wykorzystując język TLA+
Określ właściwości TLA+, których oczekujemy od wdrożenia systemu
Model ten jest uproszczoną, ale wciąż w pełni zdefiniowaną wersją systemu, która w naszym przypadku obejmuje inteligentny kontrakt Minter, ale także wszystkie inne istotne części systemu, a mianowicie umowę księgi głównej i sieć Bitcoin.
Dla każdego komponentu modelujemy jego stan oraz sposób, w jaki odpowiednie działania, jakie może podjąć użytkownik końcowy (tj. transfer BTC lub ckBTC, zdeponowanie BTC lub wywołanie różnych działań ujawnionych przez mennicę) zmieniają stan.
Wszystkie te elementy są w modelu nieco uproszczone, przy czym części, na których skupia się analiza (np. kod mintera), są modelowane bardziej szczegółowo, podczas gdy inne części (np. sieć Bitcoin) są modelowane mniej szczegółowo, w rzeczywistości model TLA+ jest podobny do szczegółowej specyfikacji projektu systemu.
Intuicyjnie, główną funkcją, którą chcemy wdrożyć, jest zapewnienie pełnego wsparcia naszego ckBTC. Innymi słowy, żaden użytkownik końcowy nie powinien mieć możliwości „podwójnego wydania” zdeponowanych BTC, aby otrzymać więcej ckBTC niż zdeponował.
Aby jednak przeanalizować taką właściwość, musimy bardzo sprecyzować tę intuicję, wyrażając ją formalnie w języku TLA+. Nasza formalna definicja jest taka, że całkowita podaż ckBTC (tj. suma wszystkich sald ckBTC użytkowników końcowych przechowywanych w księdze ckBTC) nie przekracza całkowitej ilości BTC kontrolowanej przez pojemnik menniczy (tj. wartości wszystkich UTXO będące własnością adresu depozytowego).
Wykrywaj i rozwiązuj problemy
Po utworzeniu modelu i właściwości zestaw narzędzi TLA+ może przeprowadzić analizę modelu. Aby przeprowadzić analizę, najpierw definiujemy ustawienia jej przeprowadzenia. Na przykład nasza konfiguracja dla ckBTC obejmuje tylko dwóch różnych użytkowników końcowych i niewielką część całkowitej podaży Bitcoinów (np. 5 satoshi).
Chociaż to ustawienie jest bardzo ograniczone, badania empiryczne pokazują, że zdecydowaną większość problemów w systemach komputerowych można znaleźć w niewielkiej liczbie jednostek. Mała konfiguracja pozwala na systematyczne badanie wszystkich możliwych sekwencji działań zdefiniowanych przez model i sprawdzanie, czy określone właściwości mieszczą się w dowolnej takiej sekwencji.
Co więcej, analiza przebiega całkowicie automatycznie, tj. nie wymaga żadnego udziału człowieka, a jeśli te właściwości nie są spełnione, podaje nam dokładną sekwencję operacji, która narusza tę właściwość.
Na przykład analiza może wykazać, że możemy naruszyć naszą właściwość „brak niezabezpieczonych ckBTC” w scenariuszu takim jak ten przedstawiony poniżej:
Tutaj:
Użytkownicy końcowi wpłacają BTC tak samo jak poprzednio;
Jednak teraz użytkownik końcowy instruuje mennicę ckBTC, aby dwukrotnie z rzędu zaktualizowała saldo, a na komputerze internetowym aktualizacje te mogą być jednocześnie interakcji z innymi inteligentnymi kontraktami;
Dwie uruchomione jednocześnie aktualizacje pytają sieć Bitcoin o wszystkie UTXO zdeponowane przez użytkownika końcowego i obie otrzymują w odpowiedzi ten sam UTXO zdeponowany w kroku 1. Ponieważ UTXO nie znajduje się jeszcze na liście „przetworzonych”, obie aktualizacje uważają, że UTXO jest nowe;
Obie aktualizacje instruują księgę, aby w kroku 4 wybiła odpowiednią ilość ckBTC.
Dlatego na końcu kroku 4 jesteśmy w stanie, w którym podaż ckBTC jest dwukrotnie większa od sumy UTXO w adresach depozytów, co narusza naszą właściwość „brak nieobsługiwanego ckBTC”.
Należy pamiętać, że ten błąd występuje tylko dlatego, że aktualizacje salda użytkownika końcowego są wykonywane jednocześnie — w rzeczywistości jest to błąd powtarzający się w tym samym stylu, co ten, który spowodował wyłączenie DAO.
Jednym ze sposobów rozwiązania tego problemu jest uniemożliwienie równoległego uruchamiania aktualizacji salda dla tego samego użytkownika końcowego. Możemy to zrobić poprzez polecenie mennicy przechowywania użytkownika końcowego na „zablokowanej” liście użytkowników po rozpoczęciu aktualizacji salda i trzymania ich tam aby to osiągnąć, na czas trwania listy aktualizacji.
Jeśli użytkownik końcowy podejmie próbę zainicjowania kolejnej jednoczesnej aktualizacji salda, aktualizacja najpierw sprawdzi i znajdzie tego konkretnego użytkownika końcowego na liście zablokowanych użytkowników, a następnie zostanie przerwana.
Zauważ, że nieco upraszczamy tutaj atak: blokowanie jest w rzeczywistości dość powszechnym wzorcem w przypadku inteligentnych kontraktów IC, a mennicy ckBTC stosowali go od początku. Jednak nieprawidłowo wykonane blokowanie otwiera drzwi do powyższych ataków, które TLA+ jest w stanie wykryć.
Dodatkowo znaleźliśmy kilka przypadków Edge, które naruszały zasadę „brak nieobsługiwanego ckBTC” i inne ważne właściwości, a po zastosowaniu wszystkich poprawek firma TLA+ była w stanie zweryfikować i potwierdzić, że w naszej zdefiniowanej konfiguracji nie było już więcej naruszeń właściwości.
Czy powinieneś używać TLA+ do swoich inteligentnych kontraktów?
Absolutnie! OK, OK, może powinienem podać bardziej zniuansowaną odpowiedź, której nasz zespół badawczo-rozwojowy używa w przypadku kluczowych inteligentnych kontraktów na komputerach internetowych, ilekroć w grę wchodzi nietrywialna współbieżność.
Na przykład analiza TLA+ ujawniła subtelne błędy współbieżności w zarządzaniu komputerem w Internecie i kontenerach księgi głównej, które pominięto we wcześniejszych ręcznych przeglądach bezpieczeństwa i które mogły prowadzić do poważnych problemów, przypadków i punktów — TLA+ odegrał kluczową rolę w odkryciu takich drażliwych problemów. Absolutny sukces.
Oczywiście zdobycie know-how, a następnie zbudowanie modelu ma swoją cenę, ale z empirycznego punktu widzenia cena jest rozsądna, szczególnie biorąc pod uwagę wysoką stawkę bezpieczeństwa blockchain.
Nie należy się bać samego języka TLA+, pomimo odstraszającej nazwy, dostęp do jego potężnych funkcji jest dość prosty. W rzeczywistości ściągawka TLA+ opisująca prawie wszystkie funkcje TLA+ z grubsza zmieściłaby się na stronie:
mbt.formal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
Co więcej, wysiłek wymagany do zbudowania modelu jest porównywalny ze standardowymi ręcznymi przeglądami bezpieczeństwa. Na przykład mennicy ckBTC zrozumienie projektu, stworzenie początkowego modelu i właściwości zajęłoby 1 osobie łącznie około 3 tygodni.
Powstały model TLA+ jest znacznie prostszy niż implementacja, zarówno dlatego, że jest prostszy niż kod, jak i ze względu na wysokopoziomowy charakter TLA+. Model mintera ckBTC wymaga około 250 linii kodu w porównaniu do tysięcy linii implementacji Rusta. Być może zaskakujące jest to, że jedną z najtrudniejszych części pod względem wysiłku jest określenie wymaganych właściwości, ponieważ często można znaleźć luki w intuicyjnych specyfikacjach.
Gdy model jest już gotowy, analiza (sprawdzanie modelu) kończy się automatycznie. Analiza może zająć dużo czasu – na przykład w przypadku ckBTC zajęło to ponad 20 godzin. Wreszcie kolejną zaletą TLA jest to, że modelowanie i analizę można przeprowadzić na etapie projektowania, przed wdrożeniem kodu, co pomaga wyeliminować duże refaktoryzacje wynikające z późniejszych błędów projektowych.
Gdzie TLA+ jest bezużyteczny
Z drugiej strony, TLA+ jest mniej pomocny w przypadku złożonych programów sekwencyjnych, w przeciwieństwie do programów współbieżnych, a także nie radzi sobie dobrze ze złożonymi protokołami kryptograficznymi, dla których istnieją inne, bardziej przydatne narzędzia (np. Tamarin).
Wreszcie pojawia się kwestia synchronizacji modelu TLA+ i rzeczywistej implementacji, ponieważ kod implementacji ewoluuje z biegiem czasu i może nie być już zgodny z modelem, co może być trudne do uchwycenia bez wsparcia narzędziowego.
Tak naprawdę nasz zespół badawczo-rozwojowy próbuje rozwiązać ten problem – mam nadzieję, że wkrótce będziemy mogli udostępnić Ci kilka narzędzi!
Mam nadzieję, że ten przegląd wzbudził Twoje zainteresowanie wykorzystaniem TLA+ w swoich własnych, kluczowych inteligentnych kontraktach, a jeśli tak, bądź na bieżąco – wkrótce pojawi się kolejny post z bardziej szczegółowym samouczkiem na temat korzystania z TLA+ w przypadku inteligentnych kontraktów, W załączniku znajduje się rzeczywisty model TLA+ opracowany przez nasz zespół badawczo-rozwojowy.
Treści IC, na których Ci zależy
Postęp technologiczny |. Informacje o projekcie |. Wydarzenia globalne
Zbieraj i śledź kanał IC Binance
Bądź na bieżąco z najświeższymi informacjami