The distribution of information through web protocols is today based on the client-server model. Recently, decentralized protocols with greater availability appear as well as blockchain-based attestation methods, allowing for proving the existence of information. In combination, these methods promise a secure, decentralized and long-term storage. However, there exist two major problems: (1) the scalability of blockchains limits their storage capacity and (2) various (de)centralized web protocols are in use and could alleviate this problem, but they do not support blockchain-based attestations. In this paper, we extend an approach for blockchain-based attestation with compatibility for multi-protocol storage. Instead of specific protocols or blockchains, the extended approach aims to contribute novel concepts to the discussion on blockchain scalability. It augments the capabilities of existing protocols for applications such as certification or timestamping of digital artifacts. With the use of decentralized protocols such as IPFS, further availability and inherent resilience properties are gained, allowing for applications such as open research repositories and digital registries. We discuss the architecture of the extended approach, a possible implementation in a smart contract on the Ethereum blockchain with IPFS and Git, and evaluate the time and cost of attestations.
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio
Abstract Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present $$\textsf {GASOL}^{v2}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GASOL</mml:mi> <mml:mrow> <mml:mi>v</mml:mi> <mml:mn>2</mml:mn> </mml:mrow> </mml:msup> </mml:math> , a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also wrt. memory and storage. $$\textsf {GASOL}^{v2}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GASOL</mml:mi> <mml:mrow> <mml:mi>v</mml:mi> <mml:mn>2</mml:mn> </mml:mrow> </mml:msup> </mml:math> can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler , and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas wrt. the previous version of the optimizer without memory handling, and gains of 3.28% in bytes-size over code already optimized by .
Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
We provide three detailed case studies of vulnerabilities in smart contracts, and show how property-based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave's BAT token. The last example is, in fact, new, and was missed in the auditing process. We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and Concordium's rust language. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.
Blockchains are maintained by a network of participants that run algorithms designed to maintain collectively a distributed machine tolerant to Byzantine attacks. From the point of view of users, blockchains provide the illusion of centralized computers that perform trustable verifiable computations, where all computations are deterministic and the results cannot be manipulated or undone. Smart-contracts are written in a special-purpose programming language with deterministic semantics. Each transaction begins with an invocation from an external user to a smart contract. Contracts have local storage and can call other contracts, and more importantly, they store, send and receive cryptocurrency. It is very important to guarantee that contracts are correct before deployment since their code cannot be modified afterward deployment. However, the resulting ecosystem makes it very difficult to reason about program correctness, since contracts can be executed by malicious users or malicious contracts can be designed to exploit other contracts that call them. Many attacks and bugs are caused by unexpected interactions between multiple contracts, the attacked contract and unknown code that performs the exploit. Moreover, there is a very aggressive competition between different blockchains to expand their user base. Ideas are implemented fast and blockchains compete to offer and adopt new features quickly. In this paper, we propose a formal extensible playground that allows reasoning about multi-contract interactions to ultimately prove properties before features are incorporated into the real blockchain. We implemented a model of computation that models the execution platform, abstracts the internal code of each individual contract and focuses on contract interactions. Moreover, we show how many features, existing or proposed, can be used to reason about multi-contract interactions.
Leonardo Alt, Martin Blicha, Antti E. J. Hyvärinen, Natasha Sharygina
Abstract Formally verifying smart contracts is important due to their immutable nature, usual open source licenses, and high financial incentives for exploits. Since 2019 the Ethereum Foundation’s Solidity compiler ships with a model checker. The checker, called SolCMC, has two different reasoning engines and tracks closely the development of the Solidity language. We describe SolCMC’s architecture and use from the perspective of developers of both smart contracts and tools for software verification, and show how to analyze nontrivial properties of real life contracts in a fully automated manner.
Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez · 5 authors
Abstract The most widely used Zero-Knowledge (ZK) protocols require provers to prove they know a solution to a computational problem expressed as a Rank-1 Constraint System (R1CS). An R1CS is essentially a system of non-linear arithmetic constraints over a set of signals, whose security level depends on its non-linear part only, as the linear (additive) constraints can be easily solved by an attacker. Distilling the essential constraints from an R1CS by removing the part that does not contribute to its security is important, not only to reduce costs (time and space) of producing the ZK proofs, but also to reveal to cryptographic programmers the real hardness of their proofs. In this paper, we formulate the problem of distilling constraints from an R1CS as the (hard) problem of simplifying constraints in the realm of non-linearity. To the best of our knowledge, it is the first time that constraint-based techniques developed in the context of formal methods are applied to the challenging problem of analysing and optimizing ZK protocols.
Jacco O.G. Krijnen, Manuel M. T. Chakravarty, Gabriele Keller, Wouter Swierstra
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control (valuable) assets in an adversarial environment; once committed to the blockchain, these smart contracts cannot be modified. Smart contracts are typically developed in a high-level contract language and compiled to low-level virtual machine code before being committed to the blockchain. For a smart contract user to trust a given piece of low-level code on the blockchain, they must convince themselves that (a) they are in possession of the matching source code and (b) that the compiler has correctly translated the source code to the given low-level code. Classic approaches to compiler correctness tackle the second point. We argue that translation certification also squarely addresses the first. We describe the proof architecture of a translation certification framework and demonstrate how we can model the compilation pipeline as a sequence of translation relations. We give a detailed account of such relations for most passes of the Plutus Tx compiler, which we formalised in Coq. This approach facilitates a modular verification methodology and is robust in the face of an evolving compiler implementation.
Decentralized applications (DApps) gained traction in the context of the blockchain technology. Ethereum is currently the public blockchain that backs the largest amount of the existing DApps. Onboarding new users to Ethereum DApps is a notoriously hard issue to solve. This is mainly caused by lack of cryptocurrency ownership, needed for transaction fees. Several meta-transaction patterns emerged for decoupling users from paying these fees. However, such solutions are mostly offered via off-chain, often paid relayer services and do not fully address the security issues present in the meta-transaction path. In this paper, we introduce a new meta-transaction architecture that makes use of the Intel Software Guard Extensions (SGX). Unlike other solutions, our approach would offer the possibility to deploy a fee-free Ethereum DApp on a web server that can directly relay meta-transactions to the Ethereum network while having essential security guarantees integrated by design.
Blockchains are modern distributed systems that provide decentralized financial capabilities with trustable guarantees. Smart contracts are programs written in specialized programming languages running on a blockchain and govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other contracts during the execution of transactions initiated by external users. Once deployed, smart contracts cannot be modified and their pitfalls can cause malfunctions and losses, for example by attacks from malicious users. Runtime verification is a very appealing technique to improve the reliability of smart contracts. One approach consists of specifying undesired executions (never claims) and detecting violations of the specification on the fly. This can be done by extending smart contracts with additional instructions corresponding to monitor specified properties, resulting in an onchain monitoring approach. In this paper, we study transaction monitoring that consists of detecting violations of complete transaction executions and not of individual operations within transactions. Our main contributions are to show that transaction monitoring is not possible in most blockchains and propose different execution mechanisms that would enable transaction monitoring.
We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from Dafny to EVM bytecode, the results we obtain on the Dafny code can reasonably be assumed to hold on Solidity code: the translation of the Dafny code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.