Benjamin Mariano, Yanju Chen, Yu Feng, Shuvendu K. Lahiri · 5 authors
This paper aims to shed light on how loops are used in smart contracts. Towards this goal, we study various syntactic and semantic characteristics of loops used in over 20,000 Solidity contracts deployed on the Ethereum blockchain, with the goal of informing future research on program analysis for smart contracts. Based on our findings, we propose a small domain-specific language (DSL) that can be used to summarize common looping patterns in Solidity. To evaluate what percentage of smart contract loops can be expressed in our proposed DSL, we also design and implement a program synthesis toolchain called Solis that can synthesize loop summaries in our DSL. Our evaluation shows that at least 56% of the analyzed loops can be summarized in our DSL, and 81% of these summaries are exactly equivalent to the original loop.
Luís Pedro Arrojado da Horta, João Santos Reis, Simão Melo de Sousa, Mário Pereira
This paper introduces a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. Our tool accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of our tool to automatically prove the correctness of diverse annotated smart contracts.
Recursive Length Prefix (RLP) is used to encode a wide variety of data in Ethereum, including transactions. The work described in this paper provides a formal specification of RLP encoding and a verified implementation of RLP decoding, developed in the ACL2 theorem prover. This work has led to improvements to the Ethereum documentation and additions to the Ethereum test suite.
Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea · 6 authors
Scilla is a higher-order polymorphic typed intermediate level language for implementing smart contracts. In this talk, we describe a Scilla compiler targeting LLVM, with a focus on mapping Scilla types, values, and its functional language constructs to LLVM-IR. The compiled LLVM-IR, when executed with LLVM's JIT framework, achieves a speedup of about 10x over the reference interpreter on a typical Scilla contract. This reduced latency is crucial in the setting of blockchains, where smart contracts are executed as parts of transactions, to achieve peak transactions processed per second. Experiments on the Ackermann function achieved a speedup of more than 45x. This talk abstract is aimed at both programming language researchers looking to implement an LLVM based compiler for their functional language, as well as at LLVM practitioners.
Abstract We condense the theory of UTxO blockchains down to a simple and compact set of four type equations (Idealised EUTxO), and to an algebraic characterisation (abstract chunk systems), and exhibit an adjoint pair of functors between them. This gives a novel account of the essential mathematical structures underlying blockchain technology, such as Bitcoin.
José Eduardo de Azevedo Sousa, Vinícius Cunha Oliveira, Júlia Almeida Valadares, Glauber Dias Gonçalves · 7 authors
Summary Ethereum is a new blockchain‐based platform that is also capable of running smart contracts. Despite its increasing popularity, there is a lack of studies on characterizing this system, in special the fees paid by users and the respective delay to confirm the transactions, that is, the pending time . In this sense, we study the main features of Ethereum transactions and evaluate the common belief—for blockchain systems that rely on proof of work—that users who pay higher fees will have their transactions confirmed faster. Specifically, we collect information about 7.2 million of transactions in Ethereum and correlate their pending time to several fee‐related features. Moreover, we conduct our study evaluating different ranges of values for the features, such as default and unusual values adopted by users as well as clusters of users with similar behaviors. Our empirical analysis shows strong evidence that there is no clear correlation between fees‐related features and the pending time. Overall, we conclude from our investigation that transaction's features, including gas and gas price defined by users, cannot determine the pending time of transactions.
La tecnologia blockchain nasce nel 2008 con l’annuncio di BitCoin [1], una delle più diffuse criptovalute. Il ruolo fondamentale della blockchain nell’ambito delle criptovalute è quello di garantire l’impossibilità di spendere due volte lo stesso valore in transazioni successive, fattispecie che viene indicata nel mondo anglosassone come double spending. Il problema del double spending è di difficile soluzione quando l’informazione di un valore è espressa in formato digitale, il quale ben si presta alla riproduzione di copie identiche consentendo quindi di spendere quel valore più volte. Il problema è superabile in presenza di una entità centralizzata fidata, quale ad esempio una banca, ma nei casi in cui tale intermediario non è disponibile o non ne è auspicabile la presenza, allora è necessario utilizzare altre modalità. Nell’ambito delle criptovalute, la blockchain risolve il problema attraverso un sistema distribuito in cui la verifica formale della validità della transazione finanziaria non viene affidata ad un intermediario ma viene svolta da un sistema distribuito, costituito da vari nodi gestiti in modo indipendente, i quali devono raggiungere un consenso, cioè una visione unitaria sullo stato dell’intero sistema. La blockchain consente di gestire dati in modo trasparente, immutabile, fidato e tracciabile. La trasparenza è garantita dal fatto che le informazioni in essa contenute siano messe a disposizione dei vari attori coinvolti. L’immutabilità della blockchain è dovuta alla sua struttura dati, una volta inserito il blocco non può più essere modificato. La fiducia è dovuta al fatto che la blockchain si basa su evidenze crittografiche piuttosto che nella fiducia in una entità centralizzata ed elimina pertanto la necessità di intermediari fidati. Ad esempio, in una transazione finanziaria in cui Antonio (A) vuole dare un certo importo a Benedetta (B), le parti si rivolgono alla banca, la quale decrementa il saldo del conto di A dell’importo da trasferire ed incrementa il saldo di B della medesima quantità. A e B si fidano entrambi della banca e non hanno alcuna possibilità di intervento qualora la banca commetta un errore nell’eseguire la transazione. Utilizzando la blockchain non è invece necessario avere fiducia nella banca e A e B possono effettuare una transazione anche se non si fidano tra loro. La tracciabilità è dovuta al fatto che nella blockchain non è possibile eliminare le informazioni inserite ma soltanto aggiungerne di nuove in coda, pertanto viene mantenuto lo storico delle informazioni. Inoltre, la blockchain è più efficiente laddove la sua introduzione non richiede più l’azione di intermediari, eliminando i costi ad essi associati. A seconda della tipologia di blockchain, questa può essere accessibile da chiunque in lettura (blockchain pubbliche) o da particolari entità preventivamente identificate (blockchain private). Perché un nodo possa scrivere sulla blockchain è necessario che esso giunga ad un consenso con gli altri nodi. Se i nodi che devono raggiungere il consenso sono appartenenti ad un gruppo chiuso e predefinito allora si dice che la blockchain è di tipo permissioned, in quanto solo chi ha i permessi può partecipare alla competizione interna tra i nodi per scrivere dati. Le blockchain permissionless, invece, non necessitano di alcuna identificazione preventiva.
Developing compiler optimizations, especially for new, rapidly evolving smart contract languages, can be onerous and error-prone, but is especially important for smart contracts, where deployment and execution directly translate to monetary cost and which cannot change once deployed. One common optimization technique is the use of peephole optimizations, replacement rules that are applied using pattern-matching. These rules are normally constructed using human expertise, which is both time-consuming and far from systematic in exploring opportunities for optimization. In this work we propose a pipeline to automatically populate the peephole optimizer of a smart contract compiler. We apply superoptimization to an existing code base to obtain sequences of instructions, which can be replaced by cheaper, observationally equivalent instructions. We then generate peephole optimization rules by extracting the underlying patterns of these optimizations. We provide a case study of our approach and a prototype implementation for bytecode of the Ethereum Virtual Machine, the tool ppltr, which combines the superoptimizer ebso and the rule generator sorg. Then we evaluate our approach by generating and applying nearly 1k peephole optimization rules extracted from 2k optimizations obtained from deployed bytecode.
Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. This article gives an overview of efforts using the Coq proof assistant to have stronger guarantees on Michelson smart contracts: the Mi-Cho-Coq framework, a Coq library defining formal semantics of Michelson, as well as an interpreter, a simple optimiser and a weakest-precondition calculus to reason about Michelson smart contracts; Albert, an intermediate language that abstracts Michelson stacks with a compiler written in Coq that targets Mi-Cho-Coq.
Muhammed F. Esgin, Ngoc Khanh Nguyen, Gregor Seiler
We propose a very fast lattice-based zero-knowledge proof system for exactly proving knowledge of a ternary solution \(\vec {s} \in \{-1,0,1\}^n\) to a linear equation \(A\vec {s}=\vec {u}\) over \(\mathbb {Z}_q\), which improves upon the protocol by Bootle, Lyubashevsky and Seiler (CRYPTO 2019) by producing proofs that are shorter by a factor of 8.
The rise of programmable open distributed consensus platforms based on the blockchain technology has aroused a lot of interest in replicated stateful computations, aka smart contracts. As blockchains are used predominantly in financial applications, smart contracts frequently manage millions of dollars worth of virtual coins. Since smart contracts cannot be updated once deployed, the ability to reason about their correctness becomes a critical task. Yet, the de facto implementation standard, pioneered by the Ethereum platform, dictates smart contracts to be deployed in a low-level language, which renders independent audit and formal verification of deployed code infeasible in practice. We report an ongoing experiment held with an industrial blockchain vendor on designing, evaluating, and deploying Scilla, a new programming language for safe smart contracts. Scilla is positioned as an intermediate-level language, suitable to serve as a compilation target and also as an independent programming framework. Taking System F as a foundational calculus, Scilla offers strong safety guarantees by means of type soundness. It provides a clean separation between pure computational, state-manipulating, and communication aspects of smart contracts, avoiding many known pitfalls due to execution in a byzantine environment. We describe the motivation, design principles, and semantics of Scilla, and we report on Scilla use cases provided by the developer community. Finally, we present a framework for lightweight verification of Scilla programs, and showcase it with two domain-specific analyses on a suite of real-world use cases.
Kakuro is a popular logic puzzle, in which a player fills in all empty squares with digits from 1 to 9 so that the sum of digits in each (horizontal or vertical) line is equal to a given number, called a clue, and digits in each line are all different. In 2016, Bultel, Dreier, Dumas, and Lafourcade proposed a physical zero-knowledge proof protocol for Kakuro using a deck of cards; their proposed protocol enables a prover to convince a verifier that the prover knows the solution of a Kakuro puzzle without revealing any information about the solution. One possible drawback of their protocol would be that the protocol is not perfectly extractable, implying that a prover who does not know the solution can convince a verifier with a small probability; therefore, one has to repeat the protocol to make such an error become negligible. In this paper, to overcome this, we design zero-knowledge proof protocols for Kakuro having perfect extractability property. Our improvement relies on the ideas behind the copy protocols in the field of card-based cryptography. By executing our protocols with a real deck of physical playing cards, humans can practically perform an efficient zero-knowledge proof of knowledge for Kakuro.
We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort.
Bojan Marinković, Paola Glavan, Zoran Ognjanović, Thomas Studer
Abstract In this paper we provide a strongly complete axiomatization of a temporal epistemic logic in which non-rigid sets of agents are allowed. Using this framework, we prove a number of properties of the blockchain protocol with respect to the given set of axioms and premises.
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 study the problem of approximating the commuting-operator value of a two-player non-local game. It is well-known that it is $\mathrm{NP}$-complete to decide whether the classical value of a non-local game is 1 or $1- ε$. Furthermore, as long as $ε$ is small enough, this result does not depend on the gap $ε$. In contrast, a recent result of Fitzsimons, Ji, Vidick, and Yuen shows that the complexity of computing the quantum value grows without bound as the gap $ε$ decreases. In this paper, we show that this also holds for the commuting-operator value of a game. Specifically, in the language of multi-prover interactive proofs, we show that the power of $\mathrm{MIP}^{co}(2,1,1,s)$ (proofs with two provers, one round, completeness probability $1$, soundness probability $s$, and commuting-operator strategies) can increase without bound as the gap $1-s$ gets arbitrarily small. Our results also extend naturally in two ways, to perfect zero-knowledge protocols, and to lower bounds on the complexity of computing the approximately-commuting value of a game. Thus we get lower bounds on the complexity class $\mathrm{PZK}$-$\mathrm{MIP}^{co}_δ(2,1,1,s)$ of perfect zero-knowledge multi-prover proofs with approximately-commuting operator strategies, as the gap $1-s$ gets arbitrarily small. While we do not know any computable time upper bound on the class $\mathrm{MIP}^{co}$, a result of the first author and Vidick shows that for $s = 1-1/\text{poly}(f(n))$ and $δ= 1/\text{poly}(f(n))$, the class $\mathrm{MIP}^{co}_δ(2,1,1,s)$, with constant communication from the provers, is contained in $\mathrm{TIME}(\exp(\text{poly}(f(n))))$. We give a lower bound of $\mathrm{coNTIME}(f(n))$ (ignoring constants inside the function) for this class, which is tight up to polynomial factors assuming the exponential time hypothesis.
Prabhanjan Ananth, Apoorvaa Deshpande, Yael Tauman Kalai, Anna Lysyanskaya
In this work, we define and construct fully homomorphic non-interactive zero knowledge (FH-NIZK) and non-interactive witness-indistinguishable (FH-NIWI) proof systems.
This paper introduces Spartan, a new family of zero-knowledge succinct non-interactive arguments of knowledge (zkSNARKs) for the rank-1 constraint satisfiability (R1CS), an NP-complete language that generalizes arithmetic circuit satisfiability. A distinctive feature of Spartan is that it offers the first zkSNARKs without trusted setup (i.e., transparent zkSNARKs) for NP where verifying a proof incurs sub-linear costs—without requiring uniformity in the NP statement’s structure. Furthermore, Spartan offers zkSNARKs with a time-optimal prover, a property that has remained elusive for nearly all zkSNARKs in the literature.