Formal Verification of Smart Contracts: Short Paper

Abstract : Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM code; instead, they can program in a JavaScript-like language, called Solidity, that compiles to bytecode. Since the main purpose of EVM is to execute smart contracts that manage and transfer digital assets (called Ether), security is of paramount importance. However, writing secure smart contracts can be extremely difficult: due to the openness of Ethereum, both programs and pseudonymous users can call into the public methods of other programs, leading to potentially dangerous compositions of trusted and untrusted code. This risk was recently illustrated by an attack on TheDAO contract that exploited subtle details of the EVM semantics to transfer roughly $50M worth of Ether into the control of an attacker. In this paper, we outline a framework to analyze and verify both the runtime safety and the functional correctness of Ethereum contracts by translation to F*, a functional programming language aimed at program verification.
Type de document :
Communication dans un congrès
ACM Workshop on Programming Languages and Analysis for Security, Oct 2016, Vienna, Austria. Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, 2016, 〈10.1145/2993600.2993611〉
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01400469
Contributeur : Thomas Sibut-Pinote <>
Soumis le : mardi 29 novembre 2016 - 13:38:19
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : lundi 27 mars 2017 - 08:31:13

Fichier

solidether.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, et al.. Formal Verification of Smart Contracts: Short Paper. ACM Workshop on Programming Languages and Analysis for Security, Oct 2016, Vienna, Austria. Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, 2016, 〈10.1145/2993600.2993611〉. 〈hal-01400469〉

Partager

Métriques

Consultations de la notice

681

Téléchargements de fichiers

757