V červnu 2016 vzplanulo nadšení, že „The DAO“, postavený na blockchainu Ethereum, se brzy stane prvním plně digitálním, decentralizovaným investičním fondem na světě.
Ale během několika týdnů se místo toho stal plakátovým dítětem pro hacky DeFi poté, co z něj útočníci ukradli éter v hodnotě 50 milionů dolarů.
K hacknutí The DAO útočník zneužil takzvanou reentrancy zranitelnost, zranitelnost souběžnosti, kdy je volána jedna metoda konkrétního smart kontraktu, zatímco jiná metoda se stále provádí, a The DAO je pouze součástí dlouhodobého vývoje chytrá smlouva. První z nich trpí takovými chybami.
Mezi prominentní nástupce patří Uniswap/Lendf.Me, kterému bylo v roce 2020 ukradeno 25 milionů dolarů, CREAM, kterému bylo v roce 2021 ukradeno 18 milionů dolarů, a Fei, kterému bylo v roce 2022 ukradeno 80 milionů dolarů.
Důvodem, proč tyto chyby přetrvávají, je to, že mohou zahrnovat neočekávané interakce kódu rozptýlené po celém smart kontraktu, někdy dokonce i v úplně různých smart kontraktech. Počet takových interakcí s kódem může být velmi velký, takže pro lidi je obtížné odhalit a odstranit nechtěné smart kontrakty .
Navíc je často obtížné tyto interakce testovat automaticky a systematicky.
TLA+: The Exterminator
Enter Temporal Logic of Actions (TLA+), jazyk pro specifikaci a ověřování složitých systémů TLA+ nejen najde chyby, ale také ověří jejich existenci.
Jak je to možné, ptáte se? TLA+ přichází se sadou nástrojů pro odlehčenou formální verifikaci v podobě tzv. model checkingu. Prostřednictvím kontroly modelu vyčerpávajícím způsobem prozkoumává všechny možné souběžné interakce modelu kódu – právě oblasti, které se obtížně testují – a nachází chyby.
Představte si deratizátora, který osvětlí každý kout a skulinu, aby odhalil a odstranil nežádoucí škůdce skrývající se v těch temných zákoutích, které jsou často přehlíženy nebo ignorovány. Důležité je, že po sestavení modelu kódu lze kontrolu modelu spustit prakticky bez lidského zásahu, což je vysoce nákladově efektivní.
Pro ilustraci s některými smyšlenými čísly: Pokud standardní postupy, jako je testování a bezpečnostní kontroly, eliminují 80 % chyb a „těžká“ formální verifikace eliminuje 99 %, použití TLA+ eliminuje 90 % pouze jedním. Malý počet pokusů o těžké ověření.
TLA+ a internetové počítače
Náš technický tým používá TLA+ k analýze všech aspektů výpočetní techniky na internetu, včetně inteligentních smluv kritických z hlediska zabezpečení, které na platformě běží. Přestože Ethereum a internetové počítače mají různé modely provádění, chyby opětovného vstupu se mohou objevit v chytrých kontraktech na obou blockchainech.
Internetové počítače ve skutečnosti díky své vysoké propustnosti umožňují více souběžných volání do jedné chytré smlouvy, což vyžaduje, aby autoři chytrých smluv byli opatrnější, aby eliminovali nežádoucí souběžné interakce. Vzhledem k tomu, že zabezpečení je pro úspěch počítačů na internetu zásadní, používá se TLA+ v mnoha inteligentních smlouvách k detekci chyb během vývojové fáze.
Nedávno byl proveden kontejner analýzy TLA+ (inteligentní smlouvy pro počítače na internetu) na nově vydaném bitcoinu s řetězovým klíčem (ckBTC), jehož výsledky se podělím níže.
inteligentní smlouva ckBTC
Chcete-li mluvit o TLA+ analýze ckBTC, začněme s přehledem ckBTC na vysoké úrovni. ckBTC je internetový počítačový nativní token bezpečně podporovaný bitcoiny (BTC) v poměru 1:1.
Kniha ckBTC je kontejnerová inteligentní smlouva na internetovém počítačovém blockchainu, která sleduje, kolik ckBTC vlastní každý koncový uživatel. Stejná účetní kniha umožňuje koncovým uživatelům převádět své ckBTC jiným koncovým uživatelům rychleji a levněji než převod BTC v síti bitcoinů.
Aby bylo možné převést ckBTC na BTC a zpět, koncoví uživatelé interagují s jinou inteligentní smlouvou, ckBTC minter.
Na vysoké úrovni operace převodu z BTC na ckBTC vypadá takto:
Kroky k získání ckBTC:
1. Koncový uživatel nejprve převede nějaké BTC na uživatelsky specifickou bitcoinovou vkladovou adresu, všechny vkladové adresy jsou plně řízeny kódem chytrého kontejneru ckBTC minter díky řetězovému klíči ECDSA podpisu, který vytváří nové UTXO vlastněné vkladem adresa;
2. Koncový uživatel oznámí smart kontraktu ckBTC mint nově uložené UTXO tím, že požádá mincovnu o aktualizaci uživatelského zůstatku;
3. Inteligentní smlouva minteru pak využívá bitcoinovou integraci internetových počítačů k načtení všech UTXO vlastněných minerem řízenou, ale uživatelsky specifickou depozitní adresou Miner pak třešničkou vybere nové UTXO z bitcoinové sítě tím, že jim pošle křížové kontroly svůj interní účetní seznam UTXO, které zpracoval;
4. Nakonec minter instruuje účetní knihu, aby razila nové ckBTC pro všechna nová UTXO v poměru 1:1 a po dokončení přidá nově objevená UTXO do seznamu zpracovaných UTXO.
Prohlášení: Výše uvedený proces pro jednoduchost vynechává proces KYT (Know Your Transaction).
Chytrý kontrakt ckBTC splňuje TLA+
Výše uvedený obrázek na vysoké úrovni ve skutečnosti skrývá jemný problém souběžnosti a dobrou zprávou je, že problém můžeme odhalit pomocí sady nástrojů TLA+.
Než však může TLA+ něco detekovat, musíme mu nejprve poskytnout dvě věci:
Vytvořte model našeho systému pomocí jazyka TLA+
Zadejte vlastnosti TLA+, které očekáváme od systému
Tento model je zjednodušenou, ale stále plně definovanou verzí systému, která v našem případě zahrnuje minter smart contract, ale i všechny další relevantní části systému, tedy ledger contract a bitcoinovou síť.
Pro každou komponentu modelujeme její stav a jak příslušné akce, které může koncový uživatel provést (tj. převod BTC nebo ckBTC, uložení BTC nebo vyvolání různých akcí vystavených minterem), změní stav.
Všechny tyto prvky jsou v modelu poněkud zjednodušeny, přičemž části, na které se analýza zaměřuje (např. minter kód), jsou modelovány podrobněji, zatímco ostatní části (např. bitcoinová síť) jsou modelovány méně podrobně, ve skutečnosti je model TLA+ je podobný podrobné specifikaci návrhu systému.
Intuitivně je hlavní funkcí, kterou chceme implementovat, zajistit plnou podporu našeho ckBTC. Jinými slovy, žádný koncový uživatel by neměl mít možnost „zdvojnásobit“ své vložené BTC, aby získal více ckBTC, než vložil.
Abychom však takovou vlastnost mohli analyzovat, musíme tuto intuici velmi zpřesnit tím, že ji formálně vyjádříme v jazyce TLA+. Naše formální definice je, že celková nabídka ckBTC (tj. součet všech zůstatků ckBTC koncových uživatelů, jak jsou uloženy v knize ckBTC) nepřesahuje celkové množství BTC kontrolované razícím kontejnerem (tj. UTXO vlastněné depozitní adresou) .
Zjistit a vyřešit problémy
Jakmile vytvoříme model a vlastnosti, sada nástrojů TLA+ může model analyzovat Pro spuštění analýzy nejprve definujeme nastavení pro spuštění analýzy. Například naše nastavení pro ckBTC zahrnuje pouze dva různé koncové uživatele a malé množství z celkové nabídky bitcoinů (např. 5 satoshi).
Přestože je toto nastavení velmi omezené, empirické studie ukazují, že převážnou většinu problémů v počítačových systémech lze nalézt u malého počtu subjektů. Malé nastavení umožňuje analýze systematicky prozkoumat všechny možné akční sekvence definované modelem a ověřit, zda jsou předepsané vlastnosti u každé takové sekvence dodrženy.
Analýza navíc probíhá zcela automaticky, tedy nevyžaduje žádný lidský zásah, a pokud tyto vlastnosti neplatí, poskytuje nám přesnou sekvenci operací, které tuto vlastnost porušují.
Analýza může například odhalit, že můžeme porušit naši vlastnost „no unsecured ckBTC“ ve scénáři, jako je ten na obrázku níže:
tady:
Koncoví uživatelé vkládají BTC stejně jako dříve;
Nyní však koncový uživatel dá pokyn ckBTC minteru, aby aktualizoval zůstatek dvakrát rychle za sebou a na internetovém počítači mohou být tyto aktualizace současně propojeny s jinými smart kontrakty;
Dvě aktualizace běžící současně požádají bitcoinovou síť o všechna UTXO uložená koncovým uživatelem a obě obdrží jako odpověď stejné UTXO uložené v kroku 1. Protože UTXO ještě není v „zpracovaném“ seznamu, obě aktualizace Think UTXO jsou nové;
Obě aktualizace instruují účetní knihu, aby v kroku 4 razila odpovídající množství ckBTC.
Na konci kroku 4 jsme tedy ve stavu, kdy nabídka ckBTC je dvojnásobkem součtu UTXO na depozitních adresách, což porušuje naši vlastnost „no unsupported ckBTC“.
Všimněte si, že k této chybě dochází pouze proto, že aktualizace zůstatku koncového uživatele jsou prováděny souběžně – ve skutečnosti se jedná o opakovanou chybu ve stejném stylu jako ta, která způsobila pokles DAO.
Jedním ze způsobů, jak tento problém vyřešit, je zabránit tomu, aby aktualizace zůstatku probíhaly paralelně pro stejného koncového uživatele, můžeme to udělat tak, že miner uloží koncového uživatele do „uzamčeného“ seznamu uživatelů, když se spustí aktualizace zůstatku, a tam je ponechá. po dobu trvání aktualizačního seznamu, aby toho bylo dosaženo.
Pokud se koncový uživatel pokusí zahájit další souběžnou aktualizaci zůstatku, aktualizace nejprve zkontroluje a najde tohoto konkrétního koncového uživatele v seznamu uzamčených uživatelů a poté se přeruší.
Všimněte si, že zde útok mírně zjednodušujeme: zamykání je ve skutečnosti poměrně běžným vzorem pro chytré kontrakty IC a minters ckBTC jej nasazovali od začátku. Nevhodně provedené zamykání však otevírá dveře výše uvedeným útokům, které je TLA+ schopno odhalit.
Navíc jsme našli několik okrajových případů, které porušovaly „žádné nepodporované ckBTC“ a další důležité vlastnosti, a jakmile jsme použili všechny opravy, TLA+ byla schopna ověřit a potvrdit, že v našem definovaném nastavení již nedošlo k žádnému porušení vlastností.
Měli byste pro své chytré smlouvy používat TLA+?
Absolutně! Dobře, dobře, možná bych měl poskytnout jemnější odpověď, kterou náš výzkumný a vývojový tým používá pro kritické inteligentní smlouvy na internetových počítačích, kdykoli se jedná o netriviální souběžnost.
Například analýza TLA+ odhalila jemné souběžné chyby v Internet Computer Governance a Ledger Containers, které byly přehlédnuty v dřívějších manuálních bezpečnostních kontrolách a mohly vést k významným problémům, případům a bodům – TLA+ byla nápomocná při odhalování takových ožehavých problémů. Absolutní výbuch.
Samozřejmě existuje cena, kterou je třeba zaplatit, pokud jde o získání know-how a následné vybudování modelu, ale empiricky je cena přiměřená, zejména vzhledem k vysoké povaze bezpečnosti blockchainu.
Člověk by se neměl zastrašit samotným jazykem TLA+, navzdory zastrašujícímu názvu je přístup k jeho výkonným funkcím poměrně jednoduchý. Cheat sheet TLA+ popisující téměř všechny funkce TLA+ by se ve skutečnosti vešel na stránku:
mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
A co víc, úsilí potřebné k sestavení modelu je srovnatelné se standardními manuálními bezpečnostními kontrolami. Například minerovi ckBTC by trvalo celkem asi 3 týdny, než by 1 osoba pochopila design, vytvořila počáteční model a vlastnosti.
Výsledný model TLA+ je mnohem jednodušší než implementace, a to jak proto, že je jednodušší než kód, tak kvůli povaze TLA+ na vysoké úrovni. Model pro ckBTC minter vyžaduje asi 250 řádků kódu ve srovnání s tisíci řádky implementace Rust. Možná překvapivě je jednou z nejtěžších částí z hlediska úsilí upřesnění požadovaných vlastností, protože v intuitivních specifikacích člověk často najde mezery.
Po dokončení modelu se analýza (kontrola modelu) automaticky dokončí. Analýza může trvat dlouho – například u ckBTC trvalo její dokončení více než 20 hodin. A konečně, další výhodou TLA je to, že modelování a analýzu lze provádět ve fázi návrhu před implementací kódu, což pomáhá eliminovat později velké refaktoringy kvůli chybám v návrhu.
Kde je TLA+ k ničemu
Negativní je, že TLA+ je méně užitečný pro složité sekvenční programy, na rozdíl od souběžných programů, a také není dobrý ve zpracování složitých kryptografických protokolů, pro které existují jiné nástroje (např. Tamarin), které jsou užitečnější.
Konečně je tu problém synchronizace modelu TLA+ a skutečné implementace, protože implementační kód se postupem času vyvíjí a nemusí již odpovídat modelu, což může být obtížné zachytit bez podpory nástrojů.
Ve skutečnosti se náš tým výzkumu a vývoje snaží tento problém vyřešit – doufám, že se s vámi budeme moci brzy podělit o některé nástroje!
Doufám, že tento přehled vzbudil váš zájem o používání TLA+ pro vaše vlastní kritické chytré smlouvy, a pokud ano, zůstaňte naladěni – následný příspěvek s podrobnějším návodem, jak používat TLA+ pro chytré smlouvy, bude brzy k dispozici, a Attached je skutečný model TLA+ vyvinutý naším týmem pro výzkum a vývoj.
Obsah IC, na kterém vám záleží
Technologický pokrok |. Informace o projektu |
Sbírejte a sledujte kanál IC Binance
Zůstaňte v obraze s nejnovějšími informacemi