Due to the exponential growth of IoT devices across diverse applications, it has become essential to secure edge devices against various hardware attacks, such as tampering and cloning. A tampered device with a hardware Trojan can bypass the security measures implemented through the software layers. One of the primary ways to verify the authenticity of a device is by using physically unclonable functions (PUFs) as a unique device fingerprint. During authentication, the PUF response from the edge device is transferred securely and compared with the stored response. This requires a secure communication setup between the edge device and the central server. The fingerprint must also be stored on a server for response matching. However, the potential compromise of the central server will result in the leak of all secret information of the edge devices, and adversaries can exploit it to gain unauthorized access to the IoT network. In this paper, we propose an efficient, secure, and on-demand communication protocol using zero-knowledge proofs (ZKPs) that allow the prover to provide evidence of its secret without revealing that to the verifier. The edge device, acting as the prover, convinces the central server, the verifier, of the unique PUF response stored inside the device without needing the actual storage of PUF responses on the server. The non-interactive characteristic of zk-SNARK, a widely used ZKP protocol in many popular cryptocurrencies such as Zcash, offers better optimization to authentication frequency, communication bandwidth between device and server, and protection of device-specific secret, all of which contribute to constructing our proposed device authentication framework.
Open access
2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
Most blockchain platforms from Ethereum onwards render smart contracts as stateful reactive objects that update their state and transfer crypto-assets in response to transactions. A drawback of this design is that when users submit a transaction, they cannot predict in which state it will be executed. This exposes them to transaction-ordering attacks, a widespread class of attacks where adversaries with the power to construct blocks of transactions can extract value from smart contracts (the so-called MEV attacks). The UTXO model is an alternative blockchain design that thwarts these attacks by requiring new transactions to spend past ones: since transactions have unique identifiers, reordering attacks are ineffective. Currently, the blockchains following the UTXO model either provide contracts with limited expressiveness (Bitcoin), or require complex run-time environments (Cardano). We present ILLUM , an Intermediate-Level Language for the UTXO Model. ILLUM can express real-world smart contracts, e.g. those found in Decentralized Finance. We define a compiler from ILLUM to a bare-bone UTXO blockchain with loop-free scripts. Our compilation target only requires minimal extensions to Bitcoin Script: in particular, we exploit covenants, a mechanism for preserving scripts along chains of transactions. We prove the security of our compiler: namely, any attack targeting the compiled contract is also observable at the ILLUM level. Hence, the compiler does not introduce new vulnerabilities that were not already present in the source ILLUM contract. We evaluate the practicality of ILLUM as a compilation target for higher-level languages. To this purpose, we implement a compiler from a contract language inspired by Solidity to ILLUM, and we apply it to a benchmark or real-world smart contracts.
Abstract Over the past few years, blockchain platforms supporting WebAssembly (Wasm) smart contracts are gaining popularity. However, Wasm smart contracts are often compiled from memory‐unsafe languages (e.g. C and C++). And there is a lack of effective defense against integer overflow and stack overflow at the compiler and virtual machine (VM) layers, making Wasm smart contracts even more exploitable than native C and C++ programs. In this paper, the authors propose wasm overflow detector (WASMOD) to address the integer overflow and stack overflow vulnerabilities. The authors’ approach combines bytecode instrumentation, run‐time validation, and grey‐box fuzzing to detect these vulnerabilities. The authors applied their approach to the popular EOSIO blockchain and evaluated it on 4616 deployed Wasm smart contracts. The authors’ approach detected 13 real‐world vulnerable smart contracts.
Bamidele Samuel Adelusi, Abel Chukwuemeke Uzoka, Yewande Goodness Hassan, Favour Uche Ojika
As the software supply chain becomes increasingly decentralized, ensuring the integrity and security of software components has become a critical priority. This paper presents a blockchain-integrated Software Bill of Materials (SBOM) framework designed to facilitate real-time vulnerability detection across decentralized package repositories. By leveraging blockchain’s immutable ledger and decentralized consensus mechanisms, the proposed solution enhances transparency, automates component verification, and provides a tamper-resistant audit trail for all software artifacts. The architecture incorporates smart contracts to enable automatic alerts for security vulnerabilities, expired components, and compliance violations based on real-time threat intelligence and CVE databases. A layered design approach is employed, incorporating system modeling, integration strategies, and a performance assessment conducted through simulation of real-world distributed repositories. Evaluation metrics include latency reduction, detection accuracy, and scalability under distributed workloads. This framework aligns with emerging software supply chain security mandates, including SBOM adoption in accordance with global cybersecurity policies. By synthesizing contributions from over 80 peer-reviewed studies between 2019 and 2023, the paper offers a comprehensive and future-proof strategy for enhancing the trustworthiness of software ecosystems in decentralized environments.
Kelsey Merrill, Zachary Newman, Santiago Torres-Arias, Karen Sollins
Software repositories, used for wide-scale open software distribution, are a significant vector for security attacks. Software signing provides authenticity, mitigating many such attacks. Developer-managed signing keys pose usability challenges, but certificate-based systems introduce privacy problems. This work, Speranza, uses certificates to verify software authenticity but still provides anonymity to signers using zero-knowledge identity co-commitments. In Speranza, a signer uses an automated certificate authority (CA) to create a private identity-bound signature and proof of authorization. Verifiers check that a signer was authorized to publish a package without learning the signer's identity. The package repository privately records each package's authorized signers, but publishes only commitments to identities in a public map. Then, when issuing certificates, the CA issues the certificate to a distinct commitment to the same identity. The signer then creates a zero-knowledge proof that these are identity co-commitments. We implemented a proof-of-concept for Speranza. We find that costs to maintainers (signing) and end users (verifying) are small (< 1 ms), even for a repository with millions of packages. Techniques inspired by recent key transparency systems reduce the bandwidth for serving authorization policies to 2 KiB. Server costs in this system are negligible. Our evaluation finds that Speranza is practical on the scale of the largest software repositories. We also emphasize practicality and deployability in this project. By building on existing technology and employing relatively simple and well-established cryptographic techniques, Speranza can be deployed for wide-scale use with only a few hundred lines of code and minimal changes to existing infrastructure. Speranza is a practical way to bring privacy and authenticity together for more trustworthy open-source software.
Distributed ledger technologies (DLT) usage is currently limited to a single platform as they do not have design-based interoperability capabilities. In general, it's challenging for a DLT to communicate with another one. Although several DLT solutions have been proposed and applied in specific application areas, building a general-purpose interoperability solution for any DLT remains a challenge. In previous work, we proposed a tailor-made interoperability solution between Hyperledger Fabric and Corda. This paper extends that work to enable interoperability between Hyperledger Fabric and Ethereum. The main contribution of this paper is to provide a new approach to enable interoperability between these two DLT. The approach follows a new request-response interaction model and future payments to enable the payments of services. A prototype was developed and evaluated through a case scenario, performance tests and cost analysis. Performance tests showed bottlenecks under heavy load scenarios due to Ethereum's design. Costs analysis showed that the approach is suitable for purchasing high-priced services. These promising results constitute a step forward in developing a general-purpose solution for DLT interoperability.
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.
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.
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.
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.
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.
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.