Blockchain Papers

Fan Zhang, Philip Daian, Iddo Bentov, Ari Juels

No abstract is available for this record.

Weiqi Dai, Jun Deng, Qinyuan Wang, Changze Cui · 6 authors

Due to the increasing total value of the digital currency, the security of encryption wallet is becoming more and more important. The hardware-based wallet is safe, but it is inconvenient because users need to carry an additional physical device, the software-based wallet is convenient, but the safety cannot be guaranteed. All these wallets need to synchronize the blockchain, while most current mobile devices do not have the capability to store all blocks. To solve these problems, mobile devices can use simplified payment verification (SPV). Nevertheless, in existing methods, there is no good way to protect the verification process of the transaction. In this paper, we design a secure blockchain lightweight wallet based on Trustzone to protect SPV. It is more portable compared with the hardware wallet, and safer than the software wallet. Through the isolation, it can also protect the private key and the wallet's address from being stolen by the attackers no matter whether the Rich OS is malicious or not. Meanwhile, it can protect the verification process by verifying transactions in the secure execution environment (SEE), and keep the local block headers unreadable directly from the Rich OS through encryption. We deploy it on the RASPBERRY PI 3 MODEL B development board. The result of the experiment shows that it has little impact on the system.

Eli Ben‐Sasson, Alessandro Chiesa, Michael Riabzev, Nicholas Spooner · 6 authors

We design, implement, and evaluate a zero knowledge succinct non-interactive argument (SNARG) for Rank-1 Constraint Satisfaction (R1CS), a widely-deployed NP language undergoing standardization. Our SNARG has a transparent setup, is plausibly post-quantum secure, and uses lightweight cryptography. A proof attesting to the satisfiability of n constraints has size \(O(\log ^2 n)\); it can be produced with \(O(n \log n)\) field operations and verified with O(n). At 128 bits of security, proofs are less than \({250}\,\mathrm{kB}\) even for several million constraints, more than \(10{\times }\) shorter than prior SNARGs with similar features.

Jonathan Bootle, Jens Groth

No abstract is available for this record.

Patrick McCorry, Malte Möser, Syed Taha Ali

No abstract is available for this record.

Jonathan Bootle, Andrea Cerulli, Jens Groth, S. Jakobsen · 5 authors

No abstract is available for this record.

Jonathan Katz, Vladimir Kolesnikov, Xiao Wang

Recent work, including ZKBoo, ZKB++, and Ligero, has developed efficient non-interactive zero-knowledge proofs of knowledge (NIZKPoKs) for Boolean circuits based on symmetric-key primitives alone, using the "MPC-in-the-head" paradigm of Ishai et al. We show how to instantiate this paradigm with MPC protocols in the preprocessing model; once optimized, this results in an NIZKPoK with shorter proofs (and comparable computation) as in prior work for circuits containing roughly 300--100,000 AND~gates. In contrast to prior work, our NIZKPoK also supports witness-independent preprocessing, which allows the prover to shift most of its work to an offline phase before the witness is known. We use our NIZKPoK to construct a signature scheme based only on symmetric-key primitives (and hence with "post-quantum" security). The resulting scheme has shorter signatures than the scheme built using ZKB++ (and comparable signing/verification time), and is even competitive with hash-based signature schemes. To further highlight the flexibility and power of our NIZKPoK, we also use it to build efficient ring and group signatures based on symmetric-key primitives alone. To our knowledge, the resulting schemes are the most efficient constructions of these primitives that offer post-quantum security.

Wolfgang Ahrendt, Gordon J. Pace, Gerardo Schneider

No abstract is available for this record.

Petar Tsankov

No abstract is available for this record.

Meixun Qu, Xin Huang, Chen Xu, Yi Wang · 6 authors

No abstract is available for this record.

Christian Colombo, Joshua Ellul, Gordon J. Pace

No abstract is available for this record.

Massimo Bartoletti, Roberto Zunino

A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some funds remain frozen. The relevance of this issue is witnessed by a recent liquidity attack to the Ethereum Parity Wallet, which has frozen $${\sim }160M$$ USD within the contract, making this sum unredeemable by any user. We address the problem of verifying liquidity of Bitcoin contracts. Focussing on BitML, a contracts DSL with a computationally sound compiler to Bitcoin, we study various notions of liquidity. Our main result is that liquidity of BitML contracts is decidable, in all the proposed variants. To prove this, we first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of any given set of contracts, abstracting the context moves. With respect to the chosen contracts, this abstraction is sound and complete. Our decision procedure for liquidity is then based on model-checking the finite space of states of the abstraction.

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.

Zheng Yang, Hang Lei

In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering the standard issues surrounding reusability, consistency, and automation. A specific FSPVM, denoted as FSPVM-E, was developed in Coq based on a general, extensible, and reusable formal memory (GERM) framework, an extensible and universal formal intermediate programming language, denoted as Lolisa, which is a large subset of the Solidity programming language that uses generalized algebraic datatypes, and a corresponding formally verified interpreter for Lolisa, denoted as FEther, which serves as a crucial component of FSPVM-E. However, our past work has demonstrated that the execution efficiency of the standard development of FEther is extremely low. As a result, FSPVM-E fails to achieve its expected verification effect. The present work addresses this issue by first identifying three root causes of the low execution efficiency of formal interpreters. We then build abstract models of these causes, and present respective optimization schemes for rectifying the identified conditions. Finally, we apply these optimization schemes to FEther, and demonstrate that its execution efficiency has been improved significantly.

Waqas Mahmood, Abdul Wahab

Distributed ledger technology has gained wide popularity and adoption since the emergence of bitcoin in 2008 which is based on proof of work (PoW). It is a distributed, transparent and immutable database of records of all the transactions or events that have been shared and executed among the participants. All the transactions are verified and maintained by multiple nodes across a network without a central authority through a distributed cryptographic mechanism, a consensus protocol. It forms the core of this technology that not only validates the information appended to the ledger but also ensures the order in which it is appended across all the nodes. It is the foundation of its security, accountability and trust. While many researchers are working on improving the current protocol to be quantum resistant, fault-tolerant, and energy-efficient. Others are focused on developing different variants of the protocol, best suited for specific use cases. In this paper, we shall review different consensus protocols of distributed ledger technologies and their implementations. We shall also review their properties, concept and similar-work followed by a brief analysis.

Ivan Damgård, Ji Luo, Sabine Oechsner, Peter Schöll · 5 authors

No abstract is available for this record.

Jonathan Bootle, Andrea Cerulli, Jens Groth, S. Jakobsen · 5 authors

No abstract is available for this record.

Ilya Sergey, Amrit Kumar, Aquinas Hobor

No abstract is available for this record.

Xueping Liang, Sachin Shetty, Deepak K. Tosh, Peter Foytik · 5 authors

No abstract is available for this record.

Andrew Miller, Zhicheng Cai, Somesh Jha

No abstract is available for this record.

Shaun Azzopardi, Joshua Ellul, Gordon J. Pace

No abstract is available for this record.

Leonardo Alt, Christian Reitwießner

No abstract is available for this record.

Anastasia Mavridou, Áron Lászka

Blockchain-based distributed computing platforms enable the trusted execution of computation - defined in the form of smart contracts - without trusted agents. Smart contracts are envisioned to have a variety of applications, ranging from financial to IoT asset tracking. Unfortunately, the development of smart contracts has proven to be extremely error prone. In practice, contracts are riddled with security vulnerabilities comprising a critical issue since bugs are by design non-fixable and contracts may handle financial assets of significant value. To facilitate the development of secure smart contracts, we have created the FSolidM framework, which allows developers to define contracts as finite state machines (FSMs) with rigorous and clear semantics. FSolidM provides an easy-to-use graphical editor for specifying FSMs, a code generator for creating Ethereum smart contracts, and a set of plugins that developers may add to their FSMs to enhance security and functionality.

Stephan Haarmann, Kimon Batoulis, Adriatik Nikaj, Mathias Weske

No abstract is available for this record.