Nella spinta alla verifica formale, Ethereum cerca la certezza dei contratti intelligenti

Giusto in tempo per l'autunno, arriva una nuova parola d'ordine nel mondo della blockchain: verifica formale.

La frase (usata per descrivere l'applicazione della matematica per verificare i programmi software) è stata finora evocata scarsamentenella stampaMa se la conversazione al summit degli sviluppatori di Ethereum della scorsa settimana fosse un'indicazione, potrebbe svolgere un ruolo sempre più importante, dati i dubbi sulla sicurezza che ancora circondano gli smart contract e le blockchain in senso più ampio.

Come dimostrato dai numerosi interventi dedicati all'argomento al Devcon2, l'idea che ai programmatori Ethereum possano essere date nuove garanzie è ampiamente accolta dalla sua comunità di sviluppo. Il concetto è già stato proposto come un modo per ispirare fiducia in tutto, dal protocollo Ethereum stesso alla sua blockchain proof-of-stake sperimentale.

Che ciò sia accaduto non sorprende forse, dato il crollo improvviso di The DAO quest'estate, finora il più grande contratto intelligente mai lanciato sulla piattaforma di sviluppo di applicazioni decentralizzate.

Ma mentreverifica formale può sembrare complesso, ma il concetto può essere riassunto in modo succinto se applicato a Ethereum : attualmente i programmatori utilizzano un linguaggio in gran parte nuovo (Solidity) per scrivere contratti intelligenti, scrivendo comandi che vengono poi tradotti in bytecode per l'uso da parte della macchina virtuale Ethereum (EVM) e distribuiti ai nodi della rete per l'esecuzione.

In un certo senso, la verifica formale può essere vista come un modo più oggettivo per garantire che quando diverse componenti della rete ricevono queste istruzioni, le eseguano come previsto per conto degli utenti.

Grant Passmore, co-fondatore di Aesthetic Integration, è ONE imprenditore che vede un'opportunità nel contribuire a questo sforzo, utilizzando Devcon2 per lanciare Imandra Contracts, una piattaforma di verifica formale per contratti intelligenti basati su blockchain.

Nel corso dell'evento, ha evocato l'idea che Ethereum potrebbe fungere da "paradiso" per la verifica formale (un punto di contatto ampiamente citato nei discorsi), dati gli obiettivi della sua comunità e le significative responsabilità che desidera affidare al codice.

Passmore ha detto a CoinDesk:

"La comunità Ethereum è in una posizione unica, dove dopo The DAO, abbiamo capito che è necessaria un'ingegneria rigorosa. T puoi approcciarti alla scrittura di uno smart contract come un'app web."

Altrove, relatori come Philip Daian della Cornell hanno parlato dell'interesse per la metodologia in senso più ampio, affermando al pubblico che secondo lui la verifica formale potrebbe aiutare Ethereum a risolvere problemi chiave.

"Sarà ONE elemento fondamentale del quadro generale. Non vedo l'ora di usare Ethereum per stabilire lo standard e mostrare alle persone come si fa", ha detto.

Rotelle di allenamento

Data la recente enfasi che le società finanziarie hanno posto sull’esplorazionelinguaggi di smart contracting, forse il concetto di applicazione della verifica formale a Solidity è stato l'argomento di discussione più frequente.

Sviluppato per la piattaforma Ethereum , Solidity è stato criticato per essere stato ampiamente non testato e difficile da scrivere, in gran parte perché è così nuovo. Tali problemi sono stati probabilmente amplificati a causa di problemicon il compilatore del linguaggio, la mancanza di librerie pubbliche e il crollo di The DAO, che è stato esaminato da membri illustri della sua comunità di sviluppo.

In quest'ottica, Christian Reitweissner, il creatore di Solidity, ha riconosciuto che c'è una spinta a implementare una verifica formale affinché gli errori possano essere rilevati in modo più efficace dai programmatori Ethereum .

Reitweissner ha detto a CoinDesk che gli sviluppatori di smart contract potrebbero ONE giorno usare strumenti di verifica formale per, ad esempio, determinare se ci sono errori imprevisti nel loro lavoro. Ha indicato che tale strumento potrebbe essere usato per determinare se, nell'aggiungere due saldi, il risultato si estendesse più a lungo del campo assegnato dal compilatore.

"Questo potrebbe accadere e lo strumento di verifica formale [lo] rileverebbe automaticamente. È possibile rilevarlo in anticipo e reagire all'interno dello smart contract", ha spiegato.

Reitweissner ha affermato che il team di Solidity ha già iniziato a esplorare come applicare la verifica formale al proprio lavoro. Giàlo scorso ottobre, esistevano prototipi di come un toolkit chiamato Why3 potesse essere utilizzato a questo scopo, sebbene tali soluzioni non siano ancora disponibili per il linguaggio completo.

Banco di prova

Un altro argomento ampiamente discusso durante la conferenza è stato il fatto che Ethereum potrebbe essere utilizzato per testare in che modo la verifica formale potrebbe essere applicata alla Finanza in senso più ampio.

Passmore, ad esempio, ha affermato che Aesthetic Integration lavora all'applicazione della verifica formale nelle relazioni con gli istituti finanziari dal 2014 e che finora i clienti hanno cercato di utilizzarla in aree limitate, come i dark pool, in cui i trader necessitano di certezza in termini di correttezza.

Nei contratti intelligenti, Passmore ha affermato di vedere Ethereum come una comunità che potrebbe favorirne ulteriormente l'accettazione.

"Quando abbiamo iniziato a collaborare con molti dei nostri clienti bancari, abbiamo sentito che erano interessati al settore, ma che erano preoccupati della correttezza degli smart contract", ha affermato.

L'avanzamento della verifica formale ha attratto anche Yoichi Hirai per ragioni simili. Un ingegnere di verifica formale ora impiegato presso la Ethereum Foundation, il suo interesse per il concetto è iniziato come ricercatore e nel suo precedente impiego presso il leader della sicurezza informatica FireEye.

In un intervento alla conferenza, Hirai ha parlato della sua frustrazione nell'applicare la verifica formale in contesti in cui non aveva accesso al codice sorgente o in cui i compiti erano forse troppo ampi per far progredire il concetto.

"Ho trovato Ethereum, ho visto l'EVM, il documento giallo, le specifiche, erano solo 32 pagine e ho pensato di poterle tradurre e scrivere delle prove sui contratti intelligenti", ha detto.

Ethereum, al contrario, offre quella che lui stesso ha definito una "specifica più piccola" e un "problema risolvibile" per gli ingegneri che vogliono determinare il modo migliore per tradurre Solidity in bytecode.

"Credo che arriveranno molti altri ricercatori sulla verifica formale", ha affermato.

Nessuna soluzione miracolosa

Tuttavia, nonostante l'entusiasmo, si stanno prendendo misure per mettere in guardia su quanto potrebbe raggiungere la verifica formale. Lo sviluppatore Alex Beregszaszi, che sta lavorando agli aggiornamenti dell'EVM, ha parlato della necessità di una serie di soluzioni per aiutare gli sviluppatori a garantire che il codice del contratto intelligente funzioni come previsto.

Anche Passmore ha osservato che è difficile dire se il suo nuovo sistema avrebbe potuto rilevare i problemi con The DAO, poiché gli strumenti di verifica formale richiedono ancora l'intervento Human .

"È possibile codificare i problemi che si sono verificati con The DAO e verificare che T siano presenti, ma è necessario sapere cosa cercare", ha spiegato.

Le limitazioni sono state riconosciute da Reitweissner e Passmore, i quali hanno entrambi messo in guardia gli sviluppatori dal considerare la verifica formale come una “soluzione miracolosa”.

Reitweissner, tuttavia, vede la metodologia come ONE che progredirà man mano che sarà più ampiamente utilizzata, con gli sviluppatori che diventeranno lentamente più bravi nell'identificare i problemi e nello sviluppare repository in cui la conoscenza dei problemi comuni può essere resa accessibile

In questo modo, Passmore ritiene che la comunità Ethereum stia riuscendo a "evangelizzare" il concetto, cosa che, a suo avviso, alla fine farà progredire la ricerca sulla blockchain.

Passmore ha concluso:

"Sebbene si tratti di qualcosa a cui molti non sono mai stati esposti, la verifica formale è ciò di cui abbiamo bisogno. È una curva di apprendimento, ma deve essere abbracciata, e questo è entusiasmante."

Immagini tramite Pete Rizzo per CoinDesk