Testare simbolică cu Halmos: Utilizarea testelor existente pentru verificarea formală

Verificarea formală – procesul de utilizare a metodelor matematice pentru a „inspecta” un program sau un contract inteligent în orice număr de intrări – este în general văzută ca alternativă mai concisă și mai cuprinzătoare la testarea tradițională pentru scrierea unui cod de calitate superioară și mai sigur. Dar, în realitate, verificarea formală este un proces deschis și interactiv. La fel ca și testarea unitară, dezvoltatorii trebuie să definească dinamic și să suprapună specificațiile formale, repetând abordarea lor pe măsură ce codul și analizele lor evoluează. În plus, verificarea formală este la fel de eficientă ca și specificațiile sale, care poate fi consumatoare de timp pentru a scrie (și adesea vine cu o curbă de învățare abruptă). 

Pentru mulți dezvoltatori care consideră că procesul este descurajator, testele unitare sunt adesea calea mai eficientă din punct de vedere al costurilor și mai eficientă în timp pentru a susține corectitudinea unui program. În practică, verificarea formală nu este o alternativă mai cuprinzătoare la testarea unitară, ci una complementară. Aceste procese au puncte forte și limitări diferite, oferind o siguranță și mai mare atunci când sunt utilizate împreună. Dezvoltatorii vor trebui întotdeauna să scrie teste unitare – deci ce se întâmplă dacă am putea folosi aceleași proprietăți pentru verificarea formală?

Halmos, instrumentul nostru de verificare formală open source, le permite dezvoltatorilor reutilizarea aceleași proprietăți scrise pentru testele unitare pentru specificații formale prin testare simbolică. În loc să fie nevoiți să creeze un set robust de proprietăți de la început, dezvoltatorii pot evita munca duplicat și își pot îmbunătăți testele câteva specificații la un moment dat, fără a începe de la zero. Am conceput acest instrument pentru a fi utilizat, alături de altele în procesul de verificare formală, ca o rampă de acces către verificarea formală; dezvoltatorii pot începe cu câteva analize cu un efort minim, înainte de a adăuga mai multe mai târziu în proces.

În această postare, acoperim provocările verificării formale și potențialul de a reduce decalajul dintre testarea unitară și verificarea formală cu testarea simbolică. Apoi parcurgem o demonstrație a Halmos folosind codul de contract inteligent existent și aruncăm o privire rapidă asupra altor instrumente de verificare formale (multe open source) disponibile dezvoltatorilor.

Verificare formală vs testare

Verificare formala — în general favorizat de dezvoltatorii blockchain pentru rigoarea și comprehensiunea sa — este procesul de demonstrare a corectitudinii unui program prin verificarea faptului că acesta satisface anumite proprietăți de corectitudine. Proprietățile, care sunt specifice programului, sunt de obicei furnizate extern și exprimate folosind un limbaj formal sau o notație care este susținută de instrumentul de verificare utilizat. Dezvoltatorii percep deseori verificarea formală ca pe o soluție prin apăsare pentru testarea proprietăților în toate scenariile posibile în mod automat, dar, în realitate, verificarea formală poate fi un proces intens de muncă și foarte interactiv.

La fel ca verificarea formală, testarea unitară implică evaluarea dacă un program funcționează conform așteptărilor; testarea, totuși, verifică doar comportamentul programului pentru unele intrări, în timp ce verificarea formală o poate verifica toate posibile intrări. Atât testarea, cât și verificarea formală necesită o descriere a comportamentului așteptat al programului (cu cazuri de testare utilizate în testare și specificații formale utilizate în verificarea formală). Dar, atunci când sunt utilizate împreună, acestea pot oferi o examinare mai aprofundată a unui program. Testarea, de exemplu, este eficientă în găsirea unor erori și greșeli simple, dar este în general mai rapid și mai ușor de efectuat. Verificarea formală, deși este mai greoaie de utilizat, este suficient de puternică pentru a dovedi absența erorilor sau pentru a dezvălui erori subtile care sunt ușor de ratat în teste sau revizuiri de cod.

Caietul de sarcini general

Una dintre principalele provocări ale verificării formale este suprasolicitarea redactării și menținerii specificațiilor formale. Acest proces implică adesea sarcina consumatoare de timp de a scrie manual specificațiile folosind un limbaj specializat (pe care mulți dezvoltatori vor trebui să-l învețe mai întâi). Procesul este, de asemenea, incremental, începând de obicei cu scrierea proprietăților simple și verificarea lor mai întâi, apoi adăugând treptat proprietăți mai complexe deasupra. La fel ca testarea, este un proces deschis, fără un punct de oprire clar și se pot adăuga doar cât mai multe proprietăți posibil în intervalul de timp disponibil. În plus, atunci când dezvoltatorii modifică codul pe măsură ce acesta este verificat, trebuie să-și actualizeze specificațiile existente, ceea ce duce la eforturi suplimentare de întreținere. Acești factori pot face din verificarea formală o sarcină descurajantă pentru unii dezvoltatori care ezită să se angajeze în cheltuielile suplimentare.

Și, deși testarea și verificarea formală pot îmbunătăți calitatea codului atunci când sunt utilizate împreună, ambele necesită descrieri (uneori similare) ale comportamentului așteptat al unui program în diferite limbi și formate. Scrierea și menținerea acestor descrieri necesită multă muncă, iar menținerea a două forme diferite ale aceleiași descrieri poate fi considerată ca un efort duplicat. Aceasta ridică următoarea întrebare: Este posibil să descriem comportamentul așteptat într-un mod pe care dezvoltatorii îl pot folosi atât pentru testare, cât și pentru verificare?

Reducerea decalajului dintre testare și verificarea formală cu testarea simbolică și Halmos

Testarea simbolică, practica de a rula teste cu intrări simbolice, este o metodă eficientă de verificare formală care reduce costul general al specificațiilor. Această abordare permite utilizarea acelorași cazuri de testare atât pentru testare, cât și pentru verificarea formală. Spre deosebire de testarea tradițională, care verifică dacă un program funcționează corect pentru un set limitat de intrări, testarea simbolică verifică programul pentru toate intrările posibile, prin urmare un program care trece testarea simbolică poate fi considerat verificat formal.

Halmos este un instrument formal de verificare conceput pentru testarea simbolică. În loc să solicite specificații separate sau să învețe o nouă limbă, Halmos folosește testele existente ca specificații formale. Executarea testelor prin Halmos va verifica automat că au trecut pentru toate intrările posibile sau va oferi contraexemple. Acest lucru nu numai că elimină necesitatea scrierii suplimentare a specificațiilor, dar permite și reutilizarea testelor scrise pentru testarea unitară sau fuzzing, în scopuri de verificare formală.

Dezvoltatorii au astfel o flexibilitate mai mare de a alege dintr-o gamă de opțiuni de asigurare a calității, inclusiv testarea unitară, fuzzing și verificarea formală, în funcție de nevoile lor curente. De exemplu, testele pot identifica rapid greșelile simple, eventual cu ajutorul unui fuzzer care generează intrări aleatorii, iar apoi Halmos poate crește și mai mult încrederea în corectitudinea programului în toate intrările.

Exemplu: testarea isPowerOfTwo() funcţie

Ca exemplu, luați în considerare următoarele isPowerOfTwo() funcție, care determină dacă un număr dat este o putere a lui doi. Această funcție folosește a algoritm de manipulare a biților pentru eficiență, dar poate fi dificil să-i demonstrezi corectitudinea, mai ales în cazul în care intrarea nu este o putere de doi.

Imaginați-vă următorul test pentru isPowerOfTwo() funcția: compară ieșirea reală a funcției cu ieșirea așteptată pentru o intrare dată. Acesta este un test parametrizat (cunoscut și ca test bazat pe proprietăți), ceea ce înseamnă că îl puteți rula cu ușurință cu diferite valori de intrare, eventual cu instrumente de fuzzing precum Foundry.

Puteți utiliza acest test pentru a examina isPowerOfTwo() funcția prin testarea unitară sau testarea fuzz, rulând-o cu o selecție de intrări. Teste ca acestea nu pot dovedi în mod oficial corectitudinea funcției, deoarece este imposibil din punct de vedere computațional să rulați testul pentru fiecare intrare posibilă.

Halmos, totuși, permite dezvoltatorilor să refolosească aceste teste preexistente pentru verificarea formală cu doar un mic efort suplimentar. Instrumentul verifică dacă testele au trecut pentru toate intrările posibile, efectuând execuția simbolică a testului și apoi verificând că afirmația nu este niciodată încălcată (sau, dacă afirmația is a încălcat, oferind un contraexemplu). Aceasta înseamnă că dacă testul trece Halmos, corectitudinea funcției este verificată formal, ceea ce înseamnă că algoritmul este implementat corect și a fost tradus cu precizie de compilator în bytecode.

Limitare: Execuție simbolică delimitată

În general, nu este posibil să se efectueze o testare simbolică complet automată, deoarece aceasta ar necesita rezolvarea problema de oprire, care se știe a fi indecidabil. Un motiv pentru aceasta este că este adesea imposibil să se determine automat de câte ori trebuie să se repete simbolic o buclă. Ca urmare, verificarea formală complet automată este în general indecidabilă.

Având în vedere aceste limitări fundamentale, Halmos acordă prioritate automatizării în detrimentul completității. În acest scop, Halmos este proiectat pentru a efectua raționament simbolic mărginit pentru bucle nemărginite (unde numărul de iterații depinde de intrările programului) sau matrice de lungime variabilă (inclusiv șiruri). Acest lucru sacrifică o anumită completitudine, dar îi permite lui Halmos să evite solicitarea utilizatorului de a furniza adnotări suplimentare, cum ar fi invarianții de buclă.

De exemplu, luați în considerare următoarea versiune iterativă a isPowerOfTwo() funcția, care prezintă o buclă while nemărginită, unde numărul de iterații ale buclei este determinat de numărul minim de biți necesar pentru a reprezenta numărul de intrare.

Halmos repetă simbolic această buclă nemărginită numai până la o limită specificată. De exemplu, dacă limita este setată la 3, Halmos va repeta bucla de cel mult 3 ori și nu va lua în considerare valorile de intrare care ar face ca bucla să se repete de mai mult de 3 ori (adică, orice valoare mai mare sau egală cu 2^3 ). În acest caz particular, setarea limitei la 256 sau mai mare ar permite lui Halmos să fie complet.

Demo: verificare formală a ERC721A cu Halmos

Pentru a demonstra capacitățile lui Halmos, l-am folosit pentru a testa simbolic și a verifica formal ERC721A, o implementare extrem de optimizată pentru gaz a standardului ERC721 care permite baterea în loturi la aproape același cost ca o singură batere. ERC721A include mai multe inovatoare optimizări pentru a atinge această eficiență; de exemplu, gazul poate fi salvat prin întârzierea actualizărilor datelor de proprietate asupra jetonului până când acesta este transferat, nu în momentul baterii. Acest lucru necesită utilizarea unor structuri de date complexe și algoritmi pentru a prelua eficient informațiile de proprietate din structura de date leneșă. Și, deși această optimizare îmbunătățește eficiența gazului, crește și complexitatea codului și face dificilă demonstrarea corectitudinii implementării. Acest lucru face ca ERC721A să fie un bun candidat pentru verificarea formală, deoarece poate crește încrederea în implementare și poate aduce beneficii utilizatorilor potențiali.

Proprietăți de testare simbolică

Deoarece testele existente pentru ERC721A au fost scrise în JavaScript cu Hardhat (care nu este suportat în prezent de Halmos), am scris noi teste în Solidity pentru funcțiile principale de intrare: mint(), burn(), și transfer(). Aceste teste au verificat dacă fiecare funcție actualizează corect proprietatea și soldul token-ului și afectează numai utilizatorii relevanți, fără a modifica echilibrul sau proprietatea altor utilizatori. Acesta din urmă este netrivial de demonstrat datorită utilizării algoritmului de structură de date leneș în ERC721A. De exemplu, următorul test verifică dacă transfer() funcția actualizează corect proprietatea jetonului specificat:

Un alt test verifică dacă transfer() funcția nu modifică echilibrul pentru alte adrese, ceea ce este dificil de demonstrat așa cum am menționat mai devreme:

Rezultatele verificării

Am efectuat un experiment de verificare folosind Halmos pe contractul inteligent ERC721A scriind un total de Testele 19. Testele au fost efectuate prin Halmos cu o legătură de derulare a buclei de 3, care a durat 16 minute. Defalcarea timpului de verificare poate fi văzută în tabelul de mai jos. Experimentul a fost efectuat pe un MacBook Pro cu un cip M1 Pro și 16 GB de memorie.

Test	Ora (ore)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdNeschimbat	1.40
testBurnOtherBalancePreservation	5.69
testBurnOtherOwnershipPreservation	189.70
testBurnOwnershipUpdate	3.81
testBurnRequirements	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintOtherOwnershipPreservation	5.74
testMintOwnershipUpdate	1.38
testMintRequirements	0.09
testTransferBalanceNeschimbat	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdNeschimbat	4.47
testTransferOtherBalancePreservation	19.57
testTransferOtherOwnershipPreservation	430.61
testTransferOwnershipUpdate	18.71
testTransferRequirements	149.18

În timp ce majoritatea testelor au fost finalizate în câteva secunde, câteva dintre ele au durat câteva minute. Aceste teste consumatoare de timp au fost dificil de verificat din cauza naturii complexe a cazurilor care trebuiau luate în considerare și au fost strâns legate de corectitudinea algoritmului de structură a datelor leneș.

În general, rezultatele acestui experiment indică faptul că Halmos este capabil să verifice în mod eficient corectitudinea codului de contract inteligent. Oferă o încredere sporită în integritatea codului, în ciuda complexității și a potențialelor cazuri marginale ale contractului inteligent.

Experimentați cu bug-uri injectate

Pentru a demonstra eficiența raționamentului limitat al lui Halmos, l-am folosit pentru a detecta erori într-o versiune anterioară a contractului ERC721A. Această versiune a avut o problemă care a gestionat greșit depășirea aritmetică și a permis potențial batch-area unui număr mare de jetoane, ceea ce ar putea distruge integritatea structurii de date leneșe și ar putea duce la pierderea dreptului de proprietate al token-ului pentru unii utilizatori (o problemă hotărât în versiunea actuală). Am rulat același set de 19 teste pentru ERC721A pe versiunea buggy, iar Halmos a reușit să găsească un contraexemplu pentru proprietățile mint() funcţie. Mai exact, Halmos a furnizat valori de intrare care au condus la scenariul de exploatare descris mai sus. Rezultatele acestui experiment indică faptul că, în ciuda caracterului incomplet, raționamentul limitat al lui Halmos poate fi o modalitate eficientă de detectare și prevenire a erorilor exploatabile în contractele inteligente.

Lucrări conexe

Instrumente formale de verificare pentru codul octet al contractului inteligent Ethereum au fost dezvoltate de diverse echipe. Aceste instrumente, inclusiv Halmos, pot fi folosite pentru a asigura securitatea și corectitudinea contractelor inteligente. Compararea și înțelegerea diferitelor caracteristici, capacități și limitări ale acestor instrumente poate ajuta dezvoltatorii să aleagă pe cel mai potrivit pentru nevoile lor unice.

Deși Halmos este un plus valoros la setul de instrumente disponibil pentru verificarea inteligentă a contractelor, este menit să completeze (nu să înlocuiască) instrumentele existente. Dezvoltatorii pot combina Halmos cu alte instrumente pentru a obține un nivel mai ridicat de asigurare în contractele lor. Mai jos, comparăm Halmos cu câteva instrumente formale selectate care acceptă bytecode EVM.

• K este un cadru puternic de verificare formală care permite verificarea deductivă și demonstrarea interactivă a teoremei. Teoria și implementarea sa de bază oferă un nivel ridicat de expresivitate, făcându-l potrivit pentru verificarea programelor și algoritmilor complexe. Cu toate acestea, trebuie remarcat faptul că K nu este proiectat cu accent mare pe verificarea automată și nu are anumite caracteristici de automatizare care pot necesita mai mult efort manual în timpul procesului de verificare. Pentru a utiliza cadrul K, specificațiile formale sunt scrise în limbajul K, care trebuie învățat înainte de utilizare. Puterea sa este deosebit de utilă în verificarea sistemelor complexe, care pot fi dificil de analizat folosind raționamentul automat.
• Certora este un instrument formal de verificare pentru contractele inteligente care se concentrează pe verificarea automată și acceptă verificarea modelului limitat, similar cu Halmos. Pentru a folosi Certora, dezvoltatorii trebuie să învețe noua lor limbă, CVL, pentru a scrie specificații. Acest limbaj permite descrierea concisă a multor proprietăți critice prin invariante de contract, o caracteristică pe care Halmos nu o acceptă în prezent. În ciuda faptului că este un instrument proprietar cu sursă închisă, Certora oferă instrumente solide de verificare formală, cu dezvoltare continuă și asistență bună pentru utilizatori.
  
  Halmos, pe de altă parte, este un instrument open-source care are o scară mai mică și nu are în prezent unele caracteristici oferite de Certora, dar este menit să servească drept bun public și este conceput ca o soluție de nișă pentru verificarea rapidă a contractelor inteligente fără necesitatea unei instalări și întreținere extinse.
• HEVM este un alt instrument formal de verificare care este similar cu Halmos. Anterior a făcut parte din DappTools, care este un precursor al Foundry. Atât HEVM, cât și Halmos au caracteristica de a nu necesita o specificație separată și pot executa simbolic teste existente pentru a identifica încălcările afirmațiilor. Acest lucru permite utilizatorilor să folosească ambele instrumente în mod interschimbabil sau să le ruleze în paralel pentru aceleași teste, oferindu-le mai multe opțiuni pentru testarea simbolică.
  
  Este de remarcat faptul că, în ciuda asemănărilor lor, HEVM și Halmos au fost dezvoltate independent și diferă în detaliile de implementare; în special în ceea ce priveşte optimizările şi strategiile de raţionament simbolic. În plus, HEVM este scris în Haskell, în timp ce Halmos este scris în Python, oferind expunere la ecosistemul bogat Python. Abilitatea de a utiliza ambele instrumente oferă utilizatorilor mai multă flexibilitate și opțiuni pentru a asigura securitatea și corectitudinea contractelor inteligente.

Halmos este open source și în prezent se află în faza sa beta. Lucrăm activ la noi caracteristici și funcționalitate, inclusiv coduri de înșelăciune Foundry și alte câteva caracteristici cheie de utilizare. Am aprecia foarte mult părerile dvs. cu privire la caracteristicile cele mai importante și am binevenit orice feedback, sugestii și contribuții pentru a face din Halmos un instrument mai bun pentru toată lumea.

**

Părerile exprimate aici sunt cele ale personalului individual AH Capital Management, LLC („a16z”) citat și nu sunt punctele de vedere ale a16z sau ale afiliaților săi. Anumite informații conținute aici au fost obținute din surse terțe, inclusiv de la companii de portofoliu de fonduri administrate de a16z. Deși este luat din surse considerate a fi de încredere, a16z nu a verificat în mod independent astfel de informații și nu face nicio declarație cu privire la acuratețea actuală sau de durată a informațiilor sau adecvarea acestora pentru o situație dată. În plus, acest conținut poate include reclame de la terți; a16z nu a revizuit astfel de reclame și nu aprobă niciun conținut publicitar conținut în acestea.

Acest conținut este furnizat doar în scop informativ și nu ar trebui să fie bazat pe consiliere juridică, de afaceri, de investiții sau fiscală. Ar trebui să vă consultați propriii consilieri cu privire la aceste aspecte. Referințele la orice titluri de valoare sau active digitale au doar scop ilustrativ și nu constituie o recomandare de investiții sau o ofertă de a oferi servicii de consiliere în materie de investiții. În plus, acest conținut nu este îndreptat și nici nu este destinat utilizării de către niciun investitor sau potențial investitor și nu poate fi bazat în nicio circumstanță atunci când se ia o decizie de a investi într-un fond administrat de a16z. (Ofertă de a investi într-un fond a16z va fi făcută numai prin memoriul de plasament privat, acordul de subscriere și alte documente relevante ale oricărui astfel de fond și trebuie citită în întregime.) Orice investiții sau companii de portofoliu menționate, la care se face referire sau descrise nu sunt reprezentative pentru toate investițiile în vehicule administrate de a16z și nu poate exista nicio asigurare că investițiile vor fi profitabile sau că alte investiții realizate în viitor vor avea caracteristici sau rezultate similare. O listă a investițiilor realizate de fondurile gestionate de Andreessen Horowitz (excluzând investițiile pentru care emitentul nu a oferit permisiunea ca a16z să dezvăluie public, precum și investițiile neanunțate în active digitale tranzacționate public) este disponibilă la https://a16z.com/investments /.

Diagramele și graficele furnizate în cadrul sunt doar în scop informativ și nu trebuie să se bazeze pe acestea atunci când se ia vreo decizie de investiție. Performanța trecută nu indică rezultatele viitoare. Conținutul vorbește doar de la data indicată. Orice previziuni, estimări, prognoze, obiective, perspective și/sau opinii exprimate în aceste materiale pot fi modificate fără notificare și pot diferi sau pot fi contrare opiniilor exprimate de alții. Vă rugăm să consultați https://a16z.com/disclosures pentru informații suplimentare importante.