Blockchain Papers

Sean Braithwaite, Ethan Buchman, Igor Konnov, Žarko Milošević · 7 authors

No abstract is available for this record.

Shubham Sahai, Pramod Subramanyan, Rohit Sinha

Many important cryptographic primitives offer probabilistic guarantees of security that can be specified as quantitative hyperproperties; these are specifications that stipulate the existence of a certain number of traces in the system satisfying certain constraints. Verification of such hyperproperties is extremely challenging because they involve simultaneous reasoning about an unbounded number of different traces. In this paper, we introduce a technique for verification of quantitative hyperproperties based on the notion of trace enumeration relations. These relations allow us to reduce the problem of trace-counting into one of model-counting of formulas in first-order logic. We also introduce a set of inference rules for machine-checked reasoning about the number of satisfying solutions to first-order formulas (aka model counting). Putting these two components together enables semi-automated verification of quantitative hyperproperties on infinite state systems. We use our methodology to prove confidentiality of access patterns in Path ORAMs of unbounded size, soundness of a simple interactive zero-knowledge proof protocol as well as other applications of quantitative hyperproperties studied in past work.

Cosimo Laneve, Adele Veschetti

We study Nakamoto’s Bitcoin protocol that implements a distributed ledger on peer-to-peer asynchronous networks. In particular, we define a principled formal model of key participants - the miners - as stochastic processes and describe the whole system as a parallel composition of miners. We therefore compute the probability that ledgers turn into a state with more severe inconsistencies, e.g. with longer forks, under the assumptions that messages are not lost and nodes are not hostile. We also study how the presence of hostile nodes mining blocks in wrong positions impacts on the consistency of the ledgers. Our theoretical results agree with the simulations performed on a probabilistic model checker that we extended with dynamic datatypes in order to have a faithful description of miners' behaviour.

Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian · 6 authors

No abstract is available for this record.

Carsten Baum, Alex J. Malozemoff, Marc B. Rosen, Peter Schöll

No abstract is available for this record.

Carsten Baum, Alex J. Malozemoff, Marc B. Rosen, Peter Schöll

No abstract is available for this record.

Rami Khalil, Naranker Dulay

This paper introduces the PoSH Consensus protocol, a novel work-in-progress construction for achieving Sybil-resistant Nakamoto-style probabilistic consensus on the contents of a cryptocurrency ledger in a permissionless decentralized network where parties stake their hardware’s computational power towards participation in leader election. PoSH aims to establish an openly mintable cryptocurrency that eliminates the requirement for block rewards and disincentivizes mining pools.

Sarra Alqahtani, Xinchi He, Rose Gamble, Papa Mauricio

The smart contract technology has increasingly attracted the attention of different industries. However, a significant number of smart contracts deployed in practice suffer from several bugs, which enable malicious users to cause damage. The research community has shifted their focus to verifying the correctness of smart contracts using model checkers and formal verification methods. The majority of the research investigates the correctness of systems built on one smart contract. This paper proposes a verification approach for systems composed of interacting smart contracts developed and controlled by different entities. We use the NuSMV model checker and the Behavioral Interaction Priority tool to model the behaviors of smart contracts and their interactions with the aim of verifying their compliance with the systems’ functional requirements. These requirements are formalized by Linear Temporal Logic propositions. The applicability of our approach is illustrated using a case study from The American Petroleum Institute and implemented using Hyperledger Fabric.

David Heath, Vladimir Kolesnikov

Zero-knowledge (ZK) proofs (ZKP) have received wide attention, focusing on non-interactivity, short proof size, and fast verification time. We focus on the fastest total proof time, in particular for large Boolean circuits. Under this metric, Garbled Circuit (GC)-based ZKP (Jawurek et al., [JKO], CCS 2013) remained the state-of-the-art technique due to the low-constant linear scaling of computing the garbling.

Gustavo Betarte, Maximiliano Cristiá, Carlos Luna, Adrián Silveira · 5 authors

Emin Gün Sirer once said: It's clear that writing a robust, secure smart contract requires extreme amounts of diligence. It's more similar to writing code for a nuclear power reactor, than to writing loose web code [...] Yet the current Solidity language and underlying EVM seems designed more for the latter. Formal methods (FM) are mathematics-based software development methods aimed at producing "code for a nuclear power reactor". That is, due application of FM can produce bug-free, zero-defect, correct-by-construction, guaranteed, certified software. However, the software industry seldom use FM. One of the main reasons for such a situation is that there exists the perception (which might well be a fact) that FM increase software costs. On the other hand, FM can be partially applied thus producing high-quality software, although not necessarily bug-free. In this paper we outline some FM related techniques whose application the cryptocurrency community should take into consideration because they could bridge the gap between "loose web code" and "code for a nuclear power reactor".

Dmitrii Suvorov, Vladimir Ulyantsev

Modern blockchain systems support creation of smart contracts -- stateful programs hosted and executed on a blockchain. Smart contracts hold and transfer significant amounts of digital currency which makes them an attractive target for security attacks. It has been shown that many contracts deployed to public ledgers contain security vulnerabilities. Moreover, the design of blockchain systems does not allow the code of the smart contract to be changed after it has been deployed to the system. Therefore, it is important to guarantee the correctness of smart contracts prior to their deployment. Formal verification is widely used to check smart contracts for correctness with respect to given specification. In this work we consider program synthesis techniques in which the specification is used to generate correct-by-construction programs. We focus on one of the special cases of program synthesis where programs are modeled with finite state machines (FSMs). We show how FSM synthesis can be applied to the problem of automatic smart contract generation. Several case studies of smart contracts are outlined: crowdfunding platform, blinded auction and a license contract. For each case study we specify the corresponding smart contract with a set of formulas in linear temporal logic (LTL) and use this specification together with test scenarios to synthesize a FSM model for that contract. These models are later used to generate executable Solidity code which can be directly used in a blockchain system.

Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee · 6 authors

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.

Edward A. Lee

No abstract is available for this record.

Srinath Setty

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.

Ron van der Meyden

Blockchain systems and smart contracts provide ways to securely implement multi-party transactions without the use of trusted intermediaries, which currently underpin many commercial transactions. However, they do so by transferring trust to computer systems, raising the question of whether code can be trusted. Experience with high value losses resulting from incorrect code has already shown that formal verification of smart contracts is likely to be beneficial. This note investigates the specification and verification of a simple form of multi-party transaction, atomic swaps. It is argued that logics with the ability to express properties of strategies of players in a multi-agent setting are conceptually useful for this purpose, although ultimately, for our specific examples, the less expressive setting of temporal logic suffices for verification of concrete implementations. This is illustrated through a number of examples of the use of a model checker to verify atomic swap smart contracts in on-chain and cross-chain settings.

Zeinab Nehaï, Pierre-Yves Piriou, Frédéric Daumas

DAO attack showed that formal verification of smart contracts is an important issue that should be addressed to prevent irreversible consequences due to design faults activation in Blockchain applications. This paper proposes a modeling method of an Ethereum application based on smart contracts, with the aim of applying a formal method, namely Model-Checking, to verify that the application implementation complies with its specification, formalized by a set of temporal logic propositions. NuSMV tool has been chosen to support this first approach. The proposed model template is shaped by three layers capturing respectively the behavior of Ethereum blockchain, the smart contracts themselves and the execution framework. The approach is illustrated by a case study coming from energy market field.

Edgar González Fernández, Guillermo Morales-Luna, Feliú Sagols Troncoso

Zero-Knowledge Proofs ZKP provide a reliable option to verify that a claim is true without giving detailed information other than the answer. A classical example is provided by the ZKP based in the Graph Isomorphism problem (GI), where a prover must convince the verifier that he knows an isomorphism between two isomorphic graphs without publishing the bijection. We design a novel ZKP exploiting the NP-hard problem of finding the algebraic ideal of a multivariate polynomial set, and consequently resistant to quantum computer attacks. Since this polynomial set is obtained considering instances of GI, we guarantee that the protocol is at least as secure as the GI based protocol.

Zhangbo Duan, Hongliang Mao, Zhidong Chen, Xiaomin Bai · 6 authors

As a decentralized and distributed secure storage technology, the notion of blockchain is now widely used for electronic trading in finance, for issuing digital certificates, for copyrights management, and for many other security-critical applications. With applications in so many domains with high-assurance requirements, the formalization and verification of safety and security properties of blockchain becomes essential, and the aim of the present paper. We present the model-based formalization, simulation and verification of a blockchain protocol by using the SDL formalism of Telelogic Tau. We consider the hierarchical and modular SDL model of the blockchain protocol and exercise a methodology to formally simulate and verify it. This way, we show how to effectively increase the security and safety of blockchain in order to meet high assurance requirements demanded by its application domains. Our work also provides effective support for assessing different network consensus algorithms, which are key components in blockchain protocols, as well as on the topology of blockchain networks. In conclusion, our approach contributes to setting up a verification methodology for future blockchain standards in digital trading.

Ilya Sergey, Amrit Kumar, Aquinas Hobor

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.

Shashank Agrawal, Chaya Ganesh, Payman Mohassel

The two most common ways to design non-interactive zero-knowledge (NIZK) proofs are based on Sigma protocols and QAP-based SNARKs. The former is highly efficient for proving algebraic statements while the latter is superior for arithmetic representations.

Matteo Marescotti, Martin Blicha, Antti E. J. Hyvärinen, Sepideh Asadi · 5 authors

No abstract is available for this record.

Leonardo Alt, Christian Reitwießner

No abstract is available for this record.

Svetlana Girs, Irfan Šljivo, Omar Jaradat

Cooperation of vehicular systems is the stepping stone towards both road and indoor smart transportation systems. It aims at increasing transportation efficiency and safety compared to the stand-alone vehicular systems. The usage of wireless communication as the foundation of such safety-critical cooperation needs to be embraced with all its benefits and flaws compared to the wired communication. The cooperative functions need to be designed to adapt to the varying reliability of the wireless communication channels such that both the stand-alone vehicles as well as the smart transportation system formed by their cooperation are deemed sufficiently safe. In this paper we build upon a contract-based runtime monitoring architecture and propose a methodology for assuring adaptive behaviour of transportation with respect to the wireless communication channel failures. More specifically, we elaborate how safety analysis of the interaction of the wirelessly connected vehicles can be used as the basis for derivation of the adaptive modes and the corresponding contracts. Furthermore, we discuss how such contracts can be used as the basis for assurance of the adaptive wireless cooperation. We illustrate the proposed methodology on a smart transportation system of a factory.

Alessandro Chiesa, Michael A. Forbes, Nicholas Spooner

Many seminal results in Interactive Proofs (IPs) use algebraic techniques based on low-degree polynomials, the study of which is pervasive in theoretical computer science. Unfortunately, known methods for endowing such proofs with zero knowledge guarantees do not retain this rich algebraic structure. In this work, we develop algebraic techniques for obtaining zero knowledge variants of proof protocols in a way that leverages and preserves their algebraic structure. Our constructions achieve unconditional (perfect) zero knowledge in the Interactive Probabilistically Checkable Proof (IPCP) model of Kalai and Raz [KR08] (the prover first sends a PCP oracle, then the prover and verifier engage in an Interactive Proof in which the verifier may query the PCP). Our main result is a zero knowledge variant of the sumcheck protocol [LFKN92] in the IPCP model. The sumcheck protocol is a key building block in many IPs, including the protocol for polynomial-space computation due to Shamir [Sha92], and the protocol for parallel computation due to Goldwasser, Kalai, and Rothblum [GKR15]. A core component of our result is an algebraic commitment scheme, whose hiding property is guaranteed by algebraic query complexity lower bounds [AW09,JKRS09]. This commitment scheme can then be used to considerably strengthen our previous work [BCFGRS16] that gives a sumcheck protocol with much weaker zero knowledge guarantees, itself using algebraic techniques based on algorithms for polynomial identity testing [RS05,BW04]. We demonstrate the applicability of our techniques by deriving zero knowledge variants of well-known protocols based on algebraic techniques, including the protocols of Shamir and of Goldwasser, Kalai, and Rothblum, as well as the protocol of Babai, Fortnow, and Lund [BFL91].