An extended compiler for safe Teal smart contracts

Smart contracts (SCs) are powerful applications used by the most efficient blockchains. For this reason it is crucial to be able to write safe and correct smart contracts in a simple way. The Algorand blockchain writes SCs in the programming language Teal. Since Teal is a low level language difficult to be used, many errors can occur. Several researches have tried to solve this problem. Among all of them, an innovative solution is found in the alternative model in "A formal model for Algorand smart contract" . The authors exploit this framework to prove fundamental properties of the Algorand blockchain, and to establish the security of some archetypal SCs. A declarative language for the implementation of smart contract is defined, based on the formal model. This work includes also a tool called Secteal. It provides a compiler whose main function is translating the declarative language into Teal. The aim of our work is enhancing Secteal. Our new compiler is able to handle even complex SCs for every type of transaction. It checks the correctness of the smart contract provided by the user, ensuring a better safety of the whole process. Safeness is guaranteed by validation of necessary conditions for every type of stateless smart contract. The output of Secteal is a Teal contract ready to be deployed on Algorand. To achieve these goals we have implemented various Secure functions that guide the user to correct the SC in case of errors or missing safety conditions.

I contratti intelligenti (SC) sono applicazioni che hanno portato grandi miglioramenti alle più efficienti blockchain. Per questa ragione è cruciale essere in grado di scrivere contratti intelligenti sicuri e corretti in modo semplice. Algorand utilizza il linguaggio di programmazione Teal per implementare i suoi contratti. Esso è un linguaggio di basso livello, difficile da utilizzare. Questo porta ad accrescere il numero di errori. Diversi studi sono stati presentati su questo tema per diverse tipologie di blockchain. Una soluzione innovativa per Algorand è stata proposta in "A formal model for Algorand smart contract". Gli autori presentano un modello per provare le proprietà fondamentali di Algorand e per definire un metodo per la costruzione di contratti intelligenti sicuri. Il lavoro include un applicazione chiamata SecTeal. Questa si basa principalmente su un compilatore che ha come funzione principale quella di tradurre il nuovo linguaggio basato sul modello in Teal. L’obiettivo del nostro lavoro è quello di completare SecTeal. Il nostro compilatore sarà capace di gestire anche contratti intelligenti più articolati per ogni tipo di transazione controllando la correttezza del contratto in ingresso a SecTeal. Questo assicurerà maggior sicurezza all’intero processo. La sicurezza è garantita dalla presenza di condizioni necessarie per ogni tipo di SC. Il risultato finale della nostra applicazione è un contratto intelligente scritto in Teal pronto per essere distribuito su Algorand. Per raggiungere questi obbiettivi verranno implementate diverse funzioni di sicurezza le quali analizzeranno e aggiusteranno il contratto intelligente in caso di errori e mancanza di condizioni di sicurezza.