Formal Methods for Smart Contracts

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.

• Autores: Bell Llinas, José Vicente; Ramírez Payares, Andrés Felipe; Vergara Arrieta, Juan Camilo
• Fecha de publicación: 2019
• Institución: Universidad del Norte
• Repositorio: Repositorio Uninorte
• Idioma: spa
• OAI Identifier: oai:manglar.uninorte.edu.co:10584/8443
• Acceso en línea: http://hdl.handle.net/10584/8443
• Palabra clave: Métodos formales; Lenguaje; Seguridad; Privacidad; Criptomonedas; Blockchains; Smart Contracts; Language; Security; Formal methods; Privacy; Cryptocurrencies; Blockchains
• License: Universidad del Norte