Paper Info
Title
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.
Year
DOI
Venue
2016
10.1145/2993600.2993611
PLAS@CCS
Field
DocType
ISBN
Virtual machine,Solidity,Functional programming,Computer security,Computer science,Correctness,Stack machine,Cryptocurrency,Bytecode,Formal verification
Conference
978-1-4503-4574-3
Citations 
PageRank 
References 
48
3.11
4
Authors
11
Name
Order
Citations
PageRank
Karthikeyan Bhargavan1132576.07
Antoine Delignat-Lavaud225616.17
Cédric Fournet33698213.79
Anitha Gollamudi4483.11
Georges Gonthier52275195.06
Nadim Kobeissi61039.50
Natalia Kulatova7494.13
Aseem Rastogi813314.49
Thomas Sibut-Pinote9514.25
Nikhil Swamy1076345.69
Santiago Zanella Beguelin116073475.81