Follow blockchain research across journals, conferences, and preprint repositories.
1,684 results · page 46 of 71
Bin Yu, Xu Lu, Hao Chen, Ming Lei · 5 authors
No abstract is available for this record.
Jonathan Bootle, Vadim Lyubashevsky, Ngoc Khanh Nguyen, Gregor Seiler
No abstract is available for this record.
Dimitris Mouris, Nektarios Georgios Tsoutsos
As cloud computing becomes more popular, research has focused on usable solutions to the problem of verifiable computation (VC), where a computationally weak device (Verifier) outsources a program execution to a powerful server (Prover) and receives guarantees that the execution was performed faithfully. A Prover can further demonstrate knowledge of a secret input that causes the Verifier’s program to satisfy certain assertions, without ever revealing which input was used. State-of-the-artZero-KnowledgeProofs of Knowledge (ZKPK) methods encode a computation using arithmetic circuits and preserve the privacy of Prover’s inputs while attesting the integrity of program execution. Nevertheless, developing, debugging, and optimizing programs as circuits remains a daunting task, as most users are unfamiliar with this programming paradigm. In this work, we present Zilch, a framework that accelerates and simplifies the deployment of VC and ZKPK for any applicationtransparently, i.e., without the need of trusted setup. Zilch uses traditional instruction sequences rather than static arithmetic circuits that would need to be regenerated for each different computation. Towards that end, we have implemented Z MIPS: a MIPS-like processor model that allows verifying each instruction independently and compose a proof for the execution of the target application. To foster usability, Zilch incorporates a novel cross-compiler from an object-oriented Java-like language tailored to ZKPK and optimized our Z MIPS model, as well as a powerful API that enables integration of ZKPK within existing C/C++ programs. In our experiments, we demonstrate the flexibility of Zilch using two real-life applications, and evaluate Prover and Verifier performance on a variety of benchmarks.
Shaun Azzopardi, Christian Colombo, Gordon J. Pace
No abstract is available for this record.
Xueping Liang, Sachin Shetty, Deepak K. Tosh, Peter Foytik · 5 authors
Distributed ledger technology (DLT) provides decentralised services by removing the need of trust among distributed nodes in the distributed system. Transactions across the network are visible to a...
Leonid Merkin, Ruslan Rezin, Nikolay Konstantinovich Vasilyev
No abstract is available for this record.
Marcel Müller, Nadine Ostern, Sandro Rodriguez Garzon, Axel Küpper
No abstract is available for this record.
Palina Tolmach, Yi Li, Shang‐Wei Lin, Yang Liu
Decentralized finance (DeFi) has become one of the most successful applications of blockchain and smart contracts. The DeFi ecosystem enables a wide range of crypto-financial activities, while the underlying smart contracts often contain bugs, with many vulnerabilities arising from the unforeseen consequences of composing DeFi protocols together. In this paper, we propose a formal process-algebraic technique that models DeFi protocols in a compositional manner to allow for efficient property verification. We also conduct a case study to demonstrate the proposed approach in analyzing the composition of two interacting DeFi protocols, namely, Curve and Compound. Finally, we discuss how the proposed modeling and verification approach can be used to analyze financial and security properties of interest.
Shuichi Katsumata
Many of the recent advanced lattice-based \(\varSigma \)-/public-coin honest verifier (HVZK) interactive protocols based on the techniques developed by Lyubashevsky (Asiacrypt’09, Eurocrypt’12) can be transformed into a non-interactive zero-knowledge (NIZK) proof in the random oracle model (ROM) using the Fiat-Shamir transform. Unfortunately, although they are known to be secure in the classical ROM, existing proof techniques are incapable of proving them secure in the quantum ROM (QROM). Alternatively, while we could instead rely on the Unruh transform (Eurocrypt’15), the resulting QROM secure NIZK will incur a large overhead compared to the underlying interactive protocol.
Łukasz Mazurek
No abstract is available for this record.
V. S. Dhillon, David Metcalf, Max Hooper
Ethereum is an open source, decentralized blockchain platform with computational capabilities that reconstructs an elementary currency exchange into a transfer of value between users via a scripting language. Ethereum is widely recognized as a successor to the Bitcoin protocol, generalizing the original ideas and enabling a more diverse array of applications to be built on top of the blockchain technology. Ethereum has two essential components. First, there is a Turing-complete virtual processor that can load resources and execute scripts called the Ethereum Virtual Machine (EVM). The second component is a token of value called ether, which is the currency of the network and is used for user-to-user transactions or compensation to miners of the network. In this chapter, we begin our journey with an overview of Ethereum’s architecture in comparison to Bitcoin, focusing on the EVM and Turing-completeness properties. Following the overview of its architecture, there is a short discussion of the accounts model in Ethereum and account representation with Merkle-Patricia trees. This will lead us to the topics of global state representation in Ethereum, account storage, and gas, which is a spam prevention mechanism in the network. Then, we deconstruct the notion of a smart contract enabled by the EVM, the security concerns revolving around sandboxing executable code, and how the EVM pushes executable code (bytecode) to the blockchain. After that, we provide an introduction to Solidity and Vyper, two programming languages used for writing smart contracts in Ethereum. We explore the syntax of Solidity and Vyper, as well as the popular integrated development environments (IDEs) being used, and provide a brief list of key developer resources. Next, we focus on the world computer model proposed in Ethereum and introduce supporting decentralized technologies such as IPFS and Whisper. Then, we look at the state of decentralized apps (DApps) along the publishing platform called Mist available in Ethereum. This allows us to transition into talking about the Layer 2 updates to Ethereum—the major technical focus of this chapter and the maturation of the Ethereum ecosystem beyond 2020. Then, we will introduce the enterprise aspect of Ethereum, Blockchain-as-a-Service (BaaS) deployed on the Azure cloud by Microsoft. The chapter will conclude with an overview of recent technical proposals in Ethereum, the status of Layer 2 upgrades, and exciting changes on the horizon.
Xiangyan Tang, Ke Zhou, Jieren Cheng, Hui Li · 5 authors
No abstract is available for this record.
Jianjun Huang, Songming Han, Wei You, Wenchang Shi · 7 authors
Smart contract vulnerabilities have attracted lots of concerns due to the resultant financial losses. Matching-based detection methods extrapolating known vulnerabilities to unknown have proven to be effective in other platforms. However, directly adopting the technique to smart contracts is obstructed by two issues, i.e., diversity of bytecode generation resulting from the rapid evolution of compilers and interference of noise code easily caused by the homogeneous business logics. To address the problems, we propose contract bytecode-oriented normalization and slicing techniques to augment bytecode matching. Specifically, we conduct data- and instruction-level normalizations to uniform the bytecode generated by different compilers, and enforce contract-specific slicing by tracking data- and control-flows with simulated bytecode executions to prune the noise code as far as possible. Based on the above techniques, we design an unsupervised graph embedding algorithm to encode the code graphs into quantitatively comparable vectors. The potentially vulnerable smart contracts can be identified by measuring the similarities between their vectors and known vulnerable ones. Our evaluations have shown the efficiency (0.47 seconds per contract on average), effectiveness (160 verified true positives) and high precision (91.95% for top-ranked). It is worth noting that, we also identify dozens of honeypot contracts, further demonstrating the capability of our method.
Jesús Correas, Pablo Gordillo, Guillermo Román‐Díez
Profiling tools have been widely used for studying the behavior of the programs with the objective of reducing the amount of resources consumed by them. Most profilers collect the information with dynamic techniques, i.e., execute an instrumented version of the program with some specific input arguments to profile the measures of interest. This article presents a novel static profiling technique for Ethereum smart contracts that, using static resource analysis, is able to generate upper-bound expressions that can be used to produce profiling information about the measure of interest. Unlike traditional profiling tools, we get upper-bounds on the measures of interest expressed in terms of the input arguments or the state variables of the smart contracts. The information that can be obtained by the upper-bounds allows us to detect gas-expensive fragments of a Solidity program or to spot resource-related vulnerabilities at specific program points of the program. Moreover, in this article we propose an automatic optimization of Solidity programs which reduces their gas consumption replacing the accesses to state variables by gas-efficient accesses to local variables. We have experimentally evaluated our technique and we have detected that 6.81% of the public functions analyzed can be optimized and 1.43% are vulnerable to execute arbitrary code.
Sumanth Reddy Cherupally, Srinivas Boga, Prashanth Podili, Kotaro Kataoka
Verifying the integrity of IoT data in cloud-based IoT architectures is crucial for building reliable IoT applications. Traditional data integrity verification methods rely on a Trusted Third Party (TTP) that has issues of risk and operational cost by centralization. Distributed Ledger Technology (DLT) has a high potential to verify IoT data integrity and overcome the problems with TTPs. However, the existing DLTs have low transaction throughput, high computational and storage overhead, and are unsuitable for IoT environments, where a massive scale of data is generated. Recently, Directed Acyclic Graph (DAG) based DLTs have been proposed to address the low transaction throughput of linear DLTs. However, the integration of IoT Gateways (GWs) into the peer to peer (P2P) DLT network is challenging because of their low storage and computational capacity. This paper proposes Lightweight and Scalable DAG based distributed ledger for IoT (LSDI) that can work with resource-constrained IoT GWs to provide fast and scalable IoT data integrity verification. LSDI uses two key techniques: Pruning and Clustering, to reduce 1) storage overhead in IoT GWs by removing sufficiently old transactions, and 2) computational overhead of IoT GWs by partitioning a large P2P network into smaller P2P networks. The evaluation results of the proof of concept implementation showed that the proposed LSDI system achieves high transaction throughput and scalability while efficiently managing storage and computation overhead of the IoT GWs.
Christoph Egger, Mike Graf, Ralf Küsters, Daniel Rausch · 6 authors
In the past few years blockchains have been a major focus for security research, resulting in significant progress in the design, formalization, and analysis of blockchain protocols. However, the more general class of distributed ledgers, which includes not just blockchains but also prominent non-blockchain protocols, such as Corda and OmniLedger, cannot be covered by the state-of-the-art in the security literature yet. These distributed ledgers often break with traditional blockchain paradigms, such as block structures to store data, system-wide consensus, or global consistency. In this paper, we close this gap by proposing the first framework for defining and analyzing the security of general distributed ledgers, with an ideal distributed ledger functionality, called Fledger, at the core of our contribution. This functionality covers not only classical blockchains but also non-blockchain distributed ledgers in a unified way. To illustrate Fledger, we first show that the prominent ideal block-chain functionalities Gledger and GPL realize (suitable instantiations of) Fledger, which captures their security properties. This implies that their respective implementations, including Bitcoin, Ouroboros Genesis, and Ouroboros Crypsinous, realize Fledger as well. Secondly, we demonstrate that Fledger is capable of precisely modeling also non-blockchain distributed ledgers by performing the first formal security analysis of such a distributed ledger, namely the prominent Corda protocol. Due to the wide spread use of Corda in industry, in particular the financial sector, this analysis is of independent interest. These results also illustrate that Fledger not just generalizes the modular treatment of blockchains to distributed ledgers, but moreover helps to unify existing results.
Zulfiqar Ali Khan, Akbar Siami Namin
Smart contract (SC) is an extension of BlockChain technology. Ethereum BlockChain was the first to incorporate SC and thus started a new era of crypto-currencies and electronic transactions. Solidity helps to program the SCs. Still, soon after Solidity's emergence in 2014, Solidity-based SCs suffered many attacks that deprived the SC account holders of their precious funds. The main reason for these attacks was the presence of vulnerabilities in SC. This paper discusses SC vulnerabilities and classifies them according to the domain knowledge of the faulty operations. This classification is a source of reminding developers and software engineers that for SC's safety, each SC requires proper testing with effective tools to catch those classes' vulnerabilities.
João F. Ferreira, Pedro E. D. Cruz, Thomas Durieux, Rui Abreu
Over the last few years, there has been substantial research on automated analysis, testing, and debugging of Ethereum smart contracts. However, it is not trivial to compare and reproduce that research. To address this, we present SmartBugs, an extensible and easy-to-use execution framework that simplifies the execution of analysis tools on smart contracts written in Solidity, the primary language used in Ethereum. SmartBugs is currently distributed with support for 10 tools and two datasets of Solidity contracts. The first dataset can be used to evaluate the precision of analysis tools, as it contains 143 annotated vulnerable contracts with 208 tagged vulnerabilities. The second dataset contains 47,518 unique contracts collected through Etherscan. We discuss how SmartBugs supported the largest experimental setup to date both in the number of tools and in execution time. Moreover, we show how it enables easy integration and comparison of analysis tools by presenting a new extension to the tool SmartCheck that improves substantially the detection of vulnerabilities related to the DASP10 categories Bad Randomness, Time Manipulation, and Access Control (identified vulnerabilities increased from 11% to 24%).
Yinxing Xue, Mingliang Ma, Yun Lin, Yulei Sui · 6 authors
Reentrancy bugs, one of the most severe vulnerabilities in smart contracts, have caused huge financial loss in recent years. Researchers have proposed many approaches to detecting them. However, empirical studies have shown that these approaches suffer from undesirable false positives and false negatives, when the code under detection involves the interaction between multiple smart contracts.
Leonid Al'bertovich Merkin-Janson, Ruslan Rezin, Nikolay Konstantinovich Vasilyev
In this paper we consider the software architecture of InnoChain, a distributed ledger system (DLS) with 5 levels of formal verification, including a formally-verified underlying operating system (OS). The objective of this architecture is to achieve a higher level of DLS dependability compared to more traditional software architectures and quality assurance (QA) methods. The architecture of InnoChain includes (1) a programming language for smart contracts which is a domain-specific language with formal semantics embedded into CakeML, which is a functional language ofthe ML family; this allows us to carry out formal verification of smart contracts' correctness properties using higher-order logic systems, such as HOL4; (2) trusted compilation of smart contracts into the machine code using the verified compiler available for CakeML, rather than relying on a virtual machine for execution of smart contracts; (3) using CakeML for implementation of InnoChain node functionality which allows for formal verification of code correctness and trusted compilation into the machine code; (4) formal verification of the consensus protocol used InnoChain, namely HotStuff BFT; (5) using seL4, a formally-verified microkernel, as the underlying OS for InnoChain instead of more traditional general-purpose OSes such as Linux. The proposed verified architecture will allow InnoChain to be used in mission-critical applications, such as the decentralized Aircraft Fuelling Control System which is currently under development for JSC Aeroflot, the Russian national air carrier.
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We contribute a verified boardroom voting smart contract featuring maximum voter privacy such that each vote is kept private except under collusion of all other parties. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like contract, an escrow contract, an implementation of a Decentralized Finance (DeFi) contract which includes a custom token standard (Tezos FA2), and more. In total, this gives us a way to write dependent programs in Coq, test them semi-automatically, verify, and then extract to functional smart contract languages, while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.
Xiangyang Chang, Junhu Zhu, Shibin Zhao
We propose a new type of variable coverage method called Dynamic Array Double-Access Attack (DADA Attack) in Ethereum Virtual Machine (EVM). Such attack can read and write operations anywhere in the storage area, resulting in abnormal execution of contract and out of control. Vulnerable contracts with such attacks will directly lead to the loss of a large amount of property. To evaluate the effectiveness of such Double-Access Attack, we conducted theoretical analysis and experimental verification, finding attack success rate is 100% under the condition that dynamic array length is controllable.
Zulfiqar Ali Khan, Akbar Siami Namin
Smart contract (SC) is an extension of BlockChain technology. Ethereum BlockChain was the first to incorporate SC and thus started a new era of crypto-currencies and electronic transactions. Solidity helps to program the SCs. Still, soon after Solidity's emergence in 2014, Solidity-based SCs suffered many attacks that deprived the SC account holders of their precious funds. The main reason for these attacks was the presence of vulnerabilities in SC. This paper discusses SC vulnerabilities and classifies them according to the domain knowledge of the faulty operations. This classification is a source of reminding developers and software engineers that for SC's safety, each SC requires proper testing with effective tools to catch those classes' vulnerabilities.
Yixuan Zhang, Shuyu Zheng, Haoyu Wang, Lei Wu · 6 authors
Beyond an emerging popular web applications runtime supported in almost all commodity browsers, WebAssembly (WASM) is further regarded to be the next-generation execution environment for blockchain-based applications. Indeed, many popular blockchain platforms such as EOSIO and NEAR have adopted WASM-based execution engines. Most recently, WASM has been favored by Ethereum, the largest smart contract platform, to replace the state-of-the-art EVM. However, whether and how well current WASM outperforms EVM on blockchain clients is still unknown. This article conducts the first measurement study to understand the performance on WASM VMs and EVM for executing smart contracts for blockchain-based applications. To our surprise, the current WASM VM does not provide expected satisfactory performance. The overhead introduced by WASM is really non-trivial. Our results shed the light on challenges when deploying WASM in practice, and provide insightful implications for improvement space.