SPrune: A Code Pruning Tool for Ethereum Solidity Contract Static Analysis

Ethereum is a cryptographic currency system built on top of blockchain. It allows anyone to write smart contracts in high-level programming languages, solidity is the most popular and mature one. In the last few years, the use of smart contracts across domains has increased a lot, security analysis to detect the potential issues in contracts thus becomes crucial. Theorem proving is a formal method technique which mathematically prove the correctness of a design with respect to a mathematical formal specification, that can be applied to smart contracts’ secure analysis. The successful implementation of a deduction calculs of theorem proving in an automated reasoning program requires the integration of search strategies that reduce the search space by pruning unnecessary deduction paths.This paper desribes SPrune, a code pruning tool designed to simplify static analysis for solidity contracts. It works by unfolding derived contracts based on the inheritance between contracts in one smart contract, and execute code pruning on the unfolded contract. Our tool allows for the application of static code pruning and provides facility for solidity contract developers and testers to trace and localize bugs in contracts.