Yaqiong He

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.

Smart contracts are decentralized applications running on blockchain platforms and have been widely used in a variety of scenarios in recent years. However, frequent smart contract security incidents have focused more and more attention on their security and reliability, and smart contract vulnerability detection has become an urgent problem in blockchain security. Most of the existing methods rely on fixed rules defined by experts, which have the disadvantages of single detection type, poor scalability, and high false alarm rate. To solve the above problems, this paper proposes a method that combines Bi-LSTM and an attention mechanism for multiple vulnerability detection of smart contract opcodes. First, we preprocessed the data to convert the opcodes into a feature matrix suitable as the input of the neural network and then used the Bi-LSTM model based on the attention mechanism to classify smart contracts with multiple labels. The experimental results show that the model can detect multiple vulnerabilities at the same time, and all evaluation indicators exceeded 85%, which proves the effectiveness of the method proposed in this paper for multiple vulnerability detection tasks in smart contracts.