Strengthening Solidity Invariant Generation: From Post- to Pre-Deployment

TL;DR

This paper presents InvSol, a pre-deployment invariant generation framework for Solidity smart contracts that improves coverage and effectiveness over existing post-deployment solutions, enhancing security before deployment.

Contribution

InvSol is the first framework to generate invariants pre-deployment for Solidity contracts, covering all language constructs and integrating templates to prevent critical vulnerabilities.

Findings

InvSol outperforms existing tools in invariant accuracy.

Achieves 15% better vulnerability detection than InvCon+.

Successfully addresses key vulnerabilities with custom templates.

Abstract

Invariants are essential for ensuring the security and correctness of Solidity smart contracts, particularly in the context of blockchain's immutability and decentralized execution. This paper introduces InvSol, a novel framework for pre-deployment invariant generation tailored specifically for Solidity smart contracts. Unlike existing solutions, namely InvCon, InvCon+, and Trace2Inv, that rely on post-deployment transaction histories on Ethereum mainnet, InvSol identifies invariants before deployment and offers comprehensive coverage of Solidity language constructs, including loops. Additionally, InvSol incorporates custom templates to effectively prevent critical issues such as reentrancy, out-of-gas errors, and exceptions during invariant generation. We rigorously evaluate InvSol using a benchmark set of smart contracts and compare its performance with state-of-the-art solutions. Our findings reveal that InvSol significantly outperforms these tools, demonstrating its effectiveness in handling new contracts with limited transaction histories. Notably, InvSol achieves a 15% improvement in identifying common vulnerabilities compared to InvCon+ and is able to address certain crucial vulnerabilities using specific invariant templates, better than Trace2Inv.