2016. gada jūnijā valdīja satraukums par to, ka “The DAO”, kas veidota uz Ethereum blokķēdes, gatavojās kļūt par pasaulē pirmo pilnībā digitālo, decentralizēto ieguldījumu fondu.

Taču dažu nedēļu laikā tas kļuva par DeFi uzlaušanas plakātu pēc tam, kad uzbrucēji no tā nozaga ētera 50 miljonu dolāru vērtībā.

Lai uzlauztu DAO, uzbrucējs izmantoja tā saukto atkārtotas ievainojamības ievainojamību — vienlaicīguma ievainojamību, kurā tiek izsaukta viena konkrēta viedā līguma metode, kamēr cita metode joprojām tiek izpildīta, un DAO ir tikai daļa no DAO ilgtermiņa attīstības. gudrais līgums, kas cieš no šādām kļūdām.

Ievērojami pēcteči ir Uniswap/Lendf.Me, kuram 2020. gadā tika nozagti 25 miljoni USD, CREAM, kam 2021. gadā tika nozagti 18 miljoni USD, un Fei, kuram 2022. gadā tika nozagti 80 miljoni USD.

Iemesls, kāpēc šīs kļūdas joprojām pastāv, ir tas, ka tās var ietvert neparedzētas koda mijiedarbības, kas izkaisītas visā viedajā līgumā, dažreiz pat dažādos viedos līgumos. Šādu kodu mijiedarbību skaits var būt ļoti liels, tādējādi cilvēkiem ir grūti atklāt un novērst neparedzētus viedos līgumus nepieciešams kods.

Turklāt šīs mijiedarbības bieži ir grūti pārbaudīt automātiski un sistemātiski.

TLA+: iznīcinātājs

Enter Temporal Logic of Actions (TLA+) — valoda sarežģītu sistēmu noteikšanai un apstiprināšanai TLA+ ne tikai atrod kļūdas, bet arī pārbauda to esamību.

Kā tas ir iespējams, jūs jautājat? TLA+ ir aprīkots ar rīku komplektu vieglai formālai verifikācijai tā sauktās modeļa pārbaudes veidā. Izmantojot modeļa pārbaudi, tas izsmeļoši pēta visas iespējamās koda modeļa vienlaicīgās mijiedarbības — tās pašas jomas, kuras ir grūti pārbaudīt — un atrod kļūdas.

Iedomājieties iznīcinātāju, kas izgaismo katru kaktiņu un spraugu, lai atklātu un likvidētu nevēlamus kaitēkļus, kas slēpjas tajos tumšajos stūros, kuri bieži tiek palaisti garām vai ignorēti. Svarīgi ir tas, ka pēc koda modeļa izveides modeļa pārbaudei gandrīz nav vajadzīgs cilvēka ieguldījums, tāpēc tā ir ļoti rentabla.

Ilustrācijai ar dažiem izdomātiem skaitļiem: Ja nozares standarta prakse, piemēram, testēšana un drošības pārbaudes, novērš 80% kļūdu, un "smagsvara" formālā pārbaude novērš 99%, izmantojot TLA+, tiek novērsti 90% tikai ar vienu Neliels skaits smagsvara verifikācijas pasākumu.

TLA+ un interneta datori

Mūsu inženieru komanda izmanto TLA+, lai analizētu visus interneta skaitļošanas aspektus, tostarp drošībai būtiskos viedos līgumus, kas darbojas platformā. Lai gan Ethereum un interneta datoriem ir atšķirīgi izpildes modeļi, atgriešanās kļūdas var parādīties viedajos līgumos abās blokķēdes.

Faktiski, pateicoties tā lielajai caurlaidspējai, interneta datori ļauj veikt vairākus vienlaicīgus zvanus uz vienu viedo līgumu, tāpēc viedo līgumu autoriem ir jābūt uzmanīgākiem, lai novērstu nevēlamu vienlaicīgu mijiedarbību. Tā kā drošība ir ļoti svarīga datoru panākumiem internetā, TLA+ tiek izmantots daudzos viedos līgumos, lai izstrādes posmā atklātu kļūdas.

Nesen tika veikts TLA+ analīzes konteiners (viedie līgumi par datoriem internetā) nesen izlaistajā Chain-Key Bitcoin (ckBTC), un ar rezultātiem es dalīšos tālāk.

ckBTC viedais līgums

Lai runātu par ckBTC TLA+ analīzi, sāksim ar augsta līmeņa ckBTC pārskatu. ckBTC ir interneta datora vietējais marķieris, ko droši nodrošina Bitcoin (BTC) attiecībā 1:1.

ckBTC virsgrāmata ir konteinera viedais līgums interneta datoru blokķēdē, kas izseko, cik daudz ckBTC pieder katram gala lietotājam. Šī pati virsgrāmata ļauj galalietotājiem pārsūtīt savus ckBTC citiem galalietotājiem ātrāk un lētāk nekā BTC pārsūtīšana Bitcoin tīklā.

Lai pārveidotu ckBTC par BTC un atpakaļ, galalietotāji mijiedarbojas ar citu viedo līgumu, ckBTC kaltuvi.

Augstā līmenī konvertēšanas darbība no BTC uz ckBTC izskatās šādi:

Darbības, lai iegūtu ckBTC:

1. Gala lietotājs vispirms pārskaita dažus BTC uz lietotāja specifisku Bitcoin depozīta adresi, visas depozīta adreses pilnībā kontrolē ckBTC minter viedkonteinera kods ķēdes atslēgas ECDSA paraksta dēļ, kas rada jaunu UTXO, kas pieder depozītam. adrese;

2. Galalietotājs paziņo ckBTC mint viedo līgumu par tikko noguldīto UTXO, lūdzot naudas kaltuvei atjaunināt lietotāja bilanci;

3. Kalta kaltuves viedais līgums pēc tam izmanto interneta datoru Bitcoin integrāciju, lai izgūtu visus UTXO, kas pieder kaltuves kontrolētai, bet lietotājam specifiskai depozīta adresei. Pēc tam kalējs izvēlas jaunus UTXO no Bitcoin tīkla, nosūtot tiem kontrolpārbaudes. tā apstrādāto UTXO iekšējo grāmatvedības sarakstu;

4. Visbeidzot, kaltētājs uzdod virsgrāmatai izveidot jaunu ckBTC visiem jaunajiem UTXO attiecībā 1:1, un pēc pabeigšanas tas pievieno jaunatklātos UTXO apstrādāto UTXO sarakstam.

Atruna: iepriekš minētajā procesā vienkāršības labad netiek izmantots KYT (Know Your Transaction) process.

ckBTC viedais līgums atbilst TLA+

Iepriekš parādītais augsta līmeņa attēls patiesībā slēpj smalku vienlaicības problēmu, un labā ziņa ir tā, ka mēs varam atklāt problēmu, izmantojot TLA+ rīku komplektu.

Bet, lai TLA+ varētu kaut ko atklāt, mums vispirms ir jānodrošina divas lietas:

  • Izveidojiet mūsu sistēmas modeli, izmantojot TLA+ valodu

  • Norādiet TLA+ rekvizītus, kurus mēs sagaidām, ka sistēma ieviesīs

Šis modelis ir vienkāršota, bet joprojām pilnībā definēta sistēmas versija, kas mūsu gadījumā ietver kaltuves viedo līgumu, kā arī visas citas attiecīgās sistēmas daļas, proti, virsgrāmatas līgumu un Bitcoin tīklu.

Katram komponentam mēs modelējam tā stāvokli un to, kā attiecīgās darbības, ko varētu veikt gala lietotājs (t.i., pārsūtīt BTC vai ckBTC, noguldīt BTC vai izsaukt dažādas kaltētāja atklātās darbības), maina stāvokli.

Visi šie elementi modelī ir nedaudz vienkāršoti, un daļas, uz kurām koncentrējas analīze (piemēram, naudas kaltuves kods), tiek modelētas detalizētāk, savukārt citas daļas (piemēram, Bitcoin tīkls) ir modelētas mazāk detalizēti, patiesībā TLA+ modelis. ir līdzīgs detalizētai sistēmas konstrukcijas specifikācijai.

Intuitīvi galvenā funkcija, ko vēlamies ieviest, ir nodrošināt, lai mūsu ckBTC tiktu pilnībā atbalstīts. Citiem vārdiem sakot, nevienam galalietotājam nevajadzētu būt iespējai “dubultot iztērēt” savu noguldīto BTC, lai iegūtu vairāk ckBTC, nekā viņš noguldīja.

Bet, lai analizētu šādu īpašību, mums šī intuīcija ir ļoti precīza, formāli izsakot to TLA+ valodā. Mūsu formālā definīcija ir tāda, ka kopējais ckBTC piedāvājums (t.i., visu galalietotāja ckBTC atlikumu summa, ko glabā ckBTC virsgrāmata) nepārsniedz kopējo BTC daudzumu, ko kontrolē kalšanas konteiners (t.i., visu vērtību). UTXO, kas pieder depozīta adresei).

Atklājiet un atrisiniet problēmas

Kad esam izveidojuši modeli un rekvizītus, TLA+ rīku komplekts var analizēt modeli. Piemēram, mūsu ckBTC iestatījumos ir iekļauti tikai divi dažādi galalietotāji un neliela daļa no kopējā Bitcoin piedāvājuma (piemēram, 5 satoshi).

Lai gan šis iestatījums ir ļoti ierobežots, empīriskie pētījumi liecina, ka lielākā daļa problēmu datorsistēmās ir atrodamas nelielā skaitā entītiju. Nelielā iestatīšana ļauj analīzē sistemātiski izpētīt visas iespējamās modelī definētās darbību secības un pārbaudīt, vai noteiktās īpašības atbilst jebkurai šādai secībai.

Turklāt analīze tiek veikta pilnībā automātiski, t.i., tai nav nepieciešama cilvēka ievade, un, ja šīs īpašības nav spēkā, tā sniedz mums precīzu darbību secību, kas pārkāpj šo īpašību.

Piemēram, analīze var atklāt, ka mēs varam pārkāpt mūsu rekvizītu "nav nenodrošināta ckBTC" tādā gadījumā, kā parādīts tālāk.

šeit:

  • Galalietotāji iemaksā BTC, tāpat kā iepriekš;

  • Tomēr tagad galalietotājs pēc tam uzdod ckBTC kaltuvei divreiz ātri pēc kārtas atjaunināt atlikumu, un interneta datorā šos atjauninājumus var vienlaikus mijiedarboties ar citiem viedajiem līgumiem;

  • Divi atjauninājumi, kas darbojas vienlaikus, lūdz Bitcoin tīklam visus UTXO, ko deponējis gala lietotājs, un abi saņem atbildi to pašu UTXO, kas tika deponēts 1. darbībā. Tā kā UTXO vēl nav "apstrādāto" sarakstā, abi atjauninājumi Domāju, ka UTXO ir jauns;

  • Abi atjauninājumi norāda virsgrāmatai 4. darbībā izveidot atbilstošu ckBTC daudzumu.

Tāpēc 4. darbības beigās mēs esam stāvoklī, kurā ckBTC piedāvājums ir divreiz lielāks par UTXO summu depozīta adresēs, kas pārkāpj mūsu rekvizītu “nav neatbalstīta ckBTC”.

Ņemiet vērā, ka šī kļūda rodas tikai tāpēc, ka galalietotāja bilances atjauninājumi tiek izpildīti vienlaikus — tā faktiski ir atkārtota ievadīšanas kļūda tādā pašā stilā kā tā, kas nolaida DAO.

Viens veids, kā atrisināt šo problēmu, ir novērst bilances atjauninājumu paralēlu palaišanu vienam un tam pašam gala lietotājam. Mēs to varam izdarīt, liekot naudas kaltuvei galalietotāju saglabāt "bloķēto" lietotāju sarakstā, kad sākas bilances atjaunināšana, un paturēt tos tur. uz atjauninājumu saraksta laiku, lai to panāktu.

Ja galalietotājs mēģina uzsākt citu vienlaicīgu bilances atjauninājumu, atjauninājums vispirms pārbaudīs un atradīs šo konkrēto galalietotāju bloķēto lietotāju sarakstā un pēc tam pārtrauks.

Ņemiet vērā, ka mēs šeit nedaudz vienkāršojam uzbrukumu: bloķēšana patiesībā ir diezgan izplatīta IC viedo līgumu shēma, un ckBTC kaltuves to ir izvietojušas jau no paša sākuma. Tomēr nepareizi izpildīta bloķēšana paver durvis iepriekš minētajiem uzbrukumiem, kurus TLA+ spēj atklāt.

Turklāt mēs atklājām dažus malas gadījumus, kuros tika pārkāpts "nav neatbalstīta ckBTC" un citi svarīgi rekvizīti, un pēc visu labojumu piemērošanas TLA+ varēja pārbaudīt un apstiprināt, ka mūsu definētajā iestatījumā vairs nav nekādu īpašumu pārkāpumu.

Vai viedajiem līgumiem vajadzētu izmantot TLA+?

Pilnīgi noteikti! Labi, labi, varbūt man vajadzētu sniegt niansētāku atbildi, ko mūsu pētniecības un izstrādes komanda izmanto kritiskiem viedajiem līgumiem interneta datoros ikreiz, kad ir iesaistīta nenozīmīga vienlaicība.

Piemēram, TLA+ analīze atklāja smalkas vienlaicīguma kļūdas interneta datoru pārvaldībā un virsgrāmatas konteineros, kas tika izlaistas iepriekšējos manuālajos drošības pārskatos un varēja izraisīt nozīmīgas problēmas, gadījumus un punktus — TLA+ bija noderīgs šādu sarežģītu problēmu atklāšanā. Absolūts sprādziens.

Protams, ir jāmaksā par zinātības iegūšanu un pēc tam modeļa izveidi, taču empīriski cena ir saprātīga, jo īpaši ņemot vērā blokķēdes drošības augstās likmes.

Nevajadzētu nobiedēt no pašas TLA+ valodas, neskatoties uz biedējošo nosaukumu, piekļuve tās spēcīgajām funkcijām ir diezgan vienkārša. Faktiski TLA+ apkrāptu lapa, kurā aprakstītas gandrīz visas TLA+ funkcijas, varētu aptuveni ietilpt lapā:

  • mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html

Turklāt modeļa izveidei nepieciešamās pūles ir salīdzināmas ar standarta manuālajām drošības pārbaudēm. Piemēram, ckBTC kaltuvei kopumā būtu nepieciešamas aptuveni 3 nedēļas, lai 1 persona saprastu dizainu, izveidotu sākotnējo modeli un īpašības.

Iegūtais TLA+ modelis ir daudz vienkāršāks par ieviešanu gan tāpēc, ka tas ir vienkāršāks par kodu, gan TLA+ augsta līmeņa rakstura dēļ. ckBTC kaltuves modelim ir nepieciešamas aptuveni 250 koda rindiņas, salīdzinot ar Rust ieviešanas tūkstošiem rindu. Iespējams, pārsteidzoši, ka viena no grūtākajām daļām pūļu ziņā ir nepieciešamo īpašību precizēšana, jo bieži vien tiek atrastas nepilnības intuitīvajās specifikācijās.

Kad modelis ir pabeigts, analīze (modeļa pārbaude) tiek pabeigta automātiski. Analīzes izpilde var aizņemt ilgu laiku – piemēram, ckBTC veikšanai bija nepieciešamas vairāk nekā 20 stundas. Visbeidzot, vēl viens TLA ieguvums ir tāds, ka modelēšanu un analīzi var veikt projektēšanas fāzē pirms koda ieviešanas, kas palīdz novērst lielus pārveidojumus, kas vēlāk radušies projektēšanas kļūdu dēļ.

Kur TLA+ ir bezjēdzīgs

Negatīvi ir tas, ka TLA+ ir mazāk noderīgs sarežģītām secīgām programmām, atšķirībā no vienlaicīgām programmām, un tas arī nav piemērots sarežģītu kriptogrāfijas protokolu apstrādei, kuriem ir citi rīki (piemēram, Tamarin), kas ir noderīgāki.

Visbeidzot, pastāv jautājums par TLA+ modeļa un faktiskās ieviešanas sinhronizēšanu, jo ieviešanas kods laika gaitā attīstās, tas var vairs neatbilst modelim, ko var būt grūti uztvert bez instrumentu atbalsta.

Patiesībā mūsu pētniecības un attīstības komanda cenšas atrisināt šo problēmu — ceru, ka drīz varēsim ar jums dalīties ar dažiem rīkiem!

Es ceru, ka šis pārskats ir izraisījis jūsu interesi par TLA+ izmantošanu saviem svarīgajiem viedajiem līgumiem, un, ja tā, sekojiet līdzi informācijai — drīzumā tiks publicēta papildu ziņa ar padziļinātu apmācību par TLA+ izmantošanu viedajiem līgumiem. un Attached ir faktiskais TLA+ modelis, ko izstrādājusi mūsu pētniecības un attīstības komanda.

IC saturs, kas jums rūp

Tehnoloģiju attīstība |. Informācija par projektu |

Apkopojiet un sekojiet IC Binance kanālam

Esiet informēts par jaunāko informāciju