The development of blockchain technologies has enabled the trustless execution of so-called smart contracts, i.e. programs that regulate the exchange of assets (e.g., cryptocurrency) between users. In a decentralized blockchain, the state of smart contracts is collaboratively maintained by a peer-to-peer network of mutually untrusted nodes, which collect from users a set of transactions (representing the required actions on contracts), and execute them in some order. Once this sequence of transactions is appended to the blockchain, the other nodes validate it, re-executing the transactions in the same order. The serial execution of transactions does not take advantage of the multi-core architecture of modern processors, so contributing to limit the throughput. In this paper we propose a true concurrent model of smart contract execution. Based on this, we show how static analysis of smart contracts can be exploited to parallelize the execution of transactions.
Solidity is an object-oriented and high-level language for writing smart contracts that are used to execute, verify and enforce credible transactions on permissionless blockchains. In the last few years, analysis of smart contracts has raised considerable interest and numerous techniques have been proposed to check the presence of vulnerabilities in them. Current techniques lack traceability in source code and have widely differing work flows. There is no single unifying framework for analysis, instrumentation, optimisation and code generation of Solidity contracts. In this paper, we present SIF, a comprehensive framework for Solidity contract analysis, query, instrumentation, and code generation. SIF provides support for Solidity contract developers and testers to build source level techniques for analysis, understanding, diagnostics, optimisations and code generation. We show feasibility and applicability of the framework by building practical tools on top of it and running them on 1838 real smart contracts deployed on the Ethereum network.
A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe program is used for critical systems. Therefore, formal methods for these kinds of systems are greatly required. In this paper, we use a formal language that performs deductive verification on an Ethereum Blockchain application based on smart contracts, which are self-executing digital contracts. Blockchain systems manipulate cryptocurrency and transaction information. Therefore , if a bug occurs in the blockchain, serious consequences such as a loss of money can happen. Thus, the aim of this paper is to propose a language dedicated to deductive verification, called Why3, as a new language for writing formal and verified smart contracts, thereby avoiding attacks exploiting such contract execution vulnerabilities. We first write a Why3 smart contracts program; next we formulate specifications to be proved as absence of RunTime Error properties and functional properties, then we verify the behavior of the program using the Why3 system. Finally we compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreover, we give a set of generic mathematical statements that allows verifying functional properties suited to any type of smart contracts holding cryptocurrency, showing that Why3 can be a suitable language to write smart contracts. To illustrate our approach, we describe its application to a realistic industrial use case.
Franklin Schrans, Daniel Hails, Alexander Harkness, Sophia Drossopoulou · 5 authors
The Ethereum blockchain platform supports the execution of decentralised applications or smart contracts. These typically hold and transfer digital currency to other parties on the platform; however, they have been subject to numerous attacks due to the unintentional introduction of bugs. Over a billion dollars worth of currency has been stolen since its release in July 2015. As smart contracts cannot be updated after deployment, it is imperative that the programming language supports the development of robust contracts. We propose Flint, a new statically-typed programming language specifically designed for writing robust smart contracts. Flint's features enforce the writing of safe and predictable code. To encourage good practices, we introduce protection blocks. Protection blocks restrict who can run code and when (using typestate) it can be executed. To prevent vulnerabilities relating to the unintentional loss of currency, Flint Asset traits provide safe atomic operations, ensuring the state of contracts is always consistent. Writes to state are restricted, simplifying reasoning about smart contracts.
This paper reports on the development of a formal symbolic process virtual machine (FSPVM) denoted as FSPVM-E for verifying the reliability and security of Ethereum-based services at the source code level of smart contracts, and a Coq proof assistant is employed for both programming the system and for proving its correctness. The current version of FSPVM-E adopts execution-verification isomorphism, which is an application extension of Curry-Howard isomorphism, as its fundamental theoretical framework to combine symbolic execution and higher-order logic theorem proving. The four primary components of FSPVM-E include a general, extensible, and reusable formal memory framework, an extensible and universal formal intermediate programming language denoted as Lolisa, which is a large subset of the Solidity programming language using generalized algebraic datatypes, the corresponding formally verified interpreter of Lolisa, denoted as FEther, and assistant tools and libraries. The self-correctness of all components is certified in Coq. Currently, FSPVM-E supports the ERC20 token standard, and can automatically and symbolically execute Ethereum-based smart contracts, scan their standard vulnerabilities, and verify their reliability and security properties with Hoare-style logic in Coq. To the best of authors' knowledge, the present work represents the first hybrid formal verification system implemented in Coq for Ethereum smart contracts that is applied at the Solidity source code level.
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Arash Pourdamghani
In today's programmable blockchains, smart contracts are limited to being deterministic and non-probabilistic. This lack of randomness is a consequential limitation, given that a wide variety of real-world financial contracts, such as casino games and lotteries, depend entirely on randomness. As a result, several ad-hoc random number generation approaches have been developed to be used in smart contracts. These include ideas such as using an oracle or relying on the block hash. However, these approaches are manipulatable, i.e. their output can be tampered with by parties who might not be neutral, such as the owner of the oracle or the miners. We propose a novel game-theoretic approach for generating provably unmanipulatable pseudorandom numbers on the blockchain. Our approach allows smart contracts to access a trustworthy source of randomness that does not rely on potentially compromised miners or oracles, hence enabling the creation of a new generation of smart contracts that are not limited to being non-probabilistic and can be drawn from the much more general class of probabilistic programs.
Open access
3 source records
Blockchain Technology Applications and Security
Cryptography and Data Security
Advanced Steganography and Watermarking Techniques
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning · 5 authors
Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventing the duplication or deletion of a contract's assets. This article presents the design and type-theoretic foundation of Nomos, a programming language for digital contracts that addresses these challenges. To express and enforce protocols, Nomos is based on shared binary session types. To control resource usage, Nomos employs automatic amortized resource analysis. To prevent the duplication or deletion of assets, Nomos uses a linear type system. A monad integrates the effectful session-typed language with a general-purpose functional language. Nomos' prototype implementation features linear-time type checking and efficient type reconstruction that includes automatic inference of resource bounds via off-the-shelf linear optimization. The effectiveness of the language is evaluated with case studies about implementing common smart contracts such as auctions, elections, and currencies. Nomos is completely formalized, including the type system, a cost semantics, and a transactional semantics to instantiate Nomos contracts on a blockchain. The type soundness proof ensures that protocols are followed at run-time and that types establish sound upper bounds on the resource consumption, ruling out re-entrancy and out-of-gas vulnerabilities.
We consider the problem of expected cost analysis over nondeterministic probabilistic programs, which aims at automated methods for analyzing the resource-usage of such programs. Previous approaches for this problem could only handle nonnegative bounded costs. However, in many scenarios, such as queuing networks or analysis of cryptocurrency protocols, both positive and negative costs are necessary and the costs are unbounded as well. In this work, we present a sound and efficient approach to obtain polynomial bounds on the expected accumulated cost of nondeterministic probabilistic programs. Our approach can handle (a) general positive and negative costs with bounded updates in variables; and (b) nonnegative costs with general updates to variables. We show that several natural examples which could not be handled by previous approaches are captured in our framework. Moreover, our approach leads to an efficient polynomial-time algorithm, while no previous approach for cost analysis of probabilistic programs could guarantee polynomial runtime. Finally, we show the effectiveness of our approach by presenting experimental results on a variety of programs, motivated by real-world applications, for which we efficiently synthesize tight resource-usage bounds.
The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of EVM bytecode, relatively little attention has been devoted to that of Solidity. In this paper we propose a minimal calculus for Solidity contracts, which extends an imperative core with a single primitive to transfer currency and invoke contract procedures. We build upon this formalisation to give semantics to the Ethereum blockchain. We show our calculus expressive enough to reason about some typical quirks of Solidity, like e.g. re-entrancy.
We present a toolchain for developing and verifying smart contracts that can be executed on Bitcoin. The toolchain is based on BitML, a recent domain-specific language for smart contracts with a computationally sound embedding into Bitcoin. Our toolchain automatically verifies relevant properties of contracts, among which liquidity, ensuring that funds do not remain frozen within a contract forever. A compiler is provided to translate BitML contracts into sets of standard Bitcoin transactions: executing a contract corresponds to appending these transactions to the blockchain. We assess our toolchain through a benchmark of representative contracts.
Yuepeng Wang, Shuvendu K. Lahiri, Shuo Chen, Rong Pan · 7 authors
Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. This paper studies the safety and security of smart contracts in the \emph{Azure Blockchain Workbench}, an enterprise Blockchain-as-a-Service offering from Microsoft. As part of this study, we formalize \emph{semantic conformance} of smart contracts against a state machine model with access-control policy and develop a highly-automated formal verifier for Solidity that can produce proofs as well as counterexamples. We have applied our verifier {\sc VeriSol} to analyze {\it all} contracts shipped with the Azure Blockchain Workbench, which includes application samples as well as a governance contract for Proof of Authority (PoA). We have found previously unknown bugs in these published smart contracts. After fixing these bugs, {\sc VeriSol} was able to successfully perform full verification for all of these contracts.
Purposely modular, this protocol enables customization of several protocol properties, including the consensus properties implemented, blockchain type, the roots used, and virtual machine opcodes, among others. These modules enable implementing parties to control the behavior of their economy, with a minimal amount of effort, and no sacrifice in participant cryptoeconomic quality. This work also demonstrates the simplification of the developer experience by abstracting away all technological details, except basic CRUD-based operations, using various programming languages. We demonstrate the mechanism design approach taken, and formalize a process for deploying populations of blockchain economies at scale. The framework shown includes adequate tooling for simulation, development, deployment, maintenance, and analytic-based decision making. Lastly, we introduce an expressive programming language for the purpose of creating, and interacting with the cryptoeconomy designed by the implementing developer.
Smart contracts are a special type of programs running inside a blockchain. Immutable and transparent, they provide means to implement fault-tolerant and censorship-resistant services. Unfortunately, its immutability causes a serious challenge of ensuring that a business logic and implementation is correct upfront, before publishing in a blockchain. Several big accidents have indeed shown that users of this technology need special tools to verify smart contract correctness. Existing automated checkers are able to detect only well known implementation bugs, leaving the question of business logic correctness far aside. In this work, we present a symbolic model-checking technique along with a formal specification method for a subset of Solidity programming language that is able to express both state properties and trace properties; the latter constitutes a weak analogy of temporal properties. We evaluate the proposed technique on the MiniDAO smart contract, a young brother of notorious TheDAO. Our Proof-of-Concept was able to detect a non-trivial error in the business logic of this smart contract in a few seconds.
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised. There is a wide family of contract vulnerabilities due to out-of-gas behaviours. We report on the design and implementation of GASTAP, a Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers sound gas upper bounds for all its public functions. Our bounds ensure that if the gas limit paid by the user is higher than our inferred gas bounds, the contract is free of out-of-gas vulnerabilities.
Blockchain technology adds records to a list using cryptographic links. Therefore, the security of blockchain smart contracts is among the most popular contemporary research topics. To improve the theorem-proving technology in this field, we are developing an extensible hybrid verification tool chain, denoted as FSPVM-E, for Ethereum smart contract verification. This hybrid system extends the proof assistants in Coq, a formal proof-management system. Combining symbolic execution with higher-order theorem-proving, it solves consistency, automation, and reusability problems by standard theorem-proving approaches. This article completes the FSPVM-E by developing its proof engine. FSPVM-E is an extensible definitional interpreter based on our previous work FEther, which is totally developed in the Coq proof assistant. It supports almost all semantics of the Solidity programing language, and simultaneously executes multiple types of symbols. FEther also contains a set of automatic strategies that execute and verify the smart contracts in Coq with a high level of automation. The functional correctness of FEther was verified in Coq. In standard tutorials, the execution efficiency of FEther far exceeded that of the interpreters developed in Coq.
Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu · 8 authors
The rise of modern blockchains has facilitated the emergence of smart contracts: autonomous programs that live and run on the blockchain. Smart contracts have seen a rapid climb to prominence, with applications predicted in law, business, commerce, and governance. Smart contracts are commonly written in a high-level language such as Ethereum's Solidity, and translated to compact low-level bytecode for deployment on the blockchain. Once deployed, the bytecode is autonomously executed, usually by a %Turing-complete virtual machine. As with all programs, smart contracts can be highly vulnerable to malicious attacks due to deficient programming methodologies, languages, and toolchains, including buggy compilers. At the same time, smart contracts are also high-value targets, often commanding large amounts of cryptocurrency. Hence, developers and auditors need security frameworks capable of analysing low-level bytecode to detect potential security vulnerabilities. In this paper, we present Vandal: a security analysis framework for Ethereum smart contracts. Vandal consists of an analysis pipeline that converts low-level Ethereum Virtual Machine (EVM) bytecode to semantic logic relations. Users of the framework can express security analyses in a declarative fashion: a security analysis is expressed in a logic specification written in the \souffle language. We conduct a large-scale empirical study for a set of common smart contract security vulnerabilities, and show the effectiveness and efficiency of Vandal. Vandal is both fast and robust, successfully analysing over 95\% of all 141k unique contracts with an average runtime of 4.15 seconds; outperforming the current state of the art tools---Oyente, EthIR, Mythril, and Rattle---under equivalent conditions.
Florentin Guth, Valentin Wüstholz, Maria Christakis, Péter Müller
Smart contracts are programs that manage digital assets according to a certain protocol, expressing for instance the rules of an auction. Understanding the possible behaviors of a smart contract is difficult, which complicates development, auditing, and the post-mortem analysis of attacks. This paper presents the first specification mining technique for smart contracts. Our technique extracts the possible behaviors of smart contracts from contract executions recorded on a blockchain and expresses them as finite automata. A novel dependency analysis allows us to separate independent interactions with a contract. Our technique tunes the abstractions for the automata construction automatically based on configurable metrics, for instance, to maximize readability or precision. We implemented our technique for the Ethereum blockchain and evaluated its usability on several real-world contracts.
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Yaron Velner
Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payoff games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions.
Bitcoin has attracted everyone's attention and interest recently. Ethereum (ETH), a second generation cryptocurrency, extends Bitcoin's design by offering a Turing-complete programming language called Solidity to develop smart contracts. Smart contracts allow creditable execution of contracts on EVM (Ethereum Virtual Machine) without third parties. Developing correct smart contracts is challenging due to its decentralized computation nature. Buggy smart contracts may lead to huge financial loss. Furthermore, smart contracts are very hard, if not impossible, to patch once they are deployed. Thus, there is a recent surge of interest on analyzing/verifying smart contracts. While existing work focuses on EVM opcode, we argue that it is equally important to understand and define the semantics of Solidity since programmers program and reason about smart contracts at the level of source code. In this work, we develop the structural operational semantics for Solidity, which allows us to identify multiple design issues which underlines many problematic smart contracts. Furthermore, our semantics is executable in the K framework, which allows us to verify/falsify contracts automatically.
This article presents the formal syntax and semantics for a large subset of the Solidity programming language developed for the Etheruem blockchain platform based on our resent work about developing a general, extensible, and reusable formal memory (GERM) framework and an extension of Curry-Howard isomorphism, denoted as execution-verification isomorphism (EVI). This subset is denoted as Lolisa, which, to our knowledge, is the first mechanized and validated formal syntax and semantics developed for Solidity. The formal syntax of Lolisa adopts a stronger static type system than Solidity for enhanced type safety. In addition, Lolisa not only includes nearly all the syntax components of Solidity, such as mapping, modifier, contract, and address types, but it also contains general-purpose programming language features, such as multiple return values, pointer arithmetic, struct, and field access. Therefore, the inherent compatibility of Lolisa allows Solidity programs to be directly translated into Lolisa with a line-by-line correspondence without rebuilding or abstracting, and, in addition, the inherent generality of Lolisa allows it to be extended to express other programming languages as well. To this end, we also present a preliminary scheme for extending Lolisa to other languages systematically.
In recent years, a number of lightweight programs have been deployed in critical domains, such as in smart contracts based on blockchain technology. Therefore, the security and reliability of such programs should be guaranteed by the most credible technology. Higher-order logic theorem proving is one of the most reliable technologies for verifying the properties of programs. However, programs may be developed by different high-level programming languages, and a general, extensible, and reusable formal memory (GERM) framework that can simultaneously support different formal verification specifications, particularly at the code level, is presently unavailable for verifying the properties of programs. Therefore, the present work proposes a GERM framework to fill this gap. The framework simulates physical memory hardware structure, including a low-level formal memory space, and provides a set of simple, nonintrusive application programming interfaces and assistant tools using Coq that can support different formal verification specifications simultaneously. The proposed GERM framework is independent and customizable, and was verified entirely in Coq. We also present an extension of Curry-Howard isomorphism, denoted as execution-verification isomorphism (EVI), which combines symbolic execution and theorem proving for increasing the degree of automation in higher-order logic theorem proving assistant tools. We also implement a toy functional programming language in a generalized algebraic datatypes style and a formal interpreter in Coq based on the GERM framework. These implementations are then employed to demonstrate the application of EVI to a simple code segment.
Reasoning about commutativity between data-structure operations is an important problem with applications including parallelizing compilers, optimistic parallelization and, more recently, Ethereum smart contracts. There have been research results on automatic generation of commutativity conditions, yet we are unaware of any fully automated technique to generate conditions that are both sound and effective. We have designed such a technique, driven by an algorithm that iteratively refines a conservative approximation of the commutativity (and non-commutativity) condition for a pair of methods into an increasingly precise version. The algorithm terminates if/when the entire state space has been considered, and can be aborted at any time to obtain a partial yet sound commutativity condition. We have generalized our work to left-/right-movers and proved relative completeness. We describe aspects of our technique that lead to useful commutativity conditions, including how predicates are selected during refinement and heuristics that impact the output shape of the condition. We have implemented our technique in a prototype open-source tool Servois. Our algorithm produces quantifier-free queries that are dispatched to a back-end SMT solver. We evaluate Servois through two case studies: (i) We synthesize commutativity conditions for a range of data structures including Set, HashTable, Accumulator, Counter, and Stack. (ii) We consider an Ethereum smart contract called BlockKing, and show that Servois can detect serious concurrency-related vulnerabilities and guide developers to construct robust and efficient implementations.
This paper outlines key design principles of Scilla---an intermediate-level language for verified smart contracts. Scilla provides a clean separation between the communication aspect of smart contracts on a blockchain, allowing for the rich interaction patterns, and a programming component, which enjoys principled semantics and is amenable to formal verification. Scilla is not meant to be a high-level programming language, and we are going to use it as a translation target for high-level languages, such as Solidity, for performing program analysis and verification, before further compilation to an executable bytecode. We describe the automata-based model of Scilla, present its programming component and show how contract definitions in terms of automata streamline the process of mechanised verification of their safety and temporal properties.
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Yaron Velner
Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i)~a simplified programming language for smart contracts; (ii)~an automatic translation of the programs to state-based games; (iii)~an abstraction-refinement approach to solve such games; and (iv)~experimental results on real-world-inspired smart contracts.