A smart contract, as an important part of blockchain technology, has attracted considerable interest from both industry and academia. It provides the basis for the realization of a variety of practical blockchain applications and plays a crucial role in the blockchain ecosystem. While it also holds a large number of digital assets, the frequent occurrence of smart contract vulnerabilities have caused huge economic losses and destroyed the blockchain-based credit system. Currently, the security and reliability of smart contracts have become a new focus of research, and there are a number of smart contract vulnerability detection methods, such as traditional detection tools based on static or dynamic analysis. However, most of them often rely on expert rules, and therefore have poor scalability and high false negative and false positive rates. Recent deep learning methods alleviate this issue, but without considering the semantic information and context of source code. To this end, we propose a hybrid attention mechanism (HAM) model to detect security vulnerabilities in smart contracts. We extract code fragments from the source code, which focus on key points of vulnerability. We conduct extensive experiments on two public smart contract datasets (a total of 24,957 contracts). Empirical results show remarkable accuracy improvement over the state-of-the art methods on five kinds of vulnerabilities, where the detection accuracy could achieve 93.36%, 80.85%, 82.56%, 85.62%, and 82.19% for reentrancy, arithmetic vulnerability, unchecked return value, timestamp dependency, and tx.origin, respectively.

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.

In this work, we focus on the Private Intersection-Sum (PIS) with cardinality problem: two parties hold datasets containing user identifiers, and the second party additionally has an integer value associated with each user identifier. Both parties want to learn the number of users they have in common, and the sum of the integer values associated with a user, without revealing anything more. To this end, Google proposed a PIS protocol and released the open-source library Private-Join-and-Compute. And the security of the protocol has been proven proved in the honest-but-curious model. However, this study found a two potential shortcoming shortcomings in the Private-Join-and-Compute library: the user identifier stealing attack against the PIS protocol based on a special input data structure. An improved PIS protocol is proposed based on differential privacy technology, and the Private-Join-and-Compute open-source library is optimized. Through a security proof and formal analysis based on the Tamarin tool, we show that the improved PIS protocol successfully resists the discovered attack without obvious additional overhead.

The Blockchain 2.0 era integrated with smart contract along with its platforms and applications have experienced explosive growth in recent years. However, many smart contracts deployed in practice are prone to errors and cannot be modified due to the immutability of the blockchain. In light of this, it is vital to ensure the security of correctness of smart contracts before deployment. This paper proposes a formal modeling method based on Timed Colored Petri net (TCPN) to anlyze smart contracts with time constrains. We apply this formalism to a concrete voting contract system. Its functional requirements are formalized by the improved computing timing logic ASK-CTL with ML (Meta Language). Simulation and experiment show that the security and reliability of the voting contract can be effectively guaranteed.