Input Output presenta Blaster per la verifica degli smart contract di Cardano

Cardano Community ha pubblicato una presentazione di Blaster, uno strumento di verifica automatizzata progettato per controllare se gli smart contract di Cardano seguono le regole specificate. Gli ingegneri di Input Output Romain Soulat e Jean-Frédéric Etienne mostrano come lo strumento esamina tali proprietà e può produrre un controesempio quando rileva una violazione. Discutono inoltre dei lavori in corso sulla ricostruzione delle prove e dei modi per rendere i risultati più facili da ispezionare.

Definire che cosa deve fare un contratto su Cardano

Gli smart contract stabiliscono condizioni per le transazioni sulla blockchain e determinano come le applicazioni gestiscono gli asset. Uno sviluppatore può specificare, per esempio, che solo un utente autorizzato possa sbloccare i fondi detenuti da un contratto. La verifica formale utilizza metodi matematici per controllare se un sistema soddisfa proprietà scritte in una specifica. Mentre un test convenzionale esamina casi selezionati, la verifica formale mira a stabilire se una proprietà dichiarata valga per tutti i casi coperti dal modello.

Soulat, technical lead di Cardano High Assurance, ha spiegato che Blaster è pensato per automatizzare gran parte del lavoro di dimostrazione. Gli sviluppatori devono comunque definire il comportamento che vogliono verificare e fornire la specifica corrispondente. Quando lo strumento trova una violazione, può produrre un controesempio da ispezionare. Soulat ha descritto una transazione o una sequenza di transazioni che potrebbe mostrare qualcuno diverso dall’utente autorizzato che sblocca un output.

Come Blaster verifica le proprietà dei contratti

Blaster utilizza Lean 4, un sistema per esprimere enunciati matematici e lavorare con le dimostrazioni, insieme a un risolutore automatico. Innanzitutto semplifica il problema; se la proprietà non viene risolta in quella fase, il problema rimanente può essere inviato al risolutore. Per rendere i controlli pertinenti a Cardano, il team ha formalizzato parti dell’ambiente in cui i contratti vengono eseguiti, inclusa l’esecuzione degli script e le regole delle transazioni.

Etienne, ingegnere senior di metodi formali, ha delineato tre possibili risultati: una proprietà può essere riportata come valida, falsificata oppure indeterminata. Un controesempio associato a un risultato falsificato può aiutare gli sviluppatori a individuare un bug del contratto, un’assunzione mancante o un errore nella specifica. Un risultato indeterminato significa che il risolutore non ha stabilito se la proprietà valga. La portata di un controllo dipende dalle proprietà che gli sviluppatori scelgono di esprimere.

[NEWSBREAK]

La ricostruzione delle prove è in sviluppo

Gli sviluppatori possono compilare contratti scritti in linguaggi come Plinth, Aiken o Plutarch in Untyped Plutus Core, la rappresentazione utilizzata per eseguire gli script di Cardano. Possono quindi importare il codice compilato in Lean 4 e specificare le proprietà da verificare. In precedenza, Input Output ha rilasciato due librerie open source che forniscono i modelli specifici di Cardano per questo processo. In una dimostrazione precedente, il team ha utilizzato la pipeline su un contratto di esercitazione proveniente da una sfida di sicurezza, generando un contesto di transazione che mostrava come il contratto potesse essere sfruttato.

Etienne ha spiegato che la ricostruzione delle prove è ancora in sviluppo. L’obiettivo è consentire a Lean di verificare in modo indipendente le evidenze a supporto di un risultato valido; lo strumento attuale non produce ancora una prova ricostruita in Lean quando il risolutore restituisce quel risultato. Soulat ha inoltre illustrato piani per viste di controesempio più chiare, che consentano agli sviluppatori di ispezionare i dettagli della transazione alla base di una proprietà non soddisfatta.