Formal Methods for Smart Contracts

Abstract

Blockchains are secure distributed databases that enable all types of transactions between two or more parties without the need for intermediaries; Among the best known we find Bitcoin and Ethereum. Smart Contracts are immutable computer programs that are deployed in a Blockchain and automatize such transactions.

Blockchains and Smart Contracts are subject to constant attacks, such as the DAO (Decentralized Autonomous Organization) one, in which an attacker took advantage of the security flaws existing in Solidity (main language of Ethereum) written contracts draining millions of dollars. It is necessary to provide alternatives to maintain the integrity of Smart Contracts and prevent cases like the DAO from happening again.

We propose the design of a language for the coding of Smart Contracts, without the security flaws introduced by Solidity, whose programs can be formally verified through the translation into the smart contract language PACT.

In Smarty, the language we propose, contracts are modeled through entities and events. The entities have names, fields and their respective types. The events are analogous to functions and methods, they can be creational or custom. Smarty dispenses with features such as inheritance and recursion, and possesses invariants, preconditions, and exceptions.

We use the ANTLR tool for the definition of Smarty’s grammar, the generation of Parser and Lexer classes; String Template for the construction of the base template for the translation to the PACT language, and finally JAVA to visit the syntactic tree and execute the translation of instructions.

We present a tool for the coding of Smart Contracts: -Not susceptible to security problems such as reentrancy, a breach that made possible the DAO case. -Includes formal software design and verification techniques. -Verifiable (via PACT translation). -Moderate coding Complexity, accessible.

Las Blockchains son bases de datos distribuidas y seguras que permiten todo tipo de transacciones entre dos o más partes sin necesidad de intermediarios; entre las más conocidas se encuentran Bitcoin y Ethereum. Los Smart Contracts son programas de computador inmutables que se despliegan en una Blockchain y automatizan tales transacciones. Blockchains y Smart Contracts son objeto de constantes ataques, como el de la DAO (Decentralized Autonomous Organization), en el cual un atacante tomó provecho de los defectos de seguridad de contratos escritos en Solidity (principal lenguaje de Ethereum) drenando millones de dólares. Se hace necesario brindar alternativas para mantener la integridad de Smart Contracts y evitar que casos como el de la DAO se repitan. Proponemos el diseño de un lenguaje para la codificación de Smart Contracts, sin las falencias de seguridad que introducía Solidity, cuyos programas pueden ser verificados formalmente a través de la traducción al lenguaje de Smart Contracts PACT. En Smarty, el lenguaje que proponemos, se modelan los contratos a través de entidades y eventos. Las entidades poseen nombres, campos y sus respectivos tipos. Los eventos son análogos a las funciones y métodos, pueden ser creacionales o personalizados. Smarty prescinde de características como herencia y recursividad, y cuenta con invariantes, precondiciones y excepciones. Empleamos la herramienta ANTLR para la definición de la gramática de Smarty, generación de clases Parser y Lexer; String Template para la construcción de la plantilla base para la traducción al lenguaje PACT, y finalmente JAVA para visitar el árbol sintáctico y ejecutar la traducción de instrucciones. Presentamos una herramienta para la codificación de Smart Contracts: -No susceptible a problemas de seguridad como la reentrancia, brecha que posibilitó el caso de la DAO -Incluye técnicas formales de diseño y verificación de software -Verificable (vía traducción a PACT) -Complejidad de codificación moderada.