A smart contract is a self-executing program that is stored on the blockchain and runs when predetermined conditions are satisfied. Many frequent transactions involving asset transfers rely on smart contracts deployed on the blockchain, making them highly vulnerable to attack, thus it is essential to ensure the security of smart contracts. Since the smart contract is immutable once deployed, developers must try their best to fix existing vulnerabilities in advance to ensure security. Current approaches for automatic program repair on the smart contracts have mainly adopted the heuristic search algorithms or defined patterns to fix several well-defined types of vulnerabilities. They can only provide security code recommendations for developers in specific scenarios. We explore more general automated program repair of smart contracts in software history.To pave the way for studying code changes related to bug fix of smart contracts in software history, we present a labeled public dataset for method-level program repair task, containing over 12 typical insecure code patterns. Unlike bugs in traditional software, the vulnerabilities of smart contracts are more associated with access control and conditional statements as smart contracts pertain to financial assets. For this problem, we devise a novel double-encoder network and use a code representation designed for the smart contract based on syntax information to repair program. By implementing and evaluating our approach on new dataset comprised of over 10,000 program pairs, we demonstrate the superiority of our approach in both qualitative and quantitative aspects.
Greybox fuzzers require intermediate programs called fuzz drivers to test smart contract APIs. These fuzz drivers use the semi-random inputs (bytes) generated by fuzzers to prepare suitable inputs required to test APIs. Further, fuzz driver also uses this input to decide sequence in which APIs to be invoked and enables the fuzzer to execute the APIs in that sequence to find the vulnerabilities, if any. Manually writing such complex and intelligent fuzz drivers is laborious, requires deep technical skills, hence can be cumbersome and error prone. In this paper, we propose SmartFuzzDriverGen framework to automatically generate fuzz drivers which invoke smart contract APIs using different strategies: unit-level, sequence-based (random, user-defined), and heuristics based. We evaluate the proposed framework by testing a prototype implementation of it with Golang smart contracts (targeted for Hyperledger Fabric platform) and study the effectiveness of the generated fuzz drivers in terms of code coverage as well as bug finding abilities. We observed that fuzzing of APIs in random sequences performed better than the other methods.
Nikolay Ivanov, Chenning Li, Qiben Yan, Zhiyuan Sun · 6 authors
The blockchain technology, initially created for cryptocurrency, has been re-purposed for recording state transitions of smart contracts—decentralized applications that can be invoked through external transactions. Smart contracts gained popularity and accrued hundreds of billions of dollars in market capitalization in recent years. Unfortunately, like all other computer programs, smart contracts are prone to security vulnerabilities that have incurred multibillion-dollar damages over the past decade. As a result, many automated threat mitigation solutions have been proposed to counter the security issues of smart contracts. These threat mitigation solutions include various tools and methods that are challenging to compare. This survey develops a comprehensive classification taxonomy of smart contract threat mitigation solutions within five orthogonal dimensions: defense modality, core method, targeted contracts, input-output data mapping, and threat model. We classify 133 existing threat mitigation solutions using our taxonomy and confirm that the proposed five dimensions allow us to concisely and accurately describe any smart contract threat mitigation solution. In addition to learning what the threat mitigation solutions do, we also show how these solutions work by synthesizing their actual designs into a set of uniform workflows corresponding to the eight existing defense core methods. We further create an integrated coverage map for the known smart contract vulnerabilities by the existing threat mitigation solutions. Finally, we perform the evidence-based evolutionary analysis, in which we identify trends and future perspectives of threat mitigation in smart contracts and pinpoint major weaknesses of the existing methodologies. For the convenience of smart contract security developers, auditors, users, and researchers, we deploy and maintain a regularly updated comprehensive open-source online registry of threat mitigation solutions, called Security Threat Mitigation (STM) Registry at https://seit.egr.msu.edu/research/stmregistry/ .
Sebastian Holler, Sebastian Biewer, Clara Schneidewind
The cryptocurrency Ethereum is the most widely used execution platform for smart contracts. Smart contracts are distributed applications, which govern financial assets and, hence, can implement advanced financial instruments, such as decentralized exchanges or autonomous organizations (DAOs). Their financial nature makes smart contracts an attractive attack target, as demonstrated by numerous exploits on popular contracts resulting in financial damage of millions of dollars. This omnipresent attack hazard motivates the need for sound static analysis tools, which assist smart contract developers in eliminating contract vulnerabilities a priori to deployment. Vulnerability assessment that is sound and insightful for EVM contracts is a formidable challenge because contracts execute low-level bytecode in a largely unknown and potentially hostile execution environment. So far, there exists no provably sound automated analyzer that allows for the verification of security properties based on program dependencies, even though prevalent attack classes fall into this category. In this work, we present HoRStify, the first automated analyzer for dependency properties of Ethereum smart contracts based on sound static analysis. HoRStify grounds its soundness proof on a formal proof framework for static program slicing that we instantiate to the semantics of EVM bytecode. We demonstrate that HoRStify is flexible enough to soundly verify the absence of famous attack classes such as timestamp dependency and, at the same time, performant enough to analyze real-world smart contracts.
Millions of smart contracts have been deployed onto the Ethereum platform, posing potential attack subjects. Therefore, analyzing contract binaries is vital since their sources are unavailable, involving identification comprising function entry identification and detecting its boundaries. Such boundaries are critical to many smart contract applications, e.g. reverse engineering and profiling. Unfortunately, it is challenging to identify functions from these stripped contract binaries due to the lack of internal function call statements and the compiler-inducing instruction reshuffling. Recently, several existing works excessively relied on a set of handcrafted heuristic rules which impose several faults. To address this issue, we propose a novel neural network-based framework for EVM bytecode Function Entries and Boundaries Identification (neural-FEBI) that does not rely on a fixed set of handcrafted rules. Instead, it used a two-level bi-Long Short-Term Memory network and a Conditional Random Field network to locate the function entries. The suggested framework also devises a control flow traversal algorithm to determine the code segments reachable from the function entry as its boundary. Several experiments on 38,996 publicly available smart contracts collected as binary demonstrate that neural-FEBI confirms the lowest and highest F1-scores for the function entries identification task across different datasets of 88.3 to 99.7, respectively. Its performance on the function boundary identification task is also increased from 79.4% to 97.1% compared with state-of-the-art. We further demonstrate that the identified function information can be used to construct more accurate intra-procedural CFGs and call graphs. The experimental results confirm that the proposed framework significantly outperforms state-of-the-art, often based on handcrafted heuristic rules.
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.
We introduce SDAG, a blockchain-enabled secure data awareness model by which energy nodes can provide visibility into energy operations without involving energy operators in the smart grids. SDAG consists of a registration protocol (RPro) for assigning a cryptographic identity to an energy node and a data-aware protocol (DAPro) for executing data awareness with the support of a shared secret session key and SDAG smart contracts, which facilitate data awareness consensus amongst energy nodes. SDAG satisfies the smart grid's data awareness security requirements, which include correctness of data, assurance of energy node identity, and fairness of data awareness transactions such as energy node registration. As a proof of concept, we apply our model to mitigate a recent issue on the loss of State Estimator (SE) due to contracting data in a real-world energy grid.
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.
Arijet Sarker, Simeon Wuthier, Jinoh Kim, Jonghyun Kim · 5 authors
Cryptocurrency software implements the cryptocurrency operations. We design a software assurance scheme for cryptocurrency and advance the cryptocurrency handshaking protocol. More specifically, we focus on Bitcoin for implementation and integration and advance its Version-message based hand-shaking and thus call our scheme Version++, The Version++ protocol provides software assurance, which is distinguishable from the previous research because it is permissionless, distributed, and lightweight to fit its cryptocurrency application. Utilizing Merkle Tree for the verification efficiency, we implement and test Version++ on Bitcoin software and conduct experiments in an active Bitcoin node prototype connected to the Bitcoin Mainnet. This paper for the conference demonstration supplements our technical paper at CCNC 2023 for synergy but highlights the prototyping and demonstration components of our research.
Arijet Sarker, Simeon Wuthier, Jinoh Kim, Jonghyun Kim · 5 authors
Cryptocurrency software implements the cryptocurrency operations, including the distributed consensus protocol and the peer-to-peer networking. We design a software assurance scheme for cryptocurrency and advance the cryptocurrency handshaking protocol. Since we focus on Bitcoin (the most popular cryptocurrency) for implementation and integration, we call our scheme Version++, built on and advancing the current Bitcoin handshaking protocol based on the Version message. Our Version++ protocol providing software assurance is distinguishable from the previous research because it is permissionless, distributed, and lightweight to fit its cryptocurrency application. Our scheme is permissionless since it does not require a centralized trusted authority (unlike the remote software attestation techniques from trusted computing); it is distributed since the peer checks the software assurances of its own peer connections; and it is designed for efficiency/lightweight due to the dynamic nature of the peer connections and the large-scale broadcasting in cryptocurrency networking. Utilizing Merkle Tree for the efficiency of the proof verification, we implement and test Version++ on Bitcoin software and conduct experiments in an active Bitcoin node prototype connected to the Bitcoin Mainnet. Our prototype-based performance analyses demonstrate the lightweight design of Version++. The peer-specific verification grows logarithmically with the number of software files in processing time and in storage. In addition, the Version++ verification overhead is small compared to the overall handshaking process; our measured overhead of 2.22% with minimal networking latency between the virtual machines provides an upper bound in the real-world networking with greater handshaking duration, i.e., the relative Version++ overhead in the real world with physically separate machines will be smaller.
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.
Emerging blockchain technology has become the cornerstone of many applications providing trusted data services. However, existing blockchain platforms cannot meet the growing demand for big data storage. Blockchain should duplicate both transactions and other user-defined data across nodes for integrity assurance. The rapid expansion of data on blockchain (on-chain data) increases the difficulty of deploying a full node, resulting in decreasing the degree of decentralization and adding the risk of broken data. To tackle these problems, we propose sChain, a novel framework for improving blockchain storage capacity, which does not revise blockchain implementation and can be applied to almost all the existing blockchain platforms. sChain outsources the user data to storage devices that are structurally external to the blockchain network. In theory, a user can outsource unlimited data to sChain. However, those off-chain data may suffer from corruption. To verify the data integrity, we propose a new provable data possession (PDP) scheme, which does not need a centralized entity to maintain any secret keys and therefore eliminates a single point of failure. What is more, we also design a prototype to accelerate the proposed PDP scheme through Intel SGX technology and parallel processing. Security analysis and evaluation results show that sChain can protect data security and effectively improve the blockchain storage capacity, respectively.
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.
Cyber-attacks are becoming more common against Internet users due to the increasing dependency on online communication in their daily lives. X.509 Public-Key Infrastructure (PKIX) is the most widely adopted and used system to secure online communications and digital identities. However, different attack vectors exist against the PKIX system, which attackers exploit to breach the security of the reliant protocols. Recently, various projects (e.g., Let’s Encrypt and Google Certificate Transparency) have been started to encrypt online communications, fix PKIX vulnerabilities, and guard Internet users against cyber-attacks. This survey focuses on classical PKIX proposals, certificate revocation proposals, and their implementation on blockchain as well as ledger technologies. First, we discuss the PKIX architecture, the history of the World Wide Web, the certificate issuance process, and possible attacks on the certificate issuance process. Second, a taxonomy of PKIX proposals, revocation proposals, and their modern implementation is provided. Then, a set of evaluation metrics is defined for comparison. Finally, the leading proposals are compared using 15 evaluation metrics and 13 cyber-attacks before presenting the lessons learned and suggesting future PKIX and revocation research.
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).