Smifier: A Smart Contract Verifier for Composite Transactions

Abstract

Ensuring functional correctness of smart contracts is a pressing security concern to blockchain-based systems. With the development of blockchain application, the trading scenarios and function implementation of smart contracts have become increasing complex, containing several interacted contracts or related functions. However, the existing contracts verifiers for proving functional correctness focus on verifying isolated contract or function but ignore the interactions between them, which makes it difficult to verify correctness of composite transactions, i.e., complex transaction scenarios that invoke multiple contracts or trigger a set of transactions. In this paper, we present SMIFIER, a formal verification tool for smart contracts to prove functional properties in composite transactions. SMIFIER defines a set of specifications for composite transactions and can automatically specify properties in these multiple complex transactions. Based on states extraction and mapping, SMIFIER translates annotated Solidity program into Boogie program and verifies relations between functions and properties for interacted contracts. Our experimental evaluation on 12 real-world projects and 65 properties, demonstrates that SMIFIER is practically effective in ensuring functional correctness of properties in composite transactions.