Blockchain Papers

Mahsa Moosavi, Jeremy Clark

No abstract is available for this record.

Jiao Jiao

The success of Bitcoin since 2009 stimulates the development of other blockchain-based applications, such as Ethereum, a second generation of cryptocurrency which supports the revolutionary idea of smart contracts. An Ethereum smart contract is a computer program written in some domain-specific high-level programming languages, such as Solidity, Vyper, Bamboo, Flint, etc., and stored on the blockchain to achieve certain functionality. Smart contracts benefit from the features of the blockchain in various aspects. For instance, it is not necessary to have an external trusted authority to achieve consensus, and transactions through smart contracts are always traceable and credible. Smart contracts must be verified for multiple reasons. Firstly, due to the decentralized nature of the blockchain, smart contracts are different from programs written in other programming languages (e.g., C/Java). For instance, the storage of each contract instance is located at a permanent address on the blockchain. In this way, each contract instance is a particular execution context and context switches are possible through external calls. Particularly, in Solidity, delegatecall is executed in the context of the caller rather than the recipient, making it possible to modify the state of the caller. Programmers must be aware of the execution context of each statement to guarantee the programming correctness. Therefore, programming smart contracts is error-prone without a proper understanding of the underlying semantic model. Secondly, a smart contract can be deployed on the blockchain by any user in the network. Vulnerabilities in deployed contracts can be exploited to launch attacks that lead to huge financial loss. Verifying smart contracts against such vulnerabilities is crucial for protecting digital assets. One famous attack on smart contracts is the DAO attack in which the attacker exploited the reentrancy vulnerability and managed to take 60 million dollars under his/her control. Finally, it is very difficult, if not impossible, to patch a smart contract once it is deployed due to the very nature of the blockchain. There is a surge of interest in analyzing and verifying smart contracts. To the best of our knowledge, most of the existing approaches either focus on EVM (Ethereum Virtual Machine) bytecode, or translate Solidity smart contracts into programs in intermediate languages that are suitable for verifying smart contracts or detecting potential issues in associated verifiers or checkers. Furthermore, none of the existing works can directly handle smart contracts written in different high-level programming languages without translating them into EVM bytecode or intermediate languages. None of the existing approaches defines security properties with the high-level semantics of smart contracts. A direct executable formal semantics of the high-level smart contract programming language concerned is a must for both understanding and verifying smart contracts. Firstly, programmers write and reason about smart contracts at the level of source code without the semantics of which they are required to understand how Solidity programs are compiled into EVM bytecode in order to understand these contracts, which is far from trivial. In addition, there may be semantic gaps between high-level smart contract programming languages and low-level bytecode which are introduced by compiler bugs. In other words, after compilation the semantics of bytecode may not be equivalent to that of the corresponding high-level programs due to the compiler bugs involved. Therefore, both high-level and low-level semantics definitions are necessary to conduct equivalence checking to guarantee that security properties are preserved at both levels and reason about compiler bugs. Secondly, even though smart contracts can be transformed into programs in intermediate languages to be analyzed and verified in existing model checkers and verifiers, the equivalence checking of the high-level smart contract programming language concerned and the intermediate language applied to interpret it is crucial to the validity of the verification. We develop an executable operational semantics for the Solidity programming language to formally reason about smart contracts written in Solidity. The contributions of this work lie in four aspects. Firstly, our work is the first approach, to the best of our knowledge, to a complete executable formal semantics of Solidity constructed directly on the language itself other than Solidity compilers. The proposed executable semantics completely covers the supported high-level core features specified by the official Solidity documentation and is validated with the official compiler Remix. In addition, a new and general way of semantics formalization is applied in the semantics design, making the proposed semantics robust in the language evolution of smart contracts. Secondly, the proposed semantics provides a formal specification of smart contracts which solves the specification issues in the existing verification and analysis tools. Thirdly, the proposed semantics allows us to formally define semantic-level security properties for verifying smart contracts to exclude the false positives and negatives introduced by the existing approaches. Finally, the proposed semantics defines correct and secure high-level execution behaviours of smart contracts to reason about compiler bugs and assist developers in writing secure smart contracts. Furthermore, we develop a generalized formal semantic framework for smart contracts. The contributions of this work lie in three aspects. Firstly, our work is the first approach, to the best of our knowledge, to a generalized formal semantic framework for smart contracts which can directly handle contracts written in different high-level programming languages. Secondly, a general semantic model of smart contracts is constructed with rewriting logic in the K-framework. With the general semantic model, a direct executable formal semantics of a particular high-level smart contract programming language can be constructed as long as its core features fall into the ones defined in this model. The general semantic model is validated with its interpretation in Solidity using the Solidity compiler test set and evaluation results show that it is complete and correct. Lastly, the generated semantics facilitates the formal verification of smart contracts written in a particular high-level programming language as a formal specification of the corresponding language. Together with low-level specifications, it allows us to conduct equivalence checking on high-level contracts and low-level bytecode to reason about compiler bugs and guarantee that security properties are preserved at both levels. We define some security properties based on the formal semantics of the high-level smart contract programming languages. These security properties are defined from a general point of view and can be applied to detect a variety of vulnerabilities in smart contracts, such as the reentrancy vulnerability, exception disorders, integer underflows and overflows, etc. In addition, verification algorithms for these properties are constructed with the proposed semantic framework. We compare our approaches to the security analysis of smart contracts with the existing ones and highlight the importance of precise semantic foundations for the verification of smart contracts. Lastly, we systematize the existing approaches to the security analysis of smart contracts from the perspectives of domain-specific research and applications of general ideas to study the connection between the domain-specific issues in smart contracts and general analysis techniques. To conclude, this thesis studies the formal specification and verification of smart contracts, and combines domain-specific analysis and applications of general techniques. It also motivates other research directions related to the security analysis of smart contracts, such as the equivalence checking of high-level contracts and low-level bytecode, formal reasoning of high-level smart contract programming languages, the fairness analysis of smart contracts, etc.

Behzad Abdolmaleki, Daniel Slamanig

Recently, motivated by its increased use in real-world applications, there has been a growing interest on the reduction of trust in the generation of the common reference string (CRS) for zero-knowledge (ZK) proofs. This line of research was initiated by the introduction of subversion non-interactive ZK (NIZK) proofs by Bellare et al. (ASIACRYPT’16). Here, the zero-knowledge property needs to hold even in case of a malicious generation of the CRS. Groth et al. (CRYPTO’18) then introduced the notion of updatable zk-SNARKS, later adopted by Lipmaa (SCN’20) to updatable quasi-adaptive NIZK (QA-NIZK) proofs. In contrast to the subversion setting, in the updatable setting one can achieve stronger soundness guarantees at the cost of reintroducing some trust, resulting in a model in between the fully trusted CRS generation and the subversion setting. It is a promising concept, but all previous updatable constructions are ad-hoc and tailored to particular instances of proof systems. Consequently, it is an interesting question whether it is possible to construct updatable ZK primitives in a more modular way from simpler building blocks.

Lior Rotem, Gil Segev

No abstract is available for this record.

Shaun Azzopardi, Joshua Ellul, Gordon J. Pace

No abstract is available for this record.

Karim Baghery, Cyprien Delpech de Saint Guilhem, Emmanuela Orsini, Nigel P. Smart · 5 authors

This paper introduces M-Circuits, a program representation which generalizes arithmetic and binary circuits. This new representation is motivated by the way modern multi-party computation (MPC) systems based on linear secret sharing schemes actually operate. We then show how this representation also allows one to construct zero knowledge proof (ZKP) systems based on the MPC-in-the-head paradigm. The use of the M-Circuit program abstraction then allows for a number of program-specific optimizations to be applied generically. It also allows to separate complexity and security optimizations for program compilation from those for application protocols (MPC or ZKP).

Vladimir Kukharenko, Kirill Ziborov, Rafael Faritovich Sadykov, Ruslan Rezin

The extent of formal verification methods applied in industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain , is rapidly changing the situation. Since the main area of DLSs’ application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is largely determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is also required to ensure that the software implementation of the DLS nodes complies with this protocol. Finally, the verified software implementation of the protocol must run on a fairly reliable operating system. The financial focus of DLS application has also led to the emergence of the so-called smart contracts , which are an important part of the applied implementations of specific business processes based on DLSs. Therefore, the verifiability of smart contracts is also a critical requirement for industrial DLSs. In this paper, we describe an ongoing industrial project between a large Russian airline and three universities – Innopolis University (IU), Moscow Institute of Physics and Technology (MIPT) and Lomonosov Moscow State University (MSU). The main expected project result is a DLS for more flexible refueling of aircrafts, verified at least at the four technological levels described above. After brief project overview, we focus on our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes. The formal specification of the protocol is performed in the TLA+ language and then verified with a specialized TLC tool to verify models based on TLA+ specifications.

Bingsheng Zhang, Yuan Chen, Jiaqi Li, Yajin Zhou · 7 authors

No abstract is available for this record.

François Garillot, Yashvanth Kondi, Payman Mohassel, Valeria Nikolaenko

No abstract is available for this record.

Ashrujit Ghoshal, Stefano Tessaro

No abstract is available for this record.

Silvio Šimunić, Dalen Bernaca, Kristijan Lenac

From weak clients outsourcing computational tasks to more powerful machines, to distributed blockchain nodes needing to agree on the state of the ledger in the presence of adversarial nodes, there is a growing need to efficiently verify the results of computations delegated to untrusted third parties. Verifiable computing is a new and interesting research area that addresses this problem. Recently, new applications of verifiable computing techniques have emerged in blockchain technology for secure key management, sybil-resistance and distributed consensus, and smart contracts, while providing desired performance and privacy guarantees. In this paper, we provide an overview of common methods for verifying computation and present how they are applied to blockchain technology. We group the presented verifiable computing applications into five main application areas, i.e., multiparty approval for secure key management, sybil-resistance and consensus, smart contracts and oracles, scalability, and privacy. The main contribution of this survey is to answer two research questions: 1) what are the main application areas of verifiable computing in blockchain technology, and 2) how are verifiable computing techniques used in major blockchain projects today.

Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács · 5 authors

Abstract Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer programs that operate over them, e.g., in Solidity. The ability to reason about sums is essential: even the simplest ERC-20 token standard of the Ethereum community provides a way to access the total supply of balances. Unfortunately, reasoning about code written against this interface is non-trivial: the number of addresses is unbounded, and establishing global invariants like the preservation of the sum of the balances by operations like transfer requires higher-order reasoning. In particular, automated reasoners do not provide ways to specify summations of arbitrary length. In this paper, we present a generalization of first-order logic which can express the unbounded sum of balances. We prove the decidablity of one of our extensions and the undecidability of a slightly richer one. We introduce first-order encodings to automate reasoning over software transitions with summations. We demonstrate the applicability of our results by using SMT solvers and first-order provers for validating the correctness of common transitions in smart contracts.

Franck Cassez

The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.

Jonathan Heiss, Anselm Busse, Stefan Tai

Prior to provisioning sensor data to smart contracts, a pre-processing of the data on intermediate off-chain nodes is often necessary. When doing so, originally constructed cryptographic signatures cannot be verified on-chain anymore. This exposes an opportunity for undetected manipulation and presents a problem for applications in the Internet of Things where trustworthy sensor data is required on-chain. In this paper, we propose trustworthy pre-processing as enabler for end-to-end sensor data integrity in data on-chaining workflows. We define requirements for trustworthy pre-processing, present a model and common workflow for data on-chaining, select off-chain computation utilizing Zero-knowledge Proofs (ZKPs) and Trusted Execution Environments (TEEs) as promising solution approaches, and discuss both our proof-of-concept implementations and initial experimental, comparative evaluation results. The importance of trustworthy pre-processing and principle solution approaches are presented, addressing the major problem of end-to-end sensor data integrity in blockchain-based IoT applications.

Yi Deng, Shunli Ma, Xinxuan Zhang, Hailong Wang · 6 authors

No abstract is available for this record.

Bo Gao, Ling Shi, Jiaying Li, Jialiang Chang · 6 authors

No abstract is available for this record.

Hongrui Cui, Kaiyi Zhang

No abstract is available for this record.

Luca Olivieri, Fausto Spoto, Fabio Tagliaferro

No abstract is available for this record.

Ikram Garfatta, Kaïs Klai, Mohamed Graïet, Walid Gaaloul

No abstract is available for this record.

Geoffroy Couteau, Michael Klooß, Huang Lin, Michael Reichle

No abstract is available for this record.

Zhufeng Ye, Zhenghao Wu, Xianglan Tian

Privacy-preservation and effective auditing are two desirable but challenging requirements on distributed ledgers. To meet the requirements, this paper presents an auditing scheme, called as AudiTEE, which can audit a distributed ledger in a generic, efficient, and privacy-preserving manner. AudiTEE leverages Trusted Execution Environment (TEE) to generate confidential but auditable transactions and realize arbitrary, efficient and confidential audit on them. Unfortunately, TEE suffers from some inherent barriers and is itself not a complete solution for fast audit. To tackle these challenges, AudiTEE takes advantage of KAMT (K-anonymity Authentication Based on Merkle Tree) protocol for efficient management on account and user-defined anonymous transactions. Further, to achieve a complete and fast audit with unlinkability, TEE doesn’t process through all but only a comparatively small part of transactions according to a special ktag attached on each transaction to ensure that a user cannot hide transactions from auditor even when auditor is blind with who is involved in each transaction on the ledger. Apart from the above, AudiTEE allows flexible control on user behaviors. We implement a concrete instance of AudiTEE under a bank setting and demonstrate the scalability with all its core functionalities.

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler · 6 authors

No abstract is available for this record.

Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata · 7 authors

Abstract A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This tool paper describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.

Yuichiro Chinen, Naoto Yanai, Jason Paul Cruz, Shingo Okamura

Ethereum smart contracts are programs that are deployed and executed in a consensus-based blockchain managed by a peer-to-peer network. Several re-entrancy attacks that aim to steal Ether, the cryptocurrency used in Ethereum, stored in deployed smart contracts have been found in the recent years. A countermeasure to such attacks is based on dynamic analysis that executes the smart contracts themselves, but it requires the spending of Ether and knowledge of attack patterns for analysis in advance. In this paper, we present a static analysis tool named RA (Re-entrancy Analyzer), a combination of symbolic execution and equivalence checking by a satisfiability modulo theories solver to analyze vulnerability of smart contracts to re-entrancy attacks. In contrast to existing tools, RA supports analysis of inter-contract behaviors by using only the Ethereum Virtual Machine bytecodes of target smart contracts, i.e., even without prior knowledge of attack patterns and without spending Ether. Furthermore, RA can verify existence of vulnerability to re-entrancy attacks without execution of smart contracts and it does not provide false positives and false negatives. We also present an implementation of RA to evaluate its performance in analyzing the vulnerability of deployed smart contracts to re-entrancy attacks and show that RA can precisely determine which smart contracts are vulnerable.