A smart contract is a special form of computer program that runs on a blockchain and provides a new way to implement financial and business transactions in a conflict-free and transparent environment. In blockchain systems such as Ethereum, smart contracts can handle and autonomously transfer assets of considerable value to other parties. Hence, it is particularly important to ensure that smart contracts function as intended since bugs or vulnerabilities may lead, and indeed have led, to substantial economic losses and erosion of trust for blockchain. While a number of approaches and tools have been developed to find vulnerabilities, formal methods present the highest level of confidence in the security of smart contracts. In this paper, we propose a formal solution to model a smart contract based on colored Petri nets (CPNs). Herein, we focus on the most common type of security bugs in smart contract, i.e., reentrancy bugs, which led to a serious financial loss of around USD 34 million for the Cream Finance project in 2021. We present a hierarchical CPN modelling method to analyze potential security vulnerabilities at the contract’s source code level. Then, modeling analysis methods such as correlation matrix, state space report and state space graph generated via CPN Tools simulation are exploited for formal analysis of smart contracts. The example shows the full state space and wrong path in accordance with our expected results. Finally, the conclusion was verified on the Ethereum network based on the Remix platform.
Runtime-verification of smart contracts ensures the absence of exploitations within a transaction during execution. It is a crucial security aspect that is often omitted due to its high onchain overhead. The lack of runtime-verification in public blockchains allowed attackers to compromise vulnerable contracts and cause significant monetary losses. Although several runtime protection solutions have been proposed, they do not discuss the onchain overhead limitation, which may hinder their deployment and undermine their effectiveness. To address this problem, we propose an efficient Smart contract Runtime Protection framework, called SRP, that minimizes the onchain burden of runtime-verification by integrating an off-chain mechanism with onchain contract execution. The proposed hybrid architecture is designed to protect already-deployed smart contracts from attacks in real-time while maintaining the throughput of the underlying blockchain. We first present SRP from a design perspective proposing a protocol customized for off-chain runtime-verification interoperability. Then, we evaluate our approach empirically and demonstrate the applicability of SRP using a proof-of-concept implementation on a local instance of the Ethereum network. Our empirical and experimental results indicate the feasibility and efficiency of our approach, where SRP outperforms the onchain-only mechanism in terms of service time and throughput, for increasing workloads.
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter · 9 authors
State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalizing the lower-level details, which together enable constructing machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully formalized in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles. To illustrate SSProve, we use it to mechanize the simple security proofs of ElGamal and pseudo-random-function–based encryption. We also validate the SSProve approach by conducting two more substantial case studies: First, we mechanize an SSP security proof of the key encapsulation mechanism–data encryption mechanism (KEM-DEM) public key encryption scheme, which led to the discovery of an error in the original paper proof that has since been fixed. Second, we use SSProve to formally prove security of the sigma-protocol zero-knowledge construction, and we moreover construct a commitment scheme from a sigma-protocol to compare with a similar development in CryptHOL. We instantiate the security proof for sigma-protocols to give concrete security bounds for Schnorr’s sigma-protocol.
Kealan Dunnett, Shantanu Pal, Zahra Jadidi, Raja Jurdak
CTI sharing is increasingly used by organisations to strengthen security. The sensitivity of CTI has led to research on trust-based sharing, yet most existing CTI sharing approaches only support static trust-based decisions or centralised trust evaluation, limiting their scalability and lead to centralised risk. This paper proposes a blockchain-based CTI sharing framework that relies on trustless delegates for dynamic trust-based decision-making and decentralised trust evaluation. To facilitate trustless delegation, our proposal allows CTI producers to intentionally inject false data on a periodic basis into the system to audit the behaviour of delegates. Moreover, unlike existing approaches, delegates within our framework facilitate sharing of CTI directly with consumers such that scalable CTI sharing occurs. The results of a qualitative evaluation of the proposed framework's security show that it is resilient to common privacy and trust concerns. Moreover, a quantitative evaluation of a proof-of-concept prototype using Ethereum show that the proposed framework is scalable and cost-effective.
The operation of computing$n$scalar multiplications in an elliptic curve group and then adding them together is called n-scalar multiplication.$n$-scalar multiplication is the essential operation for proof generation and verification in pairing-based trusted setup zero-knowledge succinct non-interactive argument of knowledge protocols, which enable the privacy-preserving features in blockchain applications. This paper proposed a method to compute$n$-scalar multiplication taking advantage of$3n$precomputed points. When instantiating over BLS12-381 curve, for$n=2^{c}\ (10\leq c\leq 22)$, which covers the majority of our purported applications, the proposed method showed 2.59% ∼ 12.26% theoretical speed improvement and demonstrated 1.63% ∼ 11.54% experimental improvement against Pippenger's bucket method.
We proposed a new construction for contract wallets, smart contract applications that allow users to control their crypto assets. Users can manipulate their crypto assets by simply sending emails with no need to manage keys. These emails are verified using zero-knowledge proof (ZKP) along with their attached digital signatures that the sender domain server (SDS) generates according to DomainKeys Identified Mail. Unless the SDS forges the emails, the crypto assets remain secure in the proposed system. Moreover, the existing SDSs can be used as is by outsourcing additional work to a third party that is not necessarily trusted. The system supports various functions to manipulate crypto assets. We produced a tool for variable-regex mapping (VRM) that enables developers to build a new function without ZKP skills. For example, using the tool, we built a demo application where users can exchange crypto assets via Uniswap only with emails. The published version of this paper is available at https://doi.org/10.1109/ICBC56567.2023.10174932.
In recent years, with the support of appropriate smart contract-based access control policies, blockchain technology has proven to be a compelling solution for providing a unified, trusted platform for resource sharing. However, due to the immutability property of blockchain, it can be challenging to patch or fix bugs after the deployment of a smart contract. Therefore, it is critical to ensure that the smart contract access control policies adhere to all specifications prior to their deployment, and the presence of anomalies within policies is not desirable. Thus, this paper proposes an automated policy verification and enforcement framework for Ethereum decentralized applications, which supports an automated off-chain policy verification before its deployment to the underlying blockchain. We integrate a verification engine within the off-chain module paired with a translator to convert XACML policies into Solidity smart contracts and vice-versa. Additionally, the experiments performed on benchmark XACML policies further reinforce the pragmatism of our proposal.
As most smart contracts have a financial nature and handle valuable assets, smart contract developers use access control to protect assets managed by smart contracts from being misused by malicious or unauthorized people. Unfortunately, programming languages used for writing smart contracts, such as Solidity, were not designed with a permission-based security model in mind. Therefore, smart contract developers implement access control checks based on their judgment and in an adhoc manner, which results in several vulnerabilities in smart contracts, called access control vulnerabilities. Further, the in-consistency in implementing access control makes it difficult to reason about whether a contract meets access control needs and is free of access control vulnerabilities. In this work, we propose AChecker - an approach for detecting access control vulnerabilities. Unlike prior work, AChecker does not rely on pre-defined patterns or contract transactions history. Instead, it infers access control implemented in smart contracts via static data-flow analysis. Moreover, the approach performs further symbolic-based analysis to distinguish cases when unauthorized people can obtain control of the contract as intended functionality. We evaluated AChecker on three public datasets of real-world smart contracts, including one which consists of contracts with assigned access control CVEs, and compared its effectiveness with eight analysis tools. The evaluation results showed that AChecker outperforms these tools in terms of both precision and recall. In addition, AChecker flagged vulnerabilities in 21 frequently-used contracts on Ethereum blockchain with 90% precision.
Exploitable bugs in smart contracts have caused significant monetary loss. Despite the substantial advances in smart contract bug finding, exploitable bugs and real-world attacks are still trending. In this paper we systematically investigate 516 unique real-world smart contract vulnerabilities in years 2021–2022, and study how many can be exploited by malicious users and cannot be detected by existing analysis tools. We further categorize the bugs that cannot be detected by existing tools into seven types and study their root causes, distributions, difficulties to audit, consequences, and repair strategies. For each type, we abstract them to a bug model (if possible), facilitating finding similar bugs in other contracts and future automation. We leverage the findings in auditing real world smart contracts, and so far we have been rewarded with $102,660 bug bounties for identifying 15 critical zero-day exploitable bugs, which could have caused up to $22.52 millions monetary loss if exploited.
Smart contracts are small programs on the blockchain that often handle valuable assets. Vulnerabilities in smart contracts can be costly, as time has shown over and over again. Countermeasures are high in demand and include best practice recommendations as well as tools supporting development, program verification, and post-deployment analysis. Many tools focus on detecting the absence or presence of a subset of the known vulnerabilities, delivering results of varying quality. Most comparative tool evaluations resort to selecting a handful of tools and testing them against each other. In the best case, the evaluation is based on a smallish ground truth. For Ethereum, there are commendable efforts by several author groups to manually classify contracts. However, a comprehensive ground truth is still lacking. In this work, we construct a ground truth based on publicly available benchmark sets for Ethereum smart contracts with manually checked ground truth data. We develop a method to unify these sets. Additionally, we devise strategies for matching entries that pertain to the same contract, such that we can determine overlaps and disagreements between the sets and consolidate the disagreements. Finally, we assess the quality of the included ground truth sets. Our work reduces inconsistencies, redundancies, and incompleteness while increasing the number of data points and heterogeneity.
Smart contracts are crucial elements of decentralized technologies, but they face significant obstacles to trustworthiness due to security bugs and trapdoors. To address the core issue, we propose a technology that enables programmers to focus on design-level properties rather than specific low-level attack patterns. Our proposed technology, called Theorem-Carrying-Transaction (TCT), combines the benefits of runtime checking and symbolic proof. Under the TCT protocol, every transaction must carry a theorem that proves its adherence to the safety properties in the invoked contracts, and the blockchain checks the proof before executing the transaction. The unique design of TCT ensures that the theorems are provable and checkable in an efficient manner. We believe that TCT holds a great promise for enabling provably secure smart contracts in the future. As such, we call for collaboration toward this vision.
Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan E‐Xin Tan · 10 authors
Zero-knowledge (ZK) proof systems have emerged as a promising solution for building security-sensitive applications. However, bugs in ZK applications are extremely difficult to detect and can allow a malicious party to silently exploit the system without leaving any observable trace. This paper presents Coda, a novel statically-typed language for building zero-knowledge applications. Critically, Coda makes it possible to formally specify and statically check properties of a ZK application through a rich refinement type system. One of the key challenges in formally verifying ZK applications is that they require reasoning about polynomial equations over large prime fields that go beyond the capabilities of automated theorem provers. Coda mitigates this challenge by generating a set of Coq lemmas that can be proven in an interactive manner with the help of a tactic library. We have used Coda to re-implement 77 arithmetic circuits from widely-used Circom libraries and applications. Our evaluation shows that Coda makes it possible to specify important and formally verify correctness properties of these circuits. Our evaluation also revealed 6 previously-unknown vulnerabilities in the original Circom projects.
Michael Rodler, David Paaßen, Wenting Li, Lukas Bernhard · 7 authors
Smart contracts are increasingly being used to manage large numbers of high-value cryptocurrency accounts. There is a strong demand for automated, efficient, and comprehensive methods to detect security vulnerabilities in a given contract. While the literature features a plethora of analysis methods for smart contracts, the existing proposals do not address the increasing complexity of contracts. Existing analysis tools suffer from false alarms and missed bugs in today's smart contracts that are increasingly defined by complexity and interdependencies. To scale accurate analysis to modern smart contracts, we introduce EF/CF, a high-performance fuzzer for Ethereum smart contracts. In contrast to previous work, EF/CF efficiently and accurately models complex smart contract interactions, such as reentrancy and cross-contract interactions, at a very high fuzzing throughput rate. To achieve this, EF/CF transpiles smart contract bytecode into native C++ code, thereby enabling the reuse of existing, optimized fuzzing toolchains. Furthermore, EF/CF increases fuzzing efficiency by employing a structure-aware mutation engine for smart contract transaction sequences and using a contract's ABI to generate valid transaction inputs. In a comprehensive evaluation, we show that EF/CF scales better -- without compromising accuracy -- to complex contracts compared to state-of-the-art approaches, including other fuzzers, symbolic/concolic execution, and hybrid approaches. Moreover, we show that EF/CF can automatically generate transaction sequences that exploit reentrancy bugs to steal Ether.
TrustZone as a trusted execution environment (TEE) has been proven to preserve the confidentiality of blockchain transactions supported by smart contracts. Despite some academic effort, TrustZone can only support limited languages for now. The lack of the corresponding execution environment for smart contracts seriously hinders blockchain applications from directly running on TrustZone. In this paper, we design the first virtual execution environment named TSC-VEE for performing Solidity smart contracts on TrustZone, to the best of our knowledge. TSC-VEE can be decomposed into fourfold: (1) an instruction set adapted to the isolation and world switching mechanism of TrustZone. (2) a runtime memory management mechanism that provides a pair of instructions with the corresponding processing mechanism to allocate and release the work memory. (3) a hybrid granularity resource analysis algorithm which computes and records the value of maximum stack height and static gas cost through bytecode pre-execution, avoiding runtime overflow and invalid computations. (4) a cross-isolation-environment prefetching approach that supports loading and storing the storage data from the normal world into the secure world on TrustZone before execution, thus avoiding switching the world state frequently at runtime. Extensive experimental results show that TSC-VEE can perform smart contracts correctly and efficiently on TrustZone. Compared with the most commonly used Ethereum client—Geth, TSC-VEE achieves execution performance improvements by$9.29\times$. We also implement the Ethereum virtual machine—evmoneon TrustZone. TSC-VEE can reduce the latency by 12.63% with our optimization techniques, and decrease the work memory footprint by 22.95% on average when executing various scale contracts.
Stefano Bistarelli, Andrea Bracciali, Rick Klomp, Ivan Mercanti
The Bitcoin language SCRIPT has undergone several technically non-trivial updates, still striving from security and minimal risk exposure. Up-to-date, formal verification is of strong interest for script programs that validate the correctness of the Bitcoin decentralised ledger, and allow more and more sophisticated protocols and decentralised applications to be implemented on top of Bitcoin transactions. We propose ScriFy, a comprehensive framework for the verification of the current SCRIPT language: a symbolic semantics and execution model, a model checker, and a modular (dockered), open-source verifier. Given the SCRIPT code that locks a Bitcoin transaction, ScriFy returns the minimal information needed to successfully execute it and authorise the transaction. Distinguishably, ScriFy features both recently added SCRIPT operators and an enhanced analysis, which considers prior information in the ledger. The framework is proved correct and validated through significant examples.
A smart contract is a self-executing program on a blockchain to ensure an immutable and transparent agreement without the involvement of intermediaries. Despite its growing popularity for many blockchain platforms like Ethereum, no technical means is available even when a smart contract requires to be protected from being copied. One promising direction to claim a software ownership is software watermarking. However, applying existing software watermarking techniques is challenging because of the unique properties of a smart contract, such as a code size constraint, non-free execution cost, and no support for dynamic allocation under a virtual machine environment. This paper introduces a novel software watermarking scheme, dubbed Smartmark, aiming to protect the ownership of a smart contract against a pirate activity. Smartmark builds the control flow graph of a target contract runtime bytecode, and locates a collection of bytes that are randomly elected for representing a watermark. We implement a full-fledged prototype for Ethereum, applying Smartmark to 27,824 unique smart contract bytecodes. Our empirical results demonstrate that Smartmark can effectively embed a watermark into a smart contract and verify its presence, meeting the requirements of credibility and imperceptibility while incurring an acceptable performance degradation. Besides, our security analysis shows that Smartmark is resilient against viable watermarking corruption attacks; e.g., a large number of dummy opcodes are needed to disable a watermark effectively, resulting in producing an illegitimate smart contract clone that is not economical.
Luca Olivieri, Thomas Wiben Jensen, Luca Negrini, Fausto Spoto
Smart contracts are immutable code deployed in a blockchain, whose execution modifies its global state. Code im-mutability leads to immutable bugs. To prevent such bugs, static program analysis infers information about the behavior of the code, statically, before code execution and deployment. This paper introduces MichelsonLiSA, a static analyzer based on abstract interpretation for the verification of smart contracts written in the Michelson low-level language of the Tezos blockchain. It applies MichelsonLiSA to the identification of security issues arising from cross-contract invocations.
Chihiro Kado, Naoto Yanai, Jason Paul Cruz, Shingo Okamura
Vulnerabilities are an important issue in Ethereum smart contracts. Although various vulnerability analysis tools have been developed, the effectiveness of compilers themselves in eliminating vulnerable code has not been investigated to the best of the author's knowledge. In this paper, we investigate how many vulnerable contracts are created in Ethereum smart contracts for each compiler version. In particular, we collected 503,572 contracts whose Solidity source codes are publicly available in the Ethereum blockchain and then analyzed the vulnerabilities of these contracts. Focused on three vulnerabilities with high severity, i.e., Locked Money, Using tx.origin, and Unchecked Call, we confirm that the appearance rates of these vulnerabilities are decreased by major updates of the Solidity compiler. We then found the following insights. First, the appearance rate for Locked Money is decreased after version v0.6, and second, that of Using tx.origin is quite limited independently of the compiler update. Third, the appearance rate for Unchecked Call is decreased by v0.8, but it is still high due to several factors, such as code cloning. Thus, countermeasures are needed for Unchecked Call.
As zero-knowledge proofs gain increasing adoption, the cryptography community has designed domain-specific languages (DSLs) that facilitate the construction of zero-knowledge proofs (ZKPs). Many of these DSLs, such as Circom, facilitate the construction of arithmetic circuits, which are essentially polynomial equations over a finite field. In particular, given a program in a zero-knowledge proof DSL, the compiler automatically produces the corresponding arithmetic circuit. However, a common and serious problem is that the generated circuit may be underconstrained, either due to a bug in the program or a bug in the compiler itself. Underconstrained circuits admit multiple witnesses for a given input, so a malicious party can generate bogus witnesses, thereby causing the verifier to accept a proof that it should not. Because of the increasing prevalence of such arithmetic circuits in blockchain applications, several million dollars worth of cryptocurrency have been stolen due to underconstrained arithmetic circuits. Motivated by this problem, we propose a new technique for finding ZKP bugs caused by underconstrained polynomial equations over finite fields. Our method performs semantic reasoning over the finite field equations generated by the compiler to prove whether or not each signal is uniquely determined by the input. Our proposed approach combines SMT solving with lightweight uniqueness inference to effectively reason about underconstrained circuits. We have implemented our proposed approach in a tool called QED 2 and evaluate it on 163 Circom circuits. Our evaluation shows that QED 2 can successfully solve 70% of these benchmarks, meaning that it either verifies the uniqueness of the output signals or finds a pair of witnesses that demonstrate non-uniqueness of the circuit. Furthermore, QED 2 has found 8 previously unknown vulnerabilities in widely-used circuits.
Michele Pasqua, Andrea Benini, Filippo Contro, Marco Crosara · 6 authors
The immutable nature of Ethereum transactions, and consequently Ethereum smart-contracts, has stimulated the proliferation of many approaches aiming at detecting defects and security issues before the deployment of smart-contracts on the blockchain. Indeed, the actions performed by smart-contracts instantiated on the blockchain, possibly involving substantial financial value, cannot be undone. Unfortunately, smart-contracts source code is not always available, hence approaches based on static analysis have very often to face the problem of inspecting the compiled Ethereum Virtual Machine (EVM) bytecode, retrieved directly from the blockchain. However, due to the intrinsic complexity of EVM bytecode (especially in jumps address resolution), the state-of-the-art static analysis-based solutions have poor accuracy in the automated detection of Ethereum smart-contracts programming defects and vulnerabilities. This paper presents a novel approach based on symbolic execution of the EVM operands stack that allows to resolve jumps address in the EVM bytecode and to construct a precise Control-Flow Graph (CFG) of compiled smart-contracts. Many static analysis techniques are based on a CFG-based representation of the smart-contract to validate, and would therefore benefit from our approach. We have implemented the CFG reconstruction algorithm in a tool called EtherSolve . Then, we have validated the tool on a large dataset of real-world Ethereum smart-contracts, showing that EtherSolve extracts more precise CFGs, w.r.t. state-of-the-art available approaches. Finally, we have extended EtherSolve with two detectors for two of the most prominent Ethereum smart-contracts vulnerabilities (Reentrancy and Tx.origin). Experimental results show that exploiting the proposed CFG reconstruction static analysis, leads to more accurate vulnerabilities detection, w.r.t. state-of-the-art security tools. Editor’s note: Open Science material was validated by the Journal of Systems and Software Open Science Board.
We present a Solidity smart contract implementation of the TAVS e-voting protocol. The Two Authorities Electronic Voting Scheme (TAVS) is a voting scheme that achieves universal verifiability with a reduced time-complexity both for the elector and the voting system. TAVS security derives from the RSA cryptosystem it employs, and the assumption of two entities that do not share information. We present a Solidity implementation which replaces one of these entities with an immutable smart contract in Ethereum based networks. By doing so, our implementation extends the security properties of TAVS and achieves a higher degree of resilience, verifiability, and availability. We open source the code of the implementation.
Smart contract decompilers, converting smart contract bytecode into smart contract source code, have been used extensively in many scenarios such as binary code analysis, reverse engineering, and security studies. However, existing studies, as well as industrial engineering practices, all assumed that smart contract decompilers are reliable and trustworthy, to generate correct and semantically equivalent source code from binaries. Unfortunately, whether such an assumption truly holds in practice is still unknown.In this paper, we conduct, to the best of our knowledge, the first and most comprehensive large-scale empirical study of smart contract decompilers, to gain an understanding of the reliability, limitations, and remaining research challenges of state-of-the-art smart contract decompilation tools. We first designed and implemented a software prototype SOLINSIGHT, then used it to study 5 state-of-the-art smart contract decompilers. We obtained important findings and insights from empirical results, such as: 1) we proposed 3 root causes leading to decompiler failures; 2) we revealed 2 reasons hurting performance; 3) we identified 3 root causes affecting decompilation effectiveness; 4) we proposed a measurement metric for completeness; and 5) we investigated the resilience of contract decompilers against program transformations. We suggest that: 1) decompiler builders should enhance decompilers in terms of effectiveness, performance, and completeness; and 2) security researchers should select appropriate decompilers based on the suggestions in this study. We believe these findings and suggestions will help decompiler builders, contract developers, and security researchers, by providing better guidelines for contract decompiler studies.