As is well known, smart contracts on the blockchain store plenty of digital assets, and these contracts deployed on the blockchain are difficult to be modified. For this reason, the analysis and detection of smart contract vulnerabilities have received extensive attention. Smartcheck, a typical Java-implemented static analysis tool of smart contracts, is capable of converting Solidity source code into path diagrams based on the lexical and syntactic analysis, and finds smart contract vulnerabilities by path matching. Although Smartcheck can analyze most of the real-world vulnerabilities, some imperceptible vulnerabilities may be ignored, causing huge economic losses. In order to address these issues, we develop a new tool named MSmart to analyze the vulnerabilities of high risk such as timestamp dependence vulnerabilities, integer overflow vulnerabilities, self-destruct vulnerabilities, etc. MSmart converts the smart contract source code into an intermediate representation, and looks for smart contract vulnerabilities based on intermediate representation and XPath rules. We add new intermediate representation rules of Smartcheck to detect more kinds of vulnerabilities and optimize existing rules to suit the complexity of smart contract. We also implemented smart contract batch detection to shorten the time it takes to find vulnerabilities. To analysis the performance of MSmart, we collect 6000 real-world contracts from Etherscan and design some comparative experiments with other tools. The results of experiment show that MSmart is able to analyze related vulnerabilities better, and false positives and false negatives have been reduced due to our improvements.
Smart contracts are programs that execute transactions involving independent parties and cryptocurrencies. As programs, smart contracts are susceptible to a wide range of errors and vulnerabilities. Such vulnerabilities can result in significant losses. Furthermore, by design, smart contract transactions are irreversible. This creates a need for methods to ensure the correctness and security of contracts pre-deployment. Recently there has been substantial research into such methods. The sheer volume of this research makes articulating state-of-the-art a substantial undertaking. To address this challenge, we present a systematic review of the literature. A key feature of our presentation is to factor out the relationship between vulnerabilities and methods through properties. Specifically, we enumerate and classify smart contract vulnerabilities and methods by the properties they address. The methods considered include static analysis as well as dynamic analysis methods and machine learning algorithms that analyze smart contracts before deployment. Several patterns about the strengths of different methods emerge through this classification process.
Efficiency is a fundamental property of any type of program, but it is even more so in the context of the programs executing on the blockchain (known as smart contracts). This is because optimizing smart contracts has direct consequences on reducing the costs of deploying and executing the contracts, as there are fees to pay related to their bytes-size and to their resource consumption (called gas). Optimizing memory usage is considered a challenging problem that, among other things, requires a precise inference of the memory locations being accessed. This is also the case for the Ethereum Virtual Machine (EVM) bytecode generated by the most-widely used compiler, \texttt{solc}, whose rather unconventional and low-level memory usage challenges automated reasoning. This paper presents a static analysis, developed at the level of the EVM bytecode generated by \texttt{solc}, that infers write memory accesses that are needless and thus can be safely removed. The application of our implementation on more than 19,000 real smart contracts has detected about 6,200 needless write accesses in less than 4 hours. Interestingly, many of these writes were involved in memory usage patterns generated by \texttt{solc} that can be greatly optimized by removing entire blocks of bytecodes. To the best of our knowledge, existing optimization tools cannot infer such needless write accesses, and hence cannot detect these inefficiencies that affect both the deployment and the execution costs of Ethereum smart contracts.
Santiago Cuéllar Gempeler, Bill Harris, James Parker, Stuart Pernsteiner · 6 authors
Currently, when a security analyst discovers a vulnerability in critical software system, they must navigate a fraught dilemma: immediately disclosing the vulnerability to the public could harm the system’s users; whereas disclosing the vulnerability only to the software’s vendor lets the vendor disregard or deprioritize the security risk, to the detriment of unwittingly-affected users. A compelling recent line of work aims to resolve this by using Zero Knowledge (ZK) protocols that let analysts prove that they know a vulnerability in a program, without revealing the details of the vulnerability or the inputs that exploit it. In principle, this could be achieved by generic ZK techniques. In practice, ZK vulnerability proofs to date have been restricted in scope and expressibility, due to challenges related to generating proof statements that model real-world software at scale and to directly formulating violated properties. This article presents Cheesecloth , a novel proof-statement compiler, which proves practical vulnerabilities in ZK by soundly-but-aggressively preprocessing programs on public inputs, selectively revealing information about executed control segments, and formalizing information leakage using a novel storage-labeling scheme. Cheesecloth ’s practicality is demonstrated by generating ZK proofs of well-known vulnerabilities in (previous versions of) critical software, including the Heartbleed information leakage in OpenSSL, a memory vulnerability in the FFmpeg multimedia encoding framework, a cryptographic implementation bug in the Secure Scuttlebutt decentralised social network, and a denial of service vulnerability in OpenSSL.
Today, digital identity management for individuals is either inconvenient and error-prone or creates undesirable lock-in effects and violates privacy and security expectations. These shortcomings inhibit the digital transformation in general and seem particularly concerning in the context of novel applications such as access control for decentralized autonomous organizations and identification in the Metaverse. Decentralized or self-sovereign identity (SSI) aims to offer a solution to this dilemma by empowering individuals to manage their digital identity through machine-verifiable attestations stored in a "digital wallet" application on their edge devices. However, when presented to a relying party, these attestations typically reveal more attributes than required and allow tracking end users' activities. Several academic works and practical solutions exist to reduce or avoid such excessive information disclosure, from simple selective disclosure to data-minimizing anonymous credentials based on zero-knowledge proofs (ZKPs). We first demonstrate that the SSI solutions that are currently built with anonymous credentials still lack essential features such as scalable revocation, certificate chaining, and integration with secure elements. We then argue that general-purpose ZKPs in the form of zk-SNARKs can appropriately address these pressing challenges. We describe our implementation and conduct performance tests on different edge devices to illustrate that the performance of zk-SNARK-based anonymous credentials is already practical. We also discuss further advantages that general-purpose ZKPs can easily provide for digital wallets, for instance, to create "designated verifier presentations" that facilitate new design options for digital identity infrastructures that previously were not accessible because of the threat of man-in-the-middle attacks.
Smart contracts are computer programs running on blockchain platforms to manage large sums of cryptocurrency, govern and carry out transactions of assets between multiple parties. The security of smart contracts has attracted great attention, ever since their adoption in the management of massive cryptocurrency transactions. However, current works mainly rely on the priori security patterns, e.g., reentrancy, delegatecall, gasless send and tainted owner. Although these priori security patterns have been proven effective in finding smart contract vulnerabilities, they are very limited in finding deeper design flaws such as permission bugs, bookkeeping bugs, etc. Moreover, the reliability analysis of smart contracts becomes difficult since most smart contracts have little to no documentation for specifications. Fairness is also an important quality attribute of smart contracts and fairness issues have been proved widely existing in smart contracts such as Ponzi schemes. However, fairness has not yet attracted much research attention. Most security and reliability issues can be detected via conformance checking between software implementation and its specification. As dynamic specification mining has been proven an effective way to learn specifications from software execution traces, in this dissertation, we aim to address the aforementioned challenges by proposing a systematic approach to study the security and reliability of smart contracts based on the learned specifications through dynamic specification mining techniques. In general, contract specifications can be categorized into function-level and contract level specifications. This thesis presents the implementation of InvCon, a dynamic invariant detector for Solidity smart contracts. InvCon analyzes past transac tion histories of a contract to generate likely program invariants, which represent function-level properties that must be maintained during function execution. By combining these invariants with finite event traces from historical transactions, a novel counterexample-guided abstraction refinement algorithm is proposed and implemented in SmCon to mine compact and precise contract-level automata. Additionally, the thesis also presents SPCon that mines the role structures of smart contracts from the past transaction histories for the application of permission bug detection. The thesis demonstrates the applications of program invariants in seman tic bug detection and automated fairness verification. An invariant-based semantic test oracle, implemented in a grey-box fuzzing tool ContraMaster, is developed to enhance vulnerability detection in smart contracts, effectively addressing issues like reentrancy, exception disorder, gasless send, and integer overflow/underflow. For fairness issues, a verification framework FairCon is proposed that treats smart contracts as games and focuses on four fairness properties derived from mechanism design and game theory. Mechanism models are employed for bounded fairness property checking, while program invariants are used to analyze unbounded cases. The thesis also explores the applications of contract-level models in model-based testing and access control bug detection. ModCon is introduced as a tool that allows users to provide test models for smart contracts, specifying state definitions, transition relations, pre/post conditions, invariants, and mapping to the contract code. SPCon leverages the aforementioned role mining to identify permission bugs in smart contracts through conformance testing. The evaluation results demonstrate the high accuracy of permission bug detection, uncovering 11 previously unknown bugs in a well-known smart contract benchmark. Briefly, we have successfully derived various smart contract specifications with dy namic specification mining and studied their applications on security and reliability of smart contracts
Bugs enable security attacks on smart contracts-computer programs operating on the blockchain and managing significant financial assets. In 2022, smart contracts control tens of billions of dollars, forming an entire ecosystem of so-called decentralized financial (DeFi) applications. The ever-increasing popularity of DeFi is largely attributed to its key principles, such as transparency, permissionlessness, and immutability. Unfortunately, the devastating hacks that accompany smart contract adoption demonstrate how these properties can also have adverse effects on the security of decentralized applications, considering that, like any other software, smart contracts can contain bugs or vulnerabilities. A seminal property of smart contracts-immutability-makes sure that all these implementation errors will have a long-lasting effect on the application. Considering that smart contracts also hold large amounts of funds, it is crucial to ensure that they are secure, correct, and free of vulnerabilities.
Elvira Albert, Samir Genaim, Daniel Kirchner, Enrique Martin-Martin
Abstract The efficiency and the security of smart contracts are their two fundamental properties, but might come at odds: the use of optimizers to enhance efficiency may introduce bugs and compromise security. Our focus is on (Ethereum Virtual Machine) block-optimizations , which enhance the efficiency of jump-free blocks of opcodes by eliminating, reordering and even changing the original opcodes. We reconcile efficiency and security by providing the verification technology to formally prove the correctness of block-optimizations on smart contracts using the Coq proof assistant. This amounts to the challenging problem of proving semantic equivalence of two blocks of instructions, which is realized by means of three novel Coq components: a symbolic execution engine which can execute an block and produce a symbolic state; a number of simplification lemmas which transform a symbolic state into an equivalent one; and a checker of symbolic states to compare the symbolic states produced for the two blocks under comparison. Artifact: https://doi.org/10.5281/zenodo.7863483
This paper introduces an abstract blockchain model that employs the Burn-to-Claim cross-blockchain protocol [1]. This multi-level simulator models a virtual environment of nodes running on the Ethereum Virtual Machine (EVM). Developed using the $$CSP\#$$ language [2], it has undergone formal verification with the model checker PAT. Focusing on inter-network operations, our model ( https://github.com/b-pillai/Burn-to-Claim-formal-verification ) examines the properties of correctness, security, and atomicity using PAT. Surprisingly, atomicity, assumed to be inherent in the time-lock mechanism of the Burn-to-Claim protocol, does not always hold. We establish its validity under specific assumptions while confirming the protocol’s correctness and security under the added assumptions.
Blockchain systems are lauded for their security and reliability. Security is a cornerstone, as they employ cryptographic techniques to ensure the immutability of data, making it extremely resistant to tampering. With decentralized networks, they also reduce the risk of a single point of failure, enhancing reliability. Model checking plays a vital role in ensuring the security and reliability of blockchain systems. However, traditional model-checking approaches face challenges in handling the inherent dynamism exhibited in blockchain systems. To overcome this challenge, Aspect-Oriented programming (AOP) offers capabilities to enhance blockchain model checking through the modularization of cross-cutting concerns, enabling traceability and monitoring, facilitating dynamic instrumentation, and supporting fine-grained property specifications. The aim of this research is to enable more effective and efficient verification of dynamic behaviors in blockchain systems compared to conventional model-checking techniques using AOP. As a result, this research introducesBlockASP, a novel blockchain model verification method that leverages AOP to analyze and monitor dynamic behavior of the blockchain system.BlockASPintegrates the benefits of aspect-orientation and model checking into the blockchain architecture to strengthen security and reliability. This research has examined prior arts that are related to blockchain modeling using Object-oriented (OO) and those that are using AOP. Our research has proposed and discussed theBlockASPtechnique, the research provided a case study to demonstrate the validity and superiority in facilitating the monitoring of dynamic blockchain behavior using AOP compared to traditional approaches such as Model-Driven Architecture (MDA).
Liqun Chen, Changyu Dong, Nada El Kassem, Christopher J. P. Newton · 5 authors
Direct Anonymous Attestation (DAA) was designed for the Trusted Platform Module (TPM) and versions using RSA and elliptic curve cryptography have been included in the TPM specifications and in ISO/IEC standards. These standardised DAA schemes have their security based on the factoring or discrete logarithm problems and are therefore insecure against quantum attackers. Research into quantum-resistant DAA has resulted in several lattice-based schemes. Now in this paper, we propose the first post-quantum DAA scheme from symmetric primitives. We make use of a hash-based signature scheme, which is a slight modification of SPHINCS+, as a DAA credential. A DAA signature, proving the possession of such a credential, is a multiparty computation-based non-interactive zero-knowledge proof. The security of our scheme is proved under the Universal Composability (UC) model. While maintaining all the security properties required for a DAA scheme, we try to make the TPM’s workload as low as possible. Our DAA scheme can handle a large group size (up to 2 60 group members), which meets the requirements of rapidly developing TPM applications.
Most succinct arguments (SNARKs) are initially only proven knowledge sound (KS). We show that the commonly employed compilation strategy from polynomial interactive oracle proofs (PIOP) via polynomial commitments to knowledge sound SNARKS actually also achieves other desirable properties: weak unique response (WUR) and trapdoorless zero-knowledge (TLZK); and that together they imply simulation extractability (SIM-EXT). The factoring of SIM-EXT into KS + WUR + TLZK is becoming a cornerstone of the analysis of non-malleable SNARK systems. We show how to prove WUR and TLZK for PIOP compiled SNARKs under mild falsifiable assumptions on the polynomial commitment scheme. This means that the analysis of knowledge soundness from PIOP properties that inherently relies on non-falsifiable or idealized assumption such as the algebraic group model (AGM) or generic group model (GGM) need not be repeated. While the proof of WUR requires only mild assumptions on the PIOP, TLZK is a different matter. As perfectly hiding polynomial commitments sometimes come at a substantial performance premium, SNARK designers prefer to employ deterministic commitments with some leakage. This results in the need for a stronger zero-knowledge property for the PIOP. The modularity of our approach implies that any analysis improvements, e.g. in terms of tightness, credibility of the knowledge assumption and model of the KS analysis, or the precision of capturing real-world optimizations for TLZK also benefits the SIM-EXT guarantees.
Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark Barrett
Abstract Zero Knowledge Proofs (ZKPs) are cryptographic protocols by which a prover convinces a verifier of the truth of a statement without revealing any other information. Typically, statements are expressed in a high-level language and then compiled to a low-level representation on which the ZKP operates. Thus, a bug in a ZKP compiler can compromise the statement that the ZK proof is supposed to establish. This paper takes a step towards ZKP compiler correctness by partially verifying a field-blasting compiler pass, a pass that translates Boolean and bit-vector logic into equivalent operations in a finite field. First, we define correctness for field-blasters and ZKP compilers more generally. Next, we describe the specific field-blaster using a set of encoding rules and define verification conditions for individual rules. Finally, we connect the rules and the correctness definition by showing that if our verification conditions hold, the field-blaster is correct. We have implemented our approach in the CirC ZKP compiler and have proved bounded versions of the corresponding verification conditions. We show that our partially verified field-blaster does not hurt the performance of the compiler or its output; we also report on four bugs uncovered during verification.
In this paper, we propose the application of a well-known runtime fault-tolerance technique, N-Version Program-ming (NVP), as a new tool of smart contract software fault mitigation, especially for execute-order-validate blockchain systems, such as Hyperledger Fabric (HLF). Two patterns for aligning the NVP concept with the HLF architecture are proposed. A fully transparent solution where all peers have the same N versions installed and one we termed ‘O-Version Programming’ (where ‘O’ stands for ‘Organization’), which relies on the majority voting aspects of execute-order-validate consensus mechanisms.
Rexford Nii Ayitey Sosu, Jinfu Chen, Edward Kwadwo Boahen, Zikang Zhang
Smart contracts have gained immense popularity in recent years as self‐executing programs that operate on a blockchain. However, they are not immune to security flaws, which can result in significant financial losses. These flaws can be detected using dynamic analysis methods that extract various aspects from smart contract bytecode. Methods currently used for identifying vulnerabilities in smart contracts mostly rely on static analysis methods that search for predefined vulnerability patterns. However, these patterns often fail to capture complex vulnerabilities, leading to a high rate of false negatives. To overcome this limitation, researchers have explored machine learning‐based methods. However, the accurate interpretation of complex logic and structural information in smart contract code remains a challenge. In this study, we present a technique that combines real‐time runtime batch normalization and data augmentation for data preprocessing, along with n‐grams and one‐hot encoding for feature extraction of opcode sequence information from the bytecode. We then combined bidirectional long short‐term memory (BiLSTM), convolutional neural network, and the attention mechanism for vulnerability detection and classification. Additionally, our model includes a gated recurrent units memory module that enhances efficiency using historical execution data from the contract. Our results demonstrate that our proposed model effectively identifies smart contract vulnerabilities.
Mojtaba Eshghie, Wolfgang Ahrendt, Cyrille Artho, Thomas Hildebrandt · 5 authors
Smart contracts manage blockchain assets and embody business processes. However, mainstream smart contract programming languages such as Solidity lack explicit notions of roles, action dependencies, and time. Instead, these concepts are implemented in program code. This makes it very hard to design and analyze smart contracts. We argue that DCR graphs are a suitable formalization tool for smart contracts because they explicitly and visually capture the mentioned features. We utilize this expressiveness to show that many common high-level design patterns representing the underlying business processes in smart contract applications can be naturally modeled this way. Applying these patterns shows that DCR graphs facilitate the development and analysis of correct and reliable smart contracts by providing a clear and easy-to-understand specification.
Matthew Green, Mathias Hall-Andersen, Eric Hennenfent, Gabriel Kaptchuk · 6 authors
We consider the problem of proving in zero-knowledge the existence of vulnerabilities in executables compiled to run on real-world processors. We demonstrate that it is practical to prove knowledge of real exploits for real-world processor architectures without the need for source code and without limiting our consideration to narrow vulnerability classes. To achieve this, we devise a novel circuit compiler and a toolchain that produces highly optimized, non-interactive zero-knowledge proofs for programs executed on the MSP430, an ISA commonly used in embedded hardware. Our toolchain employs a highly optimized circuit compiler and a number of novel optimizations to construct efficient proofs for program binaries. To demonstrate the capability of our system, we test our toolchain by constructing proofs for challenges in the Microcorruption capture the flag exercises.
Carsten Baum, Lennart Braun, Cyprien Delpech de Saint Guilhem, Michael Klooß · 7 authors
We present a new method for transforming zero-knowledge protocols in the designated verifier setting into public-coin protocols, which can be made non-interactive and publicly verifiable. Our transformation applies to a large class of ZK protocols based on oblivious transfer. In particular, we show that it can be applied to recent, fast protocols based on vector oblivious linear evaluation (VOLE), with a technique we call VOLE-in-the-head, upgrading these protocols to support public verifiability. Our resulting ZK protocols have linear proof size, and are simpler, smaller and faster than related approaches based on MPC-in-the-head. To build VOLE-in-the-head while supporting both binary circuits and large finite fields, we develop several new technical tools. One of these is a new proof of security for the SoftSpokenOT protocol (Crypto 2022), which generalizes it to produce certain types of VOLE correlations over large fields. Secondly, we present a new ZK protocol that is tailored to take advantage of this form of VOLE, which leads to a publicly verifiable VOLE-in-the-head protocol with only 2x more communication than the best, designated-verifier VOLE-based protocols. We analyze the soundness of our approach when made non-interactive using the Fiat-Shamir transform, using round-by-round soundness. As an application of the resulting NIZK, we present $$\textsf{FAEST}$$ , a post-quantum signature scheme based on AES. FAEST is the first AES-based signature scheme to be smaller than SPHINCS+, with signature sizes between 5.6 and 6.6kB at the 128-bit security level. Compared with the smallest version of SPHINCS+ (7.9kB), FAEST verification is slower, but the signing times are between 8x and 40x faster.