Many of today's companies use Smart Contracts to represent and execute their business processes. Smart contracts are self-executed programs running over blockchain. In this context, composite smart contracts are used to represent collaborative business processes. A composite smart contract is a smart contract that needs to execute other contracts using external calls to achieve its tasks. Composite smart contracts, through the use of external calls and the execution of other smart contracts that might belong to other owners or companies, bring many challenges with regard to security requirements. As a result, special efforts must be done to ensure composite smart contracts security verification. In this paper, we propose a novel approach to verify the security and the correctness of the composite smart contracts written in solidity in Ethereum blockchain. This approach is based on the finite state machine models and model checking method for modeling and verifying the composite smart contracts respectively. We consider seven security properties as well as the security issues that depend on the contract context to be checked in the composite smart contract. For this, we provide two different yet complementary types of verification. The first type of verification is applied to all smart contracts with properties called in our approach “standard properties” that represent the generic ones, while the second type considers the context-dependent properties that we called “specific properties” varying from one smart contract to another. Finally, we express all properties using computation tree logic formulae and we use the nuXmv symbolic model checker to verify the model against all properties. This approach is validated using a different set of solidity smart contracts.
With the rapid development of physical networks, tens of billions of Internet of Things (IoT) devices have been deployed worldwide. Access control is essential in the IoT system, which manages user access to vital IoT data. However, access control for the IoT is mainly based on centralized trusted servers, which face problems such as a single point of failure and data leakage. To tackle these challenges, we propose an access control framework for the IoT by combining blockchain and Intel software guard extension (SGX) technology. A blockchain validates both IoT devices and edge servers added to the network. The access control contract is deployed on the blockchain, which can manage attribute-based access control policies in a fine-grained manner and make access control decisions flexibly. SGX technology is introduced into the edge computing server to realize the confidentiality of data processing. Finally, we implemented the prototype of the framework on Quorum and conducted extensive experiments and theoretical analyses on the performance of the blockchain. The results of the experimental tests and theoretical analyses show that our framework has more advantages in computing costs and on-chain storage costs.
Blockchain-based smart contracts enable the creation of decentralized applications, which often handle assets of considerable value. While the underlying platforms guarantee the correctness of smart-contract execution, they cannot ensure that the code of a contract is correct. Today, as evidenced by a number of recent security breaches, developers still have a hard time making contracts that work properly.Even though these incidents often exploit contract interaction, prior work on smart-contract verification, vulnerability discovery, and secure development typically considers only individual contracts in isolation. To address this gap, we introduce theVeriSolidframework for the formal verification of contracts that are specified using a abstract state machine based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify the behavior of a set of interacting contracts at a high level of abstraction.VeriSolidallows the generation of Solidity code that is functionally and behaviorally equivalent to verified models, which enables the creation of correct-by-design smart contracts. We additionally introduce a graphical notation (calleddeployment diagrams) for specifying possible interactions between contract types. Based on this notation, we present a framework for the automated verification, generation, and deployment of contracts that conform to a deployment diagram. To demonstrate the applicability ofVeriSolid, we translate existing Ethereum Improvement Proposal (EIP) specifications to temporal properties for two of the most popular contract interfaces: ERC20 and ERC721. We also show you how to write code for the ERC20 and ERC721 interfaces in a way that is safe, and we do this by usingVeriSolid. We evaluate our framework on 726 contracts that are currently deployed on the Ethereum blockchain, which include 267 ERC20 and 459 ERC721 contracts. Our experiments indicate that 18% of ERC20 contracts and 4% of ERC721 contracts fail to satisfy the EIP specifications.
In the race toward next-generation systems of systems, the adoption of edge and cloud computing is escalating to deliver the underpinning end-to-end services. To safeguard the increasing attack landscape, remote attestation lets a verifier reason about the state of an untrusted remote prover. However, for most schemes, verifiability is only established under the omniscient and trusted verifier assumption, where a verifier knows the prover’s trusted states, and the prover must reveal evidence about its current state. This assumption severely challenges upscaling, inherently limits eligible verifiers, and naturally prohibits adoption in public-facing security-critical networks. To meet current zero trust paradigms, we propose a general ZEro-Knowledge pRoof of cOnformance (ZEKRO) scheme, which considers mutually distrusting participants and enables a prover to convince an untrusted verifier about its state’s correctness in zero-knowledge, i.e., without revealing anything about its state.
Norine Coenen, Bernd Finkbeiner, Jana Hofmann, Julia Tillman
Smart contracts are small but highly security-critical programs that implement wallets, token systems, auctions, crowd funding systems, elections, and other multi-party transactions on the blockchain. A broad range of methods has been developed to ensure that a smart contract is functionally correct. However, smart contracts often additionally need to satisfy certain hyperproperties, such as symmetry, determinism, or an information flow policy. In this paper, we show how a synthesis method for smart contracts can ensure that the contract satisfies its desired hyperproperties. We build on top of a recently developed synthesis approach from specifications in the temporal logic TSL. We present HyperTSL, an extension of TSL for the specification of hyperproperties of infinite-state software. As a preprocessing step, we show how to detect if a hyperproperty has an equivalent formulation as a (simpler) trace property. Finally, we describe how to refine a synthesized contract to adhere to its HyperTSL specification.
Blockchain systems based on a reusable resource, such as proof-of-stake (PoS), provide weaker security guarantees than those based on proof-of-work. Specifically, they are vulnerable to long-range attacks, where an adversary can corrupt prior participants in order to rewrite the full history of the chain. To prevent this attack on a PoS chain, we propose a protocol that checkpoints the state of the PoS chain to a proof-of-work blockchain such as Bitcoin. Our checkpointing protocol hence does not rely on any central authority. Our work uses Schnorr signatures and leverages Bitcoin recent Taproot upgrade, allowing us to create a checkpointing transaction of constant size. We argue for the security of our protocol and present an open-source implementation that was tested on the Bitcoin testnet.
Fausto Spoto, Sara Migliorini, Mauro Gambini, Andrea Benini
Abstract This paper shows that generic types ( generics ) are useful for writing more abstract and more general smart contracts, but this comes with some security risks, reporting a concrete security issue found while using generics for writing smart contracts that implement shared entities for the Hotmoka blockchain. That issue can be used to steal the remuneration of validator nodes. This paper proposes a patch based on appropriate code rewriting. Namely, smart contracts are pieces of code that are deployed and executed in the context of a blockchain infrastructure in order to automatically enforce some effects when particular events occur. The writing of smart contracts is a complex and critical activity that can benefit from the use of high-level features of programming languages, and generics is one of them. In many programming languages, such as Java, generics are implemented by erasure , i.e. replaced by their upper bound type during compilation into bytecode. This is safe at source level, since the compiler takes care of checking that types are correct, before erasure. However, the erased types of the generated bytecode are consequently weaker. In a permissionless blockchain, where every user can call the bytecode of smart contracts installed by other users, these weaker types pose a risk of attack.
Yang Yang, Shangbin Han, Ping Xie, Yan Zhu · 8 authors
With the increasing demand for privacy protection in the blockchain, the universal zero-knowledge proof protocol has been developed and widely used. Because hash function is an important cryptographic primitive in a blockchain, the zero-knowledge proof of hash preimage has a wide range of application scenarios. However, it is hard to implement it due to the transformation of efficiency and execution complexity. Currently, there are only zero-knowledge proof circuits of some widely used hash functions that have been implemented, such as SHA256. SM3 is a Chinese hash function standard published by the Chinese Commercial Cryptography Administration Office for the use of electronic authentication service systems, and hence might be used in several cryptographic applications in China. As the national cryptographic hash function standard, the zero-knowledge proof circuit of SM3 (Chinese Commercial Cryptography) has not been implemented. Therefore, this paper analyzed the SM3 algorithm process, designed a new layered circuit structure, and implemented the SM3 hash preimage zero-knowledge proof circuit with a circuit size reduced by half compared to the automatic generator. Moreover, we proposed several extended practical protocols based on the SM3 zero-knowledge proof circuit, which is widely used in blockchain.
This paper proposes a protocol for Proof of As-sets of a bitcoin exchange using the Zero-Knowledge Succinct Non-Interactive Argument of Knowledge (ZK-SNARK) without revealing either the bitcoin addresses of the exchange or balances associated with those addresses. The proof of assets is a mech-anism to prove the total value of bitcoins the exchange has the authority to spend using its private keys. We construct a privacy-preserving ZK-SNARK proof system to prove the knowledge of the private keys corresponding to the bitcoin assets of an exchange. The ZK-SNARK toolchain helps to convert an NP-Statement for proving the knowledge of the private keys (known to the exchange) into a circuit satisfiability problem. In this protocol, the exchange creates a Pedersen commitment to the value of bitcoins associated with each address without revealing the balance. The simulation results show that the proof generation time, size, and verification time are efficient in practice.
Davide Martintoni, Valerio Senni, Ernesto Gómez-Marín, Antonio Cabrera
Supply chain management is a critical aspect for every manufacturing business, in particular for safety critical systems where quality assessment and requirement satisfaction are evaluated in order to guarantee a certification of the final system. In this paper we present a blockchain-based methodology that focuses on enforcing strict data access control and that securely includes manufacturing equipment in the supply chain management process. The methodology provides cyber-security guarantees exploiting secure automated interaction between a blockchain supply chain management system and industrial manufacturing devices. A prototype of the proposed approach is implemented with state-of-the-art distributed ledger technologies integrating low-power devices hardened through the application of hardware security modules.
Jan-Philipp Töberg, Jonas Schiffl, Frederik Reiche, Bernhard Beckert · 6 authors
Ethereum smart contracts expose their functions to an untrusted network. Therefore, access control is of utmost importance. Nevertheless, many smart contracts have suffered exploits due to improper design or implementation of access control policies. In this work, we propose an approach for modeling role-based access control policies for Ethereum smart contracts on the architecture level, and we describe a process for ensuring that the implementation is correct w.r.t. that model. We achieve this through a combination of code generation, formal verification and static code analysis. Additionally, we provide an argument for the correctness of our approach and demonstrate its feasibility by detecting manually introduced violations in a case study.
Maha Ayub, Tania Saleem, Muhammad Umar Janjua, Talha Ahmad
In migrating and upgrading an Ethereum smart contract, it is necessary to transfer both the code as well as the stored data. Various methods attempt to migrate or upgrade a smart contract, but they are mostly manual, error-prone, and applicable only before deployment. Further, they have challenges in extracting the storage state of complex mapping data structures along with their keys. In this work, we present Smartmuv as an automatic source-code-based static analysis tool to analyze and extract the state from the storage-trie of smart contracts. Based on the abstract syntax tree and the control flow graphs of the Solidity source code, the tool analyzes each state variable including mapping types along the inheritance hierarchy. It also provides the upgrade algorithm that initializes the extracted state in the constructor of new smart contract. Smartmuv safely approximates the origin of the keys used in the mapping to extract values and has been able to extract the mapping state of 23,673 smart contracts with 95.7% overall precision. Moreover, we also validate the Smartmuv’s extracted state with the third-party tool Etherscan.
Haoxian Chen, Gerald Whitters, Mohammad Javad Amiri, Yuepeng Wang · 5 authors
This paper presents DeCon, a declarative programming language for implementing smart contracts and specifying contract-level properties. Driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints, DeCon models each smart contract as a set of relational tables that store transaction records. This relational representation of smart contracts enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to contract debugging via data provenance. Specifically, a DeCon program consists of a set of declarative rules and violation query rules over the relational representation, describing the smart contract implementation and contract-level properties, respectively. We have developed a tool that can compile DeCon programs into executable Solidity programs, with instrumentation for run-time property monitoring. Our case studies demonstrate that DeCon can implement realistic smart contracts such as ERC20 and ERC721 digital tokens. Our evaluation results reveal the marginal overhead of DeCon compared to the open-source reference implementation, incurring 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić · 6 authors
Today, the market capitalization of the seminal blockchain, Bitcoin, is about $803B which incentivizes malicious participants to find problematic executions that would allow them to steal financial assets. As the blockchain requires a distributed set of machines to agree on a unique block of transactions to be appended to the chain, attackers naturally try to exploit consensus vulnerabilities to double spend. As a result, formally verifying that a blockchain consensus protocol is safe and live is key to mitigate financial losses. Recent progress in mechanical proofs represent the first steps towards verifying blockchain consensus. The parameterized model checking of threshold automata (TAs) has recently proved instrumental in verifying fully asynchronous parts of consensus algorithms, like broadcast algorithms [4]. The aforementioned reduction technique cannot apply to partial synchrony: moving the message reception step to a later point in the execution might violate an assumed message delay.
Symbolic detection has been widely used to detect vulnerabilities in smart contracts. Unfortunately, as reported, existing symbolic tools cost too much time, since they need to execute all paths to detect vulnerabilities. Thus, their accuracy is limited by time. To tackle this problem, in this paper, we propose Park, the first general framework of parallel-fork symbolic execution for smart contracts. The main idea is to use multiple processes during symbolic execution, leveraging multiple CPU cores to enhance efficiency. Firstly, we propose a fork-operation based dynamic forking algorithm to achieve parallel symbolic contract execution. Secondly, to address the SMT performance loss problem in parallelization, we propose an adaptive processes restriction and adjustment algorithm. Thirdly, we design a shared-memory based global variable reconstruction method to collect and rebuild the global variables from different processes. We implement Park as a plug-in and apply it to two popular symbolic execution tools for smart contracts: Oyente and Mythril. The experimental results with third-party datasets show that Park-Oyente and Park-Mythril can provide up to 6.84x and 7.06x speedup compared to original tools, respectively.
Smart contracts deployed on permissionless blockchains, such as Ethereum, are accessible to any user in a trustless environment. Therefore, most smart contract applications implement access control policies to protect their valuable assets from unauthorized accesses. A difficulty in validating the conformance to such policies, i.e., whether the contract implementation adheres to the expected behaviors, is the lack of policy specifications. In this paper, we mine past transactions of a contract to recover a likely access control model, which can then be checked against various information flow policies and identify potential bugs related to user permissions. We implement our role mining and security policy validation in tool SPCon. The experimental evaluation on labeled smart contract role mining benchmark demonstrates that SPCon effectively mines more accurate user roles compared to the state-of-the-art role mining tools. Moreover, the experimental evaluation on real-world smart contract benchmark and access control CVEs indicates SPCon effectively detects potential permission bugs while having better scalability and lower false-positive rate compared to the state-of-the-art security tools, finding 11 previously unknown bugs and detecting six CVEs that no other tool can find.
The execution of smart contracts on the Ethereum blockchain consumes gas paid for by users submitting contracts' invocation requests. A contract execution proceeds as long as the users dedicate enough gas, within the limit set by Ethereum. If insufficient gas is provided, the contract execution halts and changes made during execution get reverted. Unfortunately, contracts may contain code patterns that increase execution cost, causing the contracts to run out of gas. These patterns can be manipulated by malicious attackers to induce unwanted behavior in the targeted victim contracts, e.g., Denial-of-Service (DoS) attacks. We call these gas-related vulnerabilities. We propose eTainter, a static analyzer for detecting gas-related vulnerabilities based on taint tracking in the bytecode of smart contracts. We evaluate eTainter by comparing it with the prior work, MadMax, on a dataset of annotated contracts. The results show that eTainter outperforms MadMax in both precision and recall, and that eTainter has a precision of 90% based on manual inspection. We also use eTainter to perform large-scale analysis of 60,612 real-world contracts on the Ethereum blockchain. We find that gas-related vulnerabilities exist in 2,763 of these contracts, and that eTainter analyzes a contract in eight seconds, on average.
By using zkSNARKs to prove that values have specific dependent types, it is possible to provably assure compatibility and correctness without revealing sensitive information and extend our trusted computing base well beyond our own system. The approach we developed expands the scope of what non-interactive zero-knowledge proofs can capture to include properties about both the execution and correctness of programs.
Ilya Grishkov, Roland Kromes, Thanassis Giannetsos, Kaitai Liang
This paper offers a prototype of a Hyperledger Fabric-IPFS based network architecture including a smart contract based encryption scheme that meant to improve the security of user's data that is being uploaded to the distributed ledger. A new extension to the self-encryption scheme was deployed by integrating data owner's identity into the encryption process. Such integration allows to permanently preserve ownership of the original file and link it to the person/entity who originally uploaded it. Moreover, self-encryption provides strong security guarantees that decryption of a file is computationally not feasible under the condition that the encrypted file and the key are safely stored.
Cong Yue, Tien Tuan Anh Dinh, Zhongle Xie, Meihui Zhang · 7 authors
Verifiable ledger databases protect data history against malicious tampering. Existing systems, such as blockchains and certificate transparency, are based on transparency logs --- a simple abstraction allowing users to verify that a log maintained by an untrusted server is append-only. They expose a simple key-value interface without transactions. Building a practical database from transparency logs, on the other hand, remains a challenge. In this paper, we explore the design space of verifiable ledger databases along three dimensions: abstraction, threat model, and performance. We survey existing systems and identify their two limitations, namely, the lack of transaction support and the inferior efficiency. We then present GlassDB, a distributed database system that addresses these limitations under a practical threat model. GlassDB inherits the verifiability of transparency logs, but supports transactions and offers high performance. It extends a ledgerlike key-value store with a data structure for efficient proofs, and adds a concurrency control mechanism for transactions. GlassDB batches independent operations from concurrent transactions when updating the core data structures. In addition, we design a new benchmark for evaluating verifiable ledger databases, by extending YCSB and TPC-C benchmarks. Using this benchmark, we compare GlassDB against four baselines: reimplemented versions of three verifiable databases, and a verifiable map backed by a transparency log. Experimental results demonstrate that GlassDB is an efficient, transactional, and verifiable ledger database system.
In decentralized finance (DeFi), lenders can offer flash loans to borrowers, i.e., loans that are only valid within a blockchain transaction and must be repaid with fees by the end of that transaction. Unlike normal loans, flash loans allow borrowers to borrow large assets without upfront collaterals deposits. Malicious adversaries use flash loans to gather large assets to exploit vulnerable DeFi protocols. In this paper, we introduce a new framework for automated synthesis of adversarial transactions that exploit DeFi protocols using flash loans. To bypass the complexity of a DeFi protocol, we propose a new technique to approximate the DeFi protocol functional behaviors using numerical methods (polynomial linear regression and nearest-neighbor interpolation). We then construct an optimization query using the approximated functions of the DeFi protocol to find an adversarial attack constituted of a sequence of functions invocations with optimal parameters that gives the maximum profit. To improve the accuracy of the approximation, we propose a novel counterexample driven approximation refinement technique. We implement our framework in a tool named FlashSyn. We evaluate FlashSyn on 16 DeFi protocols that were victims to flash loan attacks and 2 DeFi protocols from Damn Vulnerable DeFi challenges. FlashSyn automatically synthesizes an adversarial attack for 16 of the 18 benchmarks. Among the 16 successful cases, FlashSyn identifies attack vectors yielding higher profits than those employed by historical hackers in 3 cases, and also discovers multiple distinct attack vectors in 10 cases, demonstrating its effectiveness in finding possible flash loan attacks.
Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes.