Formal Verification of Smart Contracts: Short Paper

By Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, T. Sibut-Pinote, Nikhil Swamy and 1 more. PLAS@CCS, 2016

631 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Information Systems, Signal Processing

View Paper: https://www.semanticscholar.org/paper/4b13d7d3abcd071619bd4834882fccda95bc7c98

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Signal Processing

Citations in the corpus

ZEUS: Analyzing Safety of Smart Contracts (2018, background): “Like prior art [54], a formal proof for soundness of the translation strategy is outside the scope of this work.”
The Roadmap to 6G Security and Privacy (2021, neutral): “The accurate functionality of smart contacts can be checked by identifying semantic flaws [101], [102], using security check tools [103], [104], [105] and performing formal verification [106]–[109].”
teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts (2018, methodology): “[9] presents EVM* and Solidity* that provide a direct translation of a subset of EVM bytecode and Solidity into F* respectively, which can then be used for further verification.”
Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks (2018, background): “Other works leverage translation to F* to prove safety and security properties of smart contracts and to improve on existing static analysis tools [12], [20].”
sFuzz: An Efficient Adaptive Fuzzer for Solidity Smart Contracts (2020, background): “proposed a framework to verify smart contracts formally by transforming the source code and the bytecode to F*, a language designed for verification [9].”
Securify: Practical Security Analysis of Smart Contracts (2018, methodology): “[23] present preliminary work on verifying Ethereum smart contracts by translating Solidity and EVM bytecode to an existing verification system.”
MadMax: surviving out-of-gas conditions in Ethereum smart contracts (2018, methodology): “The formal verification tool by [Bhargavan et al. 2016] detects three classes of vulnerabilities, two of which were covered by Oyente.”
Blockchain-Enabled Smart Contracts: Architecture, Applications, and Future Trends (2019, methodology): “Overview of workflow in the Ethereum network [6].”
Combining Graph Neural Networks With Expert Knowledge for Smart Contract Vulnerability Detection (2021, methodology): “For example, [22] introduces a framework, translating Solidity”
Blockchain-based Smart Contracts: A Systematic Mapping Study (2017, methodology): “The first one is the difficulty of writing correct smart contracts [8,16,1718].”