arXiv ScienceSearch

arXiv subjects

Chengxuan Zhang

Publications and source records attributed to Chengxuan Zhang.

2 recordsLinked to original sources

EventSpec: Defining and Detecting Event-Semantic Issues in Blockchain Ecosystems

In recent years, smart contracts have become the backbone of decentralized applications (DApps), and off-chain systems such as bridges, wallets, and indexers rely heavily on event logs to track contract execution and state changes. However, the Ethereum Virtual Machine (EVM) does not validate or enforce event semantics, so logs can diverge from on-chain state, misleading off-chain systems into accepting incorrect state transitions. Existing smart contract vulnerability detection tools focus on logic bugs, with limited support for detecting event-semantic defects. To address this gap, we collect audit reports and incident cases and apply open card sorting to define five classes of event-semantic defects: event collision, state-event mismatch, unauthorized event emission, event emission mismatch, and event parameter mismatch. We propose EventSpec, which infers event specifications from a contract corpus via behavior inference and semantic-constraint extraction and applies differential checking to identify event-semantic defects in target contracts. We run EventSpec on 6,617 real-world contracts and evaluate detection effectiveness based on manually labeled results; EventSpec achieves an overall comprehensive precision of 90.17%. We further provide an off-chain evaluation harness that reproduces two off-chain attack vectors on any EVM-compatible chain: event origin confusion caused by unintended emitters and event-state desynchronization where events lack matching state updates. Using this harness, we demonstrate the feasibility of these attacks on bridge relayers, blockchain explorers, and NFT marketplaces, and report six wallet issues, four of which were confirmed (including a $600 bounty), with two remaining pending.

cs.CR

Automated Invariant Generation for Solidity Smart Contracts

Smart contracts are computer programs running on blockchains to automate the transaction execution between users. The absence of contract specifications poses a real challenge to the correctness verification of smart contracts. Program invariants are properties that are always preserved throughout the execution, which characterize an important aspect of the program behaviors. In this paper, we propose a novel invariant generation framework, INVCON+, for Solidity smart contracts. INVCON+ extends the existing invariant detector, InvCon, to automatically produce verified contract invariants based on both dynamic inference and static verification. Unlike INVCON+, InvCon only produces likely invariants, which have a high probability to hold, yet are still not verified against the contract code. Particularly, INVCON+ is able to infer more expressive invariants that capture richer semantic relations of contract code. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks. The experimental results indicate that INVCON+ efficiently produces high-quality invariant specifications, which can be used to secure smart contracts from common vulnerabilities.

cs.SE