Auditarea contractelor inteligente: reentrancy, invarianți și verificări formale

Un contract inteligent este software cu modul de eșec al unui seif de bancă ale cărui planuri sunt publice. Codul este imuabil odată desfășurat, soldurile pe care le păzește sunt reale, iar fiecare atacator de pe pământ îl poate citi pe îndelete și poate lovi la orice oră. Auditarea unuia seamănă mai puțin cu revizuirea unui serviciu web și mai mult cu verificarea unei parașute: nu există a doua încercare.

Reentrancy: clasicul care încă se livrează

Cel mai vechi bug serios din domeniu este în continuare cel mai frecvent. Un contract care trimite fonduri înainte de a-și actualiza propria stare cedează controlul destinatarului la mijlocul tranzacției, iar un destinatar rău intenționat poate apela înapoi în aceeași funcție înainte ca primul apel să se termine — retrăgând iar și iar dintr-un sold care nu a fost încă decrementat. Remedierea este veche și de încredere: respectă ordinea verificări-efecte-interacțiuni, modificând toată starea internă înainte de a face orice apel extern, și adaugă o gardă de reentrancy pentru orice atinge valoare. Într-un audit căutăm fiecare apel extern și urmărim ce stare este încă învechită atunci când controlul părăsește contractul.

Invarianții de stare sunt adevărata ta specificație

Funcțiile sunt ușor de raționat una câte una și perfide în combinație. Ceea ce protejează cu adevărat un protocol sunt invarianții săi — proprietățile care trebuie să fie valabile indiferent de secvența de apeluri pe care o face cineva. Suma soldurilor utilizatorilor egalează deținerile de tokeni ale contractului. Numărul total de acțiuni nu depășește niciodată activele totale. Niciun cont nu poate retrage mai mult decât a depus. Îi scriem explicit, pentru că o funcție care pare corectă izolat nu valorează nimic dacă vreo altă cale lasă un utilizator să încalce invariantul de care depinde întregul sistem.

Testele arată că un contract funcționează pe intrările pe care ți le-ai imaginat. Invarianții și demonstrațiile constrâng intrările pe care nu ți le-ai imaginat.

— Protocore · Inginerie blockchain

Demonstrează ceea ce testele pot doar eșantiona

Testele unitare verifică cazurile la care te-ai gândit, ceea ce este exact acoperirea greșită pentru cod advers. Așa că adăugăm două tehnici care explorează cazurile la care nu te-ai gândit. Fuzzing-ul aruncă milioane de secvențe de apeluri randomizate asupra contractului și verifică dacă invarianții supraviețuiesc fiecăreia. Verificarea formală merge mai departe, demonstrând matematic că o proprietate este valabilă pentru toate intrările posibile, în loc să le eșantioneze — costisitoare, lentă și care merită pentru acea mână de invarianți a căror încălcare golește trezoreria. Între cele două, scopul este același: să transformi „nu am reușit să-l spargem” în „nu poate fi spart în acest mod anume”.

Un audit nu este o ștampilă; este un argument documentat că un contract face ceea ce pretinde și nimic altceva. Livrăm invarianții pe care i-am verificat, demonstrațiile și campaniile de fuzzing din spatele lor și o hartă onestă a riscului rezidual — presupunerile despre oracole, guvernanță și posibilitatea de actualizare pe care nicio cantitate de revizuire Solidity nu le poate elimina. Codul imuabil răsplătește paranoia. Momentul potrivit pentru a găsi bug-ul este cât timp încă poți redesfășura, nu după ce fondurile au dispărut și tranzacția este finală.