Test simbolici con Halmos: sfruttare i test esistenti per la verifica formale

La verifica formale - il processo di utilizzo di metodi matematici per "ispezionare" un programma o un contratto intelligente attraverso un numero qualsiasi di input - è generalmente vista come l'alternativa più concisa e completa ai test tradizionali per scrivere codice di qualità superiore e più sicuro. Ma in realtà, la verifica formale è un processo aperto e interattivo. Proprio come i test unitari, gli sviluppatori devono definire dinamicamente e stratificare le specifiche formali, ripetendo il loro approccio man mano che il codice e le analisi si evolvono. Inoltre, la verifica formale è efficace solo quanto le sue specifiche, che possono richiedere molto tempo per essere scritte (e spesso comportano una ripida curva di apprendimento). 

Per molti sviluppatori che trovano il processo scoraggiante, i test unitari sono spesso il percorso più conveniente ed efficiente in termini di tempo per verificare la correttezza di un programma. In pratica, la verifica formale non è un'alternativa più completa ai test unitari, ma complementare. Questi processi hanno diversi punti di forza e limitazioni, fornendo una sicurezza ancora maggiore se usati insieme. Gli sviluppatori dovranno sempre scrivere test unitari, quindi se potessimo utilizzare le stesse proprietà per la verifica formale?

Halmos, il nostro strumento di verifica formale open source, consente agli sviluppatori di riutilizzare le stesse proprietà scritte per unit test per specifiche formali attraverso test simbolici. Anziché dover creare un solido set di proprietà dall'inizio, gli sviluppatori possono evitare lavori duplicati e migliorare i test di alcune specifiche alla volta senza ripartire da zero. Abbiamo progettato questo strumento per l'uso, insieme ad altri nel processo di verifica formale, come rampa verso la verifica formale; gli sviluppatori possono iniziare con poche analisi con il minimo sforzo, prima di aggiungerne altre più avanti nel processo.

In questo post, trattiamo le sfide della verifica formale e il potenziale per colmare il divario tra unit test e verifica formale con test simbolici. Esaminiamo quindi una demo di Halmos utilizzando il codice del contratto intelligente esistente e diamo una rapida occhiata ad altri strumenti di verifica formale (molti open source) disponibili per gli sviluppatori.

Verifica formale vs test

Verifica formale - generalmente favorito dagli sviluppatori blockchain per il suo rigore e completezza - è il processo per dimostrare la correttezza di un programma verificando che soddisfi determinate proprietà di correttezza. Le proprietà, che sono specifiche del programma, sono generalmente fornite esternamente ed espresse utilizzando un linguaggio formale o una notazione supportata dallo strumento di verifica utilizzato. Gli sviluppatori spesso percepiscono la verifica formale come una soluzione immediata per testare automaticamente le proprietà in tutti i possibili scenari, ma in realtà la verifica formale può essere un processo laborioso e altamente interattivo.

Come la verifica formale, il test unitario implica la valutazione se un programma funziona come previsto; testing, tuttavia, controlla solo il comportamento del programma per alcuni input, mentre la verifica formale può verificarne la presenza contro tutti i possibili ingressi. Sia il test che la verifica formale richiedono una descrizione del comportamento previsto del programma (con casi di test utilizzati nei test e specifiche formali utilizzate nella verifica formale). Ma, se usati insieme, possono fornire un esame più approfondito di un programma. I test, ad esempio, sono efficaci nel trovare bug ed errori semplici, ma sono generalmente più veloci e facili da eseguire. La verifica formale, sebbene più complicata da usare, è abbastanza potente da dimostrare l'assenza di errori o rivelare bug sottili che è facile non notare nei test o nelle revisioni del codice.

Specifiche generali

Una delle principali sfide della verifica formale è l'overhead della scrittura e del mantenimento delle specifiche formali. Questo processo comporta spesso l'attività dispendiosa in termini di tempo di scrivere manualmente le specifiche utilizzando un linguaggio specializzato (che molti sviluppatori dovranno prima imparare). Anche il processo è incrementale, in genere inizia con la scrittura di proprietà semplici e la loro verifica prima, per poi aggiungere gradualmente proprietà più complesse. Come il test, è un processo a tempo indeterminato, senza un chiaro punto di arresto, e si possono solo aggiungere quante più proprietà possibili entro il periodo di tempo disponibile. Inoltre, quando gli sviluppatori modificano il codice durante la verifica, devono anche aggiornare le specifiche esistenti, comportando ulteriori sforzi di manutenzione. Questi fattori possono rendere la verifica formale un compito scoraggiante per alcuni sviluppatori che esitano a impegnarsi per il sovraccarico aggiuntivo.

E sebbene il test e la verifica formale possano migliorare la qualità del codice se usati insieme, entrambi richiedono descrizioni (a volte simili) del comportamento previsto di un programma in linguaggi e formati diversi. Scrivere e mantenere queste descrizioni richiede molto lavoro e mantenere due diverse forme della stessa descrizione può sembrare uno sforzo duplicato. Ciò solleva la seguente domanda: è possibile descrivere il comportamento previsto in un modo che gli sviluppatori possano utilizzare sia per il test che per la verifica?

Colmare il divario tra test e verifica formale con test simbolici e Halmos

Il test simbolico, la pratica di eseguire test con input simbolici, è un metodo di verifica formale efficace che riduce il sovraccarico delle specifiche. Questo approccio consente l'utilizzo degli stessi casi di test sia per il test che per la verifica formale. A differenza del test tradizionale, che verifica che un programma funzioni correttamente per un insieme limitato di input, il test simbolico controlla il programma per tutti i possibili input, quindi un programma che supera il test simbolico può essere considerato formalmente verificato.

Halmos è uno strumento di verifica formale progettato per i test simbolici. Invece di richiedere specifiche separate o imparare una nuova lingua, Halmos utilizza i test esistenti come specifiche formali. L'esecuzione di test tramite Halmos verificherà automaticamente che passino per tutti i possibili input o fornirà controesempi. Ciò non solo elimina la necessità di scrivere specifiche aggiuntive, ma consente anche il riutilizzo di test scritti per unit test o fuzzing, a scopo di verifica formale.

Gli sviluppatori hanno quindi una maggiore flessibilità per scegliere tra una gamma di opzioni di garanzia della qualità, inclusi test unitari, fuzzing e verifica formale, a seconda delle loro esigenze attuali. Ad esempio, i test possono identificare rapidamente errori semplici, possibilmente con l'aiuto di un fuzzer che genera input casuali, e quindi Halmos può aumentare ulteriormente la fiducia nella correttezza del programma in tutti gli input.

Esempio: testare il isPowerOfTwo() function

Come esempio, si consideri quanto segue isPowerOfTwo() funzione, che determina se un dato numero è una potenza di due. Questa funzione usa a algoritmo di manipolazione dei bit per l'efficienza, ma può essere difficile dimostrarne la correttezza, in particolare nel caso in cui l'input non sia una potenza di due.

Immagina il seguente test per il isPowerOfTwo() funzione: confronta l'output effettivo della funzione con l'output previsto per un dato input. Questo è un test parametrizzato (noto anche come test basato su proprietà), il che significa che puoi facilmente eseguirlo con diversi valori di input, possibilmente con strumenti di fuzzing come Foundry.

È possibile utilizzare questo test per esaminare il isPowerOfTwo() funzione tramite unit test o fuzz test, eseguendolo con una selezione di input. Test come questi non possono dimostrare formalmente la correttezza della funzione, poiché è computazionalmente impossibile eseguire il test per ogni possibile input.

Halmos, tuttavia, consente agli sviluppatori di riutilizzare questi test preesistenti per la verifica formale con solo un piccolo sforzo in più. Lo strumento verifica che i test vengano superati per tutti i possibili input eseguendo l'esecuzione simbolica del test e quindi verificando che l'asserzione non venga mai violata (oppure, se l'asserzione is violato, fornendo un controesempio). Ciò significa che se il test supera Halmos, la correttezza della funzione viene verificata formalmente, ovvero l'algoritmo è correttamente implementato ed è stato accuratamente tradotto dal compilatore in bytecode.

Limitazione: esecuzione simbolica limitata

In genere non è possibile eseguire test simbolici completamente automatici e completi, poiché ciò richiederebbe la risoluzione del fermare il problema, che è noto per essere indecidibile. Uno dei motivi è che spesso è impossibile determinare automaticamente quante volte un ciclo dovrebbe iterare simbolicamente. Di conseguenza, la verifica formale completamente automatica è generalmente indecidibile.

Date queste limitazioni fondamentali, Halmos dà la priorità all'automazione piuttosto che alla completezza. A tal fine, Halmos è progettato per eseguire ragionamenti simbolici limitati per loop illimitati (in cui il numero di iterazioni dipende dagli input del programma) o array di lunghezza variabile (comprese le stringhe). Ciò sacrifica una certa completezza, ma consente ad Halmos di evitare di richiedere all'utente di fornire annotazioni aggiuntive come invarianti di ciclo.

Ad esempio, si consideri la seguente versione iterativa di isPowerOfTwo() funzione, che presenta un ciclo while illimitato, in cui il numero di iterazioni del ciclo è determinato dal numero minimo di bit richiesti per rappresentare il numero di input.

Halmos itera simbolicamente questo ciclo illimitato solo fino a un limite specificato. Ad esempio, se il limite è impostato su 3, Halmos ripeterà il ciclo al massimo 3 volte e non considererà i valori di input che causerebbero l'iterazione del ciclo più di 3 volte (ovvero, qualsiasi valore maggiore o uguale a 2^3 ). In questo caso particolare, l'impostazione del limite a 256 o superiore consentirebbe a Halmos di essere completo.

Demo: verifica formale di ERC721A con Halmos

Per dimostrare le capacità di Halmos, lo abbiamo usato per testare simbolicamente e verificare formalmente ERC721A, un'implementazione altamente ottimizzata per il gas dello standard ERC721 che consente il conio in lotti quasi allo stesso costo del conio singolo. ERC721A include diversi innovativi ottimizzazioni raggiungere questa efficienza; ad esempio, il gas può essere risparmiato ritardando gli aggiornamenti dei dati di proprietà del token fino a quando il token non viene trasferito, non al momento del conio. Ciò richiede l'uso di strutture dati e algoritmi complessi per recuperare in modo efficiente le informazioni sulla proprietà dalla struttura dati pigra. E sebbene questa ottimizzazione migliori l'efficienza del gas, aumenta anche la complessità del codice e rende difficile dimostrare la correttezza dell'implementazione. Ciò rende ERC721A un buon candidato per la verifica formale, in quanto può aumentare la fiducia nell'implementazione e avvantaggiare i potenziali utenti.

Proprietà test simboliche

Poiché i test esistenti per ERC721A sono stati scritti in JavaScript con Hardhat (che non è attualmente supportato da Halmos), abbiamo scritto nuovi test in Solidity per le principali funzioni del punto di ingresso: mint(), burn()e transfer(). Questi test hanno verificato che ogni funzione aggiorni correttamente la proprietà e il saldo dei token e influisca solo sugli utenti pertinenti senza alterare il saldo o la proprietà di altri utenti. Quest'ultimo non è banale da dimostrare a causa dell'uso dell'algoritmo di struttura dati pigro in ERC721A. Ad esempio, il seguente test controlla che il file transfer() la funzione aggiorna correttamente la proprietà del token specificato:

Un altro test verifica che il file transfer() la funzione non altera l'equilibrio per altri indirizzi, che è difficile da dimostrare come accennato in precedenza:

Risultati della verifica

Abbiamo condotto un esperimento di verifica utilizzando Halmos sul contratto intelligente ERC721A scrivendo un totale di Test 19. I test sono stati eseguiti attraverso Halmos con un limite di srotolamento del ciclo di 3, che ha richiesto 16 minuti per essere completato. La ripartizione del tempo di verifica può essere vista nella tabella sottostante. L'esperimento è stato condotto su un MacBook Pro con chip M1 Pro e 16 GB di memoria.

Test	Tempo / i
testBurnBalanceUpdate	6.67
testBurnNextTokenIdInvariato	1.40
testBurnOtherBalancePreservation	5.69
testBurnAltroProprietàConservazione	189.70
testBurnOwnershipUpdate	3.81
testBurnRequisiti	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintaAltroConservazioneequilibrio	0.26
testMintAltroProprietàConservazione	5.74
testMintOwnershipUpdate	1.38
testMintRequisiti	0.09
testTransferBalanceInvariato	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdInvariato	4.47
testTrasferimentoAltroConservazione del saldo	19.57
testTrasferimentoAltroProprietàConservazione	430.61
testTransferOwnershipUpdate	18.71
testTransferRequirements	149.18

Sebbene la maggior parte dei test sia stata completata in pochi secondi, alcuni di essi hanno richiesto diversi minuti. Questi lunghi test erano difficili da verificare a causa della natura complessa dei casi da considerare ed erano strettamente correlati alla correttezza dell'algoritmo della struttura dei dati pigri.

Nel complesso, i risultati di questo esperimento indicano che Halmos è in grado di verificare efficacemente la correttezza del codice del contratto intelligente. Fornisce una maggiore fiducia nell'integrità del codice, nonostante la complessità e i potenziali casi limite dello smart contract.

Sperimenta con bug iniettati

Per dimostrare l'efficacia del ragionamento limitato di Halmos, lo abbiamo utilizzato per rilevare bug in una versione precedente del contratto ERC721A. Questa versione presentava un problema che gestiva in modo errato l'overflow aritmetico e potenzialmente consentiva il conio in batch di un numero elevato di token, il che poteva compromettere l'integrità della struttura di dati pigri e comportare la perdita della proprietà del token da parte di alcuni utenti (un problema risoluto nella versione attuale). Abbiamo eseguito la stessa serie di 19 test per ERC721A sulla versione con bug e Halmos è stato in grado di trovare un controesempio per le proprietà del mint() funzione. Nello specifico, Halmos ha fornito valori di input che hanno portato allo scenario di exploit sopra descritto. I risultati di questo esperimento indicano che, nonostante la sua incompletezza, il ragionamento limitato di Halmos può essere un modo efficace per rilevare e prevenire bug sfruttabili negli smart contract.

Lavoro correlato

Gli strumenti di verifica formale per il bytecode del contratto intelligente Ethereum sono stati sviluppati da vari team. Questi strumenti, incluso Halmos, possono essere utilizzati per garantire la sicurezza e la correttezza dei contratti intelligenti. Il confronto e la comprensione delle diverse caratteristiche, capacità e limiti di questi strumenti può aiutare gli sviluppatori a scegliere quello più appropriato per le loro esigenze specifiche.

Sebbene Halmos sia una preziosa aggiunta al set di strumenti disponibile per la verifica dei contratti intelligenti, è pensato per integrare (non sostituire) gli strumenti esistenti. Gli sviluppatori possono combinare Halmos con altri strumenti per ottenere un livello più elevato di garanzia nei loro contratti. Di seguito, confrontiamo Halmos con alcuni strumenti formali selezionati che supportano il bytecode EVM.

• K è un potente framework di verifica formale che consente la verifica deduttiva e la dimostrazione interattiva di teoremi. La sua teoria e implementazione sottostanti forniscono un alto livello di espressività, rendendolo adatto alla verifica di programmi e algoritmi complessi. Tuttavia, va notato che K non è progettato con una forte enfasi sulla verifica automatizzata e manca di alcune funzionalità di automazione che possono richiedere uno sforzo manuale maggiore durante il processo di verifica. Per utilizzare il framework K, le specifiche formali sono scritte nel linguaggio K, che deve essere appreso prima dell'uso. La sua forza è particolarmente utile nella verifica di sistemi complessi, che possono essere difficili da analizzare utilizzando il ragionamento automatico.
• Certora è uno strumento di verifica formale per contratti intelligenti che si concentra sulla verifica automatizzata e supporta il controllo del modello limitato, simile a Halmos. Per usare Certora, gli sviluppatori devono imparare la loro nuova lingua, CVL, per scrivere le specifiche. Questo linguaggio consente la descrizione concisa di molte proprietà critiche attraverso invarianti di contratto, una caratteristica che Halmos attualmente non supporta. Nonostante sia uno strumento proprietario a codice chiuso, Certora fornisce solidi strumenti di verifica formale, con uno sviluppo continuo e un buon supporto per gli utenti.
  
  Halmos, d'altra parte, è uno strumento open source di dimensioni più ridotte e attualmente privo di alcune funzionalità fornite da Certora, ma è pensato per fungere da bene pubblico ed è inteso come una soluzione di nicchia per verificare rapidamente gli smart contract senza la necessità di un'ampia installazione e manutenzione.
• HEVM è un altro strumento di verifica formale simile a Halmos. In precedenza faceva parte di DappTools, che è un precursore di Foundry. Sia HEVM che Halmos hanno la caratteristica di non richiedere una specifica separata e possono eseguire simbolicamente test esistenti per identificare violazioni di asserzioni. Ciò consente agli utenti di utilizzare entrambi gli strumenti in modo intercambiabile o di eseguirli in parallelo per gli stessi test, fornendo loro più opzioni per i test simbolici.
  
  Vale la pena notare che, nonostante le loro somiglianze, HEVM e Halmos sono stati sviluppati in modo indipendente e differiscono nei dettagli di implementazione; in particolare in termini di ottimizzazioni e strategie di ragionamento simbolico. Inoltre, HEVM è scritto in Haskell, mentre Halmos è scritto in Python, fornendo visibilità al ricco ecosistema Python. Avere la possibilità di utilizzare entrambi gli strumenti offre agli utenti maggiore flessibilità e opzioni per garantire la sicurezza e la correttezza degli smart contract.

Halmos è open source e attualmente nella sua fase beta. Stiamo lavorando attivamente su nuovi Caratteristiche e funzionalità, inclusi i cheat code di Foundry e molte altre caratteristiche chiave di usabilità. Apprezzeremmo molto i tuoi pensieri su quali funzionalità sono più importanti e accogliamo con favore qualsiasi feedback, suggerimento e contributo per rendere Halmos uno strumento migliore per tutti.

**

Le opinioni qui espresse sono quelle del personale di AH Capital Management, LLC ("a16z") citato e non sono le opinioni di a16z o delle sue affiliate. Alcune informazioni qui contenute sono state ottenute da fonti di terze parti, incluse società in portafoglio di fondi gestiti da a16z. Sebbene tratti da fonti ritenute affidabili, a16z non ha verificato in modo indipendente tali informazioni e non fornisce dichiarazioni sull'accuratezza attuale o duratura delle informazioni o sulla sua adeguatezza per una determinata situazione. Inoltre, questo contenuto può includere pubblicità di terze parti; a16z non ha esaminato tali annunci pubblicitari e non approva alcun contenuto pubblicitario in essi contenuto.

Questo contenuto viene fornito solo a scopo informativo e non deve essere considerato come consulenza legale, commerciale, di investimento o fiscale. Dovresti consultare i tuoi consulenti in merito a tali questioni. I riferimenti a qualsiasi titolo o risorsa digitale sono solo a scopo illustrativo e non costituiscono una raccomandazione di investimento o un'offerta per fornire servizi di consulenza in materia di investimenti. Inoltre, questo contenuto non è diretto né destinato all'uso da parte di investitori o potenziali investitori e non può in alcun caso essere invocato quando si decide di investire in qualsiasi fondo gestito da a16z. (Un'offerta per investire in un fondo a16z sarà fatta solo dal memorandum di collocamento privato, dal contratto di sottoscrizione e da altra documentazione pertinente di tale fondo e dovrebbe essere letta nella sua interezza.) Eventuali investimenti o società in portafoglio menzionati, citati o descritti non sono rappresentativi di tutti gli investimenti in veicoli gestiti da a16z, e non si può garantire che gli investimenti saranno redditizi o che altri investimenti effettuati in futuro avranno caratteristiche o risultati simili. Un elenco degli investimenti effettuati da fondi gestiti da Andreessen Horowitz (esclusi gli investimenti per i quali l'emittente non ha autorizzato a16z a divulgare pubblicamente e gli investimenti non annunciati in asset digitali quotati in borsa) è disponibile all'indirizzo https://a16z.com/investments /.

Grafici e grafici forniti all'interno sono esclusivamente a scopo informativo e non dovrebbero essere presi in considerazione quando si prende una decisione di investimento. I rendimenti passati non sono indicativi di risultati futuri. Il contenuto parla solo a partire dalla data indicata. Eventuali proiezioni, stime, previsioni, obiettivi, prospettive e/o opinioni espresse in questi materiali sono soggette a modifiche senza preavviso e possono differire o essere contrarie alle opinioni espresse da altri. Si prega di consultare https://a16z.com/disclosures per ulteriori informazioni importanti.