Call me back, i have a type invariant

Abstract

Callbacks in Smart Contracts on blockchain-based distributed ledgers are a potential source of security vulnerabilities: callbacks may lead to reentrancy, which has been previously exploited to steal large sums of money. Unfortunately, analysis tools for Smart Contracts either fail to support callbacks or simply detect and disallow patterns of callbacks that may lead to reentrancy. As a result, many authors of Smart Contracts avoid callbacks altogether, and some Smart Contract programming languages, including Solidity, recommend using primitives that avoid callbacks. Nevertheless, reentrancy remains a threat, due to the utility of and frequent reliance on callbacks in Smart Contracts. In this paper, we propose the use of type invariants, a feature of some languages supporting formal verification, to enable proof of correctness for Smart Contracts, including Smart Contracts that permit or rely on callbacks. Our result improves upon existing research because it neither forbids reentrancy nor relies on informal, meta-arguments to prove correctness of reentrant Smart Contracts. We demonstrate our approach using the SPARK programming language, which supports type invariants and moreover can be compiled to relevant blockchains.