Blockchain Papers

Follow blockchain research across journals, conferences, and preprint repositories.

1,684 papersLast indexed Aug 31, 2026
Search papers

Paper index

1,684 results · page 40 of 71

Clear filters
Jan 1, 2022·IEEE Access
39 cites
Formal Verification of Blockchain Smart Contracts via ATL Model Checking

Wonhong Nam, Hyunyoung Kil

A blockchain is a list of data blocks as a publicly distributed ledger, which are linked together using cryptography. By allowing Turing-complete programming languages to implement smart contracts, recent blockchains such as Ethereum can reduce needs in trusted intermediators, arbitrations and enforcement costs. However, subtle errors in smart contracts have induced an enormous financial loss—for examples, the DAO attack, Parity multisignature wallet attacks, and integer underflow/overflow attacks. To identify such errors in smart contracts, various researches are performed, which are based on static analysis and theorem proving. However, they only support inspection for pre-defined error patterns, or they cannot explore the whole searching space exhaustively or be fully automatic. Hence, in this paper, we propose a novel formal verification technique to analyze blockchain smart contracts by using ATL model checking. In our methodology, we represent the interaction between users and smart contracts into a two-player game and verify properties we want to check using MCMAS that is an efficient ATL model checker for multi-agent systems. Moreover, we present three case studies to show that our proposal can successfully identify subtle flaws in real world smart contracts.

Open access
Blockchain Technology Applications and Security
Security and Verification in Computing
Advanced Malware Detection Techniques
Original source
Jan 1, 2022·Journal of Systems and Software
89 cites
Combine sliced joint graph with graph neural networks for smart contract vulnerability detection

Jie Cai, Bin Li, Jiale Zhang, Xiaobing Sun · 5 authors

Smart contract security has drawn extensive attention in recent years because of the enormous economic losses caused by vulnerabilities. Even worse, fixing bugs in a deployed smart contract is difficult, so developers must detect security vulnerabilities in a smart contract before deployment. Existing smart contract vulnerability detection efforts heavily rely on fixed rules defined by experts, which are inefficient and inflexible.To overcome the limitations of existing vulnerability detection approaches, we propose a GNN based approach for smart contract vulnerability detection. First, we construct a graph representation for a smart contract function with syntactic and semantic features by combining abstract syntax tree (AST), control flow graph (CFG), and program dependency graph (PDG). To further strengthen the presentation ability of our approach, we perform program slicing to normalize the graph and eliminate the redundant information unrelated to vulnerabilities. Then, we use a Bidirectional Gated Graph Neural-Network model with hybrid attention pooling to identify potential vulnerabilities in smart contract functions.

Open access
4 source records
Advanced Malware Detection Techniques
Security and Verification in Computing
Network Security and Intrusion Detection
Original source
Jan 1, 2022·IEEE Access
36 cites
Bulletproofs+: Shorter Proofs for a Privacy-Enhanced Distributed Ledger

Heewon Chung, Kyoohyung Han, Chanyang Ju, Myungsun Kim · 5 authors

This paper presents a new short zero-knowledge argument for the range proof and arithmetic circuits without a trusted setup. In particular, it can achieve the shortest proof size of the proof system categories without a trusted setup. More specifically, when proving that a committed value is a positive integer less than 64 bits, except for negligible error in the 128-bit security parameter, the proof size is 576 bytes long, which is 85.7% the size of the previous shortest proof due to Bünzet al.(Bulletproofs, IEEE Security and Privacy 2018). Similarly, circuit satisfiability can be proven with less communication overhead. Nevertheless, computational overheads in both proof generation and verification are comparable with those of Bulletproofs. Bulletproofs is established as one of the important privacy-enhancing technologies for a distributed ledger due to its trustless feature and short proof size. In particular, it has been implemented and optimized in various programming languages for practical usage by independent entities since it was proposed. The essence of Bulletproofs is based on the logarithmic inner product argument with no zero-knowledge. This paper revisits Bulletproofs from the viewpoint of the first sublinear zero-knowledge argument for linear algebra due to Groth (CRYPTO 2009) and then propose Bulletproofs+, an improved variety of Bulletproofs. The main component is thezero-knowledge weighted inner product argument (zk-WIP)which enables to reduce both the range proof and the arithmetic circuit proof. It already has zero-knowledge properties, there is no additional information when reducing zk-WIP, and it incurs a minimal transmission cost during the reduction process. Note that zk-WIP has all characteristics of the inner product argument, such as an aggregating range proof and batch verification; thus, Bulletproofs+ is superior to Bulletproofs in all aspects.

Open access
2 source records
Cryptography and Data Security
Blockchain Technology Applications and Security
Security and Verification in Computing
Original source
Dec 29, 2021·Lecture notes in operations research
17 cites
Gas Gauge: A Security Analysis Tool for Smart Contract Out-of-Gas Vulnerabilities

Behkish Nassirzadeh, Huaiying Sun, Sebastian Bănescu, Vijay Ganesh

In recent years we have witnessed a dramatic increase in the adoption and application of smart contracts in a variety of contexts such as decentralized finance, supply chain management, and identity management. However, a critical stumbling block to the further adoption of smart contracts is their security. A particularly widespread class of security vulnerabilities that afflicts Ethereum smart contracts is the gas limit denial of service(DoS) on a contract via unbounded operations. These vulnerabilities result in a failed transaction with an out-of-gas error and are often present in contracts containing loops whose bounds are affected by end-user input. Note that such vulnerabilities differ from gas limit DoS on the network via block stuffing. Therefore, we present Gas Gauge, a tool aimed at detecting Out-of-Gas DoS vulnerabilities in Ethereum smart contracts. Gas Gauge consists of three major components: the Detection, Identification, and Correction Phases. The Detection Phase consists of an accurate static analysis approach that finds and summarizes all the loops in a smart contract. The Identification Phase uses a white-box fuzzing approach to generate a set of inputs that causes the contract to run out of gas. The Correction Phase uses static analysis and run-time verification to predict the maximum loop bounds consistent with allowable gas usage and suggest appropriate repairs to the user of the tool. Each part of the tool can be used separately for different purposes or all together to detect, identify and help repair the contracts vulnerable to Out-of-Gas DoS vulnerabilities. Gas Gauge was tested on 1,000 real-world solidity smart contracts deployed on the Ethereum Mainnet. The results were compared to seven state-of-the-art static and symbolic tools, and it was empirically demonstrated that Gas Gauge is far more effective than competing state-of-the-art tools.

Open access
3 source records
cs.CR
Blockchain Technology Applications and Security
Security and Verification in Computing
Original source
Dec 15, 2021·arXiv (Cornell University)
0 cites
00

Nguyen Thoi Minh Quan

What is the funniest number in cryptography (Episode 2)? 0 [1]. The reason is that $\forall x, x \cdot 0 = 0$, i.e., the equation is satisfied no matter what $x$ is. We'll use zero to attack zero-knowledge proof (ZKP). In particular, we'll discuss a critical issue in a cutting-edge ZKP PLONK [2] C++ implementation which allows an attacker to create a forged proof that all verifiers will accept. We'll show how theory guides the attack's direction. In practice, the attack works like a charm and we'll show how the attack falls through a chain of perfectly aligned software cracks. In the same codebase, there is an independent critical ECDSA bug where (r, s) = (0, 0) is a valid signature for arbitrary keys and messages, but we won't discuss it further because it's a known ECDSA attack vector in the Google Wycheproof cryptanalysis project [3] that I worked on a few years ago. All bugs have been responsibly disclosed through the vendor's bug bounty program with total reward $\sim \$15,000$ (thank you).

Open access
Advanced Malware Detection Techniques
Security and Verification in Computing
Cryptographic Implementations and Security
Original source
Dec 15, 2021·2021 IEEE International Conference on Big Data (Big Data)
3 cites
Private Blockchain for Visitor Authentication and Access Control

Ka Ying Chan, Mason Lovett, Yeṣem Kurt Peker

This study applies the high data integrity that comes with blockchain technology towards authentication and access control for visitors of a physical facility. The use of smart contracts on an Ethereum based implementation of the blockchain allows for smart contract code to handle both access control and visitor authentication at scale. Javascript code executed off the blockchain enables the system to interact with and parse through the blockchain data. The proposed system is scalable, applies to multiple use cases, and mitigates issues a centralized approach faces.

Blockchain Technology Applications and Security
IoT and Edge/Fog Computing
Security and Verification in Computing
Original source
Dec 15, 2021·The Transactions of The Korean Institute of Electrical Engineers
2 cites
ATL Model Checking for Analysis of Ethereum Smart Contracts

Wonhong Nam, Hyunyoung Kil

A blockchain is a growing list of cryptographically secured blocks to maintain shared data on decentralized systems, in order to archive transactions between untrusted participants. Smart contracts are computer programs that automatically execute legal events according to the terms of contracts. Although the Ethereum blockchain has been successfully applied to a number of interesting applications, there have been several events that subtle flaws in smart contracts induce a huge amount of financial loss such as the DAO attack. Accordingly, to analyze smart contracts, we propose a novel formal verification technique to employ ATL (Alternating-time Temporal Logic) model checking. Our methodology represents the interaction between users and smart contracts with a two-player game and verify game properties by using MCMAS that is an efficient ATL model checker.

Access Control and Trust
Digital Rights Management and Security
Security and Verification in Computing
Original source
Dec 14, 2021·Proceedings of the ACM on Measurement and Analysis of Computing Systems
8 cites
Tuxedo: Maximizing Smart Contract Computation in PoW Blockchains

Sourav Das, Nitin Awathare, Ling Ren, Vinay J. Ribeiro · 5 authors

Proof-of-Work (PoW) based blockchains typically allocate only a tiny fraction (e.g., less than 1% for Ethereum) of the average interarrival time (I) between blocks for validating smart contracts present in transactions. In such systems, block validation and PoW mining are typically performed sequentially, the former by CPUs and the latter by ASICs. A trivial increase in validation time (τ) introduces the popularly known Verifier's Dilemma, and as we demonstrate, causes more forking and hurts fairness. Large τ also reduces the tolerance for safety against a Byzantine adversary. Solutions that offload validation to a set of non-chain nodes (a.k.a. off-chain approaches) suffer from trust and performance issues that are non-trivial to resolve. In this paper, we present Tuxedo, the first on-chain protocol to theoretically scale τ/I ≈1 in PoW blockchains. The key innovation in Tuxedo is to perform CPU-based block processing in parallel to ASIC mining. We achieve this by allowing miners to delay validation of transactions in a block by up to ζ blocks, where ζ is a system parameter. We perform security analysis of Tuxedo considering all possible adversarial strategies in a synchronous network with maximum end-to-end delay Δ and demonstrate that Tuxedo achieves security equivalent to known results for longest chain PoW Nakamoto consensus. Our prototype implementation of Tuxedo atop Ethereum demonstrates that it can scale τ without suffering the harmful effects of naive scaling up of τ/I in existing blockchains

Blockchain Technology Applications and Security
Cryptography and Data Security
Security and Verification in Computing
Original source
Dec 6, 2021·2021 Eighth International Conference on Software Defined Systems (SDS)
3 cites
Simulating an Ethereum 2.0 Beacon Chain Network

Marco Hünseler, Kerstin Lemke‐Rust

In this contribution, we present a simulator for the Ethereum 2.0 Beacon Chain Network. The purpose of this tool is to run various simulations to verify hypotheses and attack scenarios without the need to actually stake cryptocurrency and fulfilling validator's obligations inside the network. Because its codebase is derived from the official specification, functionality such as the fork choice rule and finality mechanisms are guaran-teed to match the behavior of conforming client implementations. Basic metrics about the live Beacon Chain network were collected and used as an input to the conducted simulations and to verify the obtained simulation results. We find that the results of conducted simulations show great correspondence to the behavior of the live Beacon Chain. We further implement various kinds of misbehavior to verify that misbehaving validators are slashed and deprived of their invested capital. Finally, two attacks are implemented to demonstrate how the simulator can be used to verify and test the applicability of various attack scenarios.

Blockchain Technology Applications and Security
Cloud Data Security Solutions
Security and Verification in Computing
Original source
Dec 1, 2021·2021 IEEE Global Communications Conference (GLOBECOM)
16 cites
Cost-Efficient Blockchain-Based Access Control for the Internet of Things

Christopher Wiraatmaja, Yuanyu Zhang, Masahiro Sasabe, Shoji Kasahara

Blockchain-based access control (BBAC) has been highly promising to prevent unauthorized resource access in the Internet of Things (IoT). However, maintaining BBAC can be potentially expensive due to the storage cost of the blockchain. To address this issue, we propose a layered BBAC architecture by combining blockchain with blockchain oracle and tamper-proof decentralized storage (e.g., IOTA). The proposed architecture consists of three main layers: a blockchain layer, which provides distributed and trustworthy access control, a storage layer, which stores meta data (e.g., subject/object attributes and policies) used in the access control of the blockchain layer, and an oracle layer, which works as a bridge to help transfer data between the blockchain and decentralized storage. This architecture achieves robust, auditable, and cost-efficient access control by migrating the meta data from the blockchain to the decentralized storage while keeping the fascinating tamper-proof feature of the blockchain. We implement and evaluate this architecture in terms of time and monetary cost to demonstrate its feasibility and superiority over existing ones.

Blockchain Technology Applications and Security
Cryptography and Data Security
Security and Verification in Computing
Original source
Dec 1, 2021·2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)
2 cites
A Novel Method to Prevent Multiple Withdraw Attack on ERC20 Tokens

Jinlei Sun, Song Huang, Changyou Zheng, Meijuan Wang · 6 authors

ERC20 is the first token standard on Ethereum and is widely used in ICOs, voting, and various asset representations. However, some methods defined in ERC20 imply potential vulnerabilities and Multiple Withdrawal Attack is one of them. Attackers can transfer more tokens than the actual allowance through this vulnerability. The current prevention methods for Multiple Withdrawal Attack include changing the transaction process, modifying the API of ERC20, and modifying the implementation of functions, etc. However, these methods have disadvantages such as poor compatibility, incomplete resolution, and high gas consumption. In this paper, we describe the process of Multiple Withdrawal Attack and analyze the shortcomings of the existing methods, and then propose a solution with lower gas consumption. In our method, a variable is added to record the allowance in the approval function to prevent tokens from being transferred repeatedly. Finally, the effectiveness and the performance of the proposed method is analyzed. The result shows that the method proposed in this paper is safe and has lower gas consumption than the existing methods.

Blockchain Technology Applications and Security
Security and Verification in Computing
Cloud Data Security Solutions
Original source
Dec 1, 2021·2021 IEEE 21st International Conference on Software Quality, Reliability and Security Companion (QRS-C)
1 cites
Support for the safety of EVM bytecode via function-call interceptor

Jisoo Kim, Eun-Sun Cho

Security problems in smart contracts are considered critical, because they are usually implemented in the field of financial services, such as cryptocurrency management. Although numerous solutions have been proposed recently, most of these are dedicated to the vulnerabilities of the source code of smart contracts before they are deployed and cannot cover runtime security issues. For instance, the deployment of vulnerable smart contracts on Ethereum block chains could cause serious damage at runtime, because contracts deployed on block chains are indestructible and are freely used later in the public domain. In addition, smart contracts are deployed in bytecode, a form that is naturally not human-readable, and thus, users fail to perceive their vulnerabilities. In this paper, ReByte, a runtime monitoring method for security enhancement of smart contracts deployed on Ethereum, is proposed. This method is based on a function-call interceptor for smart contracts that operates at runtime, and it checks the security-related properties of smart contracts and takes the corresponding measures described in a JSON policy file. At the beginning of its runtime, a smart contract bytecode is dynamically rewritten to embed within it the policy enforcement logic. The results of experiments on real-world Ethereum smart contracts on EtherScan [18] show that the ReByte prototype efficiently enhances the safety of smart contracts.

Blockchain Technology Applications and Security
Security and Verification in Computing
Advanced Malware Detection Techniques
Original source
Dec 1, 2021·2021 IEEE 27th International Conference on Parallel and Distributed Systems (ICPADS)
2 cites
Jyane: Detecting Reentrancy vulnerabilities based on path profiling method

Yicheng Fang, Chunping Wang, Zhe Sun, Hongbing Cheng

Ethereum is essentially a transaction-driven state machine, and a smart contract is a piece of executable code on Ethereum. Compared with the scripting language on Bitcoin, the smart contract language solidity, which is Turing-complete and the ex-pressive capabilities are very powerful. However, this attribute also brings many potential security threats, vulnerabilities, and various other issues. In this paper, we propose a novel smart contract security technology, named Jyane, to detect the Reentrancy vulnerability, which is one of the most threatening vulnerabilities to smart contracts. More importantly, Our tool-Jyane is the first path profiling solution for smart contracts. Firstly, we use EVM (Ethereum Virtual Machine) binary bytecode to construct control flow graphs (CFG), then use the improved Ball-Larus Path profiling algorithm (BLPP) to generate IDs for acyclic paths. Finally, after profiling the constructed paths, the suspicious paths can be detected successfully. We evaluate Jyane and other technology through comprehensive test and comparison; the results show that Jyane can profile the actual execution path of smart contracts to detect vulnerabilities with a low false-positive rate accurately. From the results of the evaluation, Jyane marked 27 of 1,226 Ethereum smart contracts selected in 2016 and 2017 as vulnerable contracts, included the vulnerability of the DAO contract which once led to a $60 million loss. Furthermore, compared with some other existing detection tools, Jyane shows broader detection range for Reentrancy vulnerabilities with lower time overhead.

Blockchain Technology Applications and Security
Advanced Malware Detection Techniques
Security and Verification in Computing
Original source
Dec 1, 2021·2021 IEEE 23rd Int Conf on High Performance Computing & Communications; 7th Int Conf on Data Science & Systems; 19th Int Conf on Smart City; 7th Int Conf on Dependability in Sensor, Cloud & Big Data Systems & Application (HPCC/DSS/SmartCity/DependSys)
2 cites
TeeSwap: Private Data Exchange using Smart Contract and Trusted Execution Environment

Peng Chen, Peichang Shi, Jie Xu, Xiang Fu · 8 authors

With importance of data value is approved, data-sharing will create more and greater value has become consensus. However, data exchange has to use a trusted third party(TTP) as an intermediary in an untrusted network environment, which may lead to leakage of data privacy. In this paper, we design a system named TeeSwap, which uses smart contract to complete data exchange, and at the same time uses cryptographic algorithms and trusted execution environment (TEE) to ensure privacy in process of data transmission, verification and contract execution. Meanwhile, TeeSwap can ensure the credibility, fairness, integrity and privacy while data are shared in our system. In the end, we implement contracts about data market and data exchange. When confirming the data transaction, data market contract can automatically generate and deploy exchange contract, which can complete the data exchange authoritatively.

Blockchain Technology Applications and Security
Cryptography and Data Security
Security and Verification in Computing
Original source
Dec 1, 2021·2021 28th Asia-Pacific Software Engineering Conference (APSEC)
7 cites
Verification Assisted Gas Reduction for Smart Contracts

Bo Gao, Siyuan Shen, Ling Shi, Jiaying Li · 6 authors

Smart contracts are computerized transaction protocols built on top of blockchain networks. Users are charged with fees, a.k.a. gas in Ethereum, when they create, deploy or execute smart contracts. Since smart contracts may contain vulnerabilities which may result in huge financial loss, developers and smart contract compilers often insert codes for security checks. The trouble is that those codes consume gas every time they are executed. Many of the inserted codes are however redundant. In this work, we present sOptimize, a tool that optimizes smart contract gas consumption automatically without compromising functionality or security. sOptimize works on smart contract bytecode, statically identifies 3 kinds of code patterns, and further removes them through verification-assisted techniques. The resulting code is guaranteed to be equivalent to the original one and can be directly deployed on blockchain. We evaluate sOptimize on a collection of 1,152 real-world smart contracts and show that it optimizes 43% of them, and the reduction on gas consumption is about 2.0% while in deployment and 1.2% in transactions, the amount can be as high as 954,201 gas units per contract.

Open access
Security and Verification in Computing
Blockchain Technology Applications and Security
Advanced Malware Detection Techniques
Original source
Dec 1, 2021·2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)
13 cites
Increasing Fuzz Testing Coverage for Smart Contracts with Dynamic Taint Analysis

Songyan Ji, Jian Dong, Junfu Qiu, Bowen Gu · 6 authors

Nowadays, smart contracts manage more and more digital assets and have become an attractive target for adversaries. To prevent smart contracts from malicious attacks, a thorough test is indispensable and must be finished before deployment because smart contracts cannot be modified after being deployed. Fuzzing is an important testing approach, but most existing smart contract fuzzers can hardly solve the constraints which involve deeply nested conditional statements, resulting in low coverage. To address this problem, we propose Targy, an efficient targeted mutation strategy based on dynamic taint analysis. We obtain the taint flow by dynamic taint propagation, and generate a more accurate mutation strategy for the input parameters of functions to simultaneously satisfy all conditional statements. We implemented Targy on sFuzz with 3.6 thousand smart contracts running on Ethereum. The numbers of covered branches and detected vulnerabilities increase by 6% and 7% respectively, and the average time required for covering a branch is reduced by 11 %.

Advanced Malware Detection Techniques
Adversarial Robustness in Machine Learning
Security and Verification in Computing
Original source
Dec 1, 2021·2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)
30 cites
WANA: Symbolic Execution of Wasm Bytecode for Extensible Smart Contract Vulnerability Detection

Bo Jiang, Yifei Chen, Dong Wang, Imran Ashraf · 5 authors

Many popular blockchain platforms support smart contracts for building decentralized applications. However, the vulnerabilities within smart contracts have demonstrated to lead to serious financial loss to their end users. In particular, the smart contracts on EOSIO smart contract platform have resulted in the loss of around 380K EOS tokens, which was around 1.9 million worth of USD at the time of attack. The EOSIO smart contract platform is based on the Wasm VM, which is also the underlying system supporting other smart contract platforms as well as Web application. In this work, we present WANA, an extensible smart contract vulnerability detection tool based on the symbolic execution for Wasm bytecode. WANA proposes a set of algorithms to detect the vulnerabilities in EOSIO smart contracts based on Wasm bytecode analysis. Our experimental analysis shows that WANA can effectively and efficiently detect vulnerabilities in EOSIO smart contracts. Furthermore, our case study also demonstrates that WANA can be extended to effectively detect vulnerabilities in Ethereum smart contracts.

Blockchain Technology Applications and Security
Advanced Malware Detection Techniques
Security and Verification in Computing
Original source
Nov 24, 2021·IEEE Transactions on Dependable and Secure Computing
78 cites
xFuzz: Machine Learning Guided Cross-Contract Fuzzing

Yinxing Xue, Jiaming Ye, Wei Zhang, Jun Sun · 7 authors

Smart contract transactions are increasingly interleaved by cross-contract calls. While many tools have been developed to identify a common set of vulnerabilities, the cross-contract vulnerability is overlooked by existing tools. Cross-contract vulnerabilities are exploitable bugs that manifest in the presence of more than two interacting contracts. Existing methods are however limited to analyze a maximum of two contracts at the same time. Detecting cross-contract vulnerabilities is highly non-trivial. With multiple interacting contracts, the search space is much larger than that of a single contract. To address this problem, we present xFuzz, a machine learning guided smart contract fuzzing framework. The machine learning models are trained with novel features (e.g., word vectors and instructions) and are used to filter likely benign program paths. Comparing with existing static tools, machine learning model is proven to be more robust, avoiding directly adopting manually-defined rules in specific tools. We compare xFuzz with three state-of-the-art tools on 7,391 contracts. xFuzz detects 18 exploitable cross-contract vulnerabilities, of which 15 vulnerabilities are exposed for the first time. Furthermore, our approach is shown to be efficient in detecting non-cross-contract vulnerabilities as well -- using less than 20% time as that of other fuzzing tools, xFuzz detects twice as many vulnerabilities.

Open access
3 source records
cs.CR
cs.SE
Advanced Malware Detection Techniques
Original source
Nov 23, 2021·2022 IEEE/ACM 44th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)
5 cites
ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts

Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho, Lucas C. Cordeiro

Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool, and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.

Open access
4 source records
Security and Verification in Computing
Advanced Malware Detection Techniques
Blockchain Technology Applications and Security
Original source
Nov 22, 2021·Anais Estendidos do X Latin-American Symposium on Dependable Computing (LADC Estendido 2021)
0 cites
Static Analysis Tools Applied to Smart Contracts

Mirko Staderini, András Pataricza, Andrea Bondavalli

Smart contracts are one of the most important innovations of the second generation of the Blockchain. They are widely used in various contexts, including financial, insurance, gaming, and betting. Once a smart contract is deployed on a Blockchain, due to its code immutability, residual vulnerabilities cannot be patched. Static analysis is an efficient method for vulnerability detection. This paper addresses the security evaluation and improvement of Solidity smart contracts through the use of static analysis tools, discussing: (i) the motivation and background, (ii) the evaluation of how good the tools are for improving security, (iii) their combination, and (iv) main results.

Open access
Blockchain Technology Applications and Security
Security and Verification in Computing
Advanced Malware Detection Techniques
Original source
Nov 22, 2021·2021 XI Brazilian Symposium on Computing Systems Engineering (SBESC)
10 cites
Verifying Security Vulnerabilities for Blockchain-based Smart Contracts

Nedas Matulevicius, Lucas C. Cordeiro

In a modern world, aspects of cybersecurity become more of a requirement to software, systems, applications than just a feature implemented by programmers in their spare time. On the one hand, blockchain remains a pastime for people interested in digital currencies or decentralized, anonymous environments such as auctions or voting. On the other hand, cyberattacks are also not an exception to the blockchain community. Most of those attacks were made through smart contracts - pieces of code through which blockchain users interact with the actual blockchain. This paper analyses the background of blockchain technology, the implementation of smart contracts, and the cybersecurity aspect in the blockchain field. We describe an in-depth analysis of five static analysis tools (or code verifiers), their capabilities and drawbacks. These are tested with smart contracts with vulnerabilities deliberately included in their source code. The vulnerabilities are tailored so that they fit into the cybersecurity properties. After the implementation process, analysis is presented. We have found out which state-of-the-art static analysis tool is the most appropriate to secure the smart contract code from future cyberattacks on the blockchain.

Blockchain Technology Applications and Security
Advanced Malware Detection Techniques
Security and Verification in Computing
Original source
Nov 18, 2021·Reversing and Offensive-Oriented Trends Symposium
9 cites
Uncovering Smart Contract VM Bugs Via Differential Fuzzing

Dominik Maier, Fabian Fäßler, Jean‐Pierre Seifert

The ongoing public interest in blockchains and smart contracts has brought a rise to a magnitude of different blockchain implementations. The rate at which new concepts are envisioned and implemented makes it hard to vet their impact on security. Especially smart contract platforms, executing untrusted code, are very complex by design. Still, people put their trust and money into chains that may lack proper testing. A behavior deviation for edge cases of single op-codes is a critical bug class in this brave new world. It can be abused for Denial of Service against the blockchain, chain splits, double-spending, or direct attacks on applications operating on the blockchain. In this paper, we propose an automated methodology to uncover such differences. Through coverage-guided and state-guided fuzzing, we explore smart contract virtual machine behavior against multiple VMs in parallel. We develop NeoDiff, the first framework for feedback-guided differential fuzzing of smart contract VMs. We discuss real, monetary consequences our tool prevents. NeoDiff can be ported to new smart contract platforms with ease. Apart from fuzzing Ethereum VMs, NeoDiff found a range of critical differentials in VMs for the Neo blockchain. Moreover, through a higher-layer semantics mutator, we uncovered semantic discrepancies between Neo smart contracts written in Python when executed on the blockchain vs. classic CPython. Along the way, NeoDiff uncovered memory corruptions in the C# Neo VM.

2 source records
Security and Verification in Computing
Advanced Malware Detection Techniques
Advanced Data Storage Technologies
Original source