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.

翻译：不变量对于确保Solidity智能合约的安全性与正确性至关重要，尤其在区块链不可篡改和去中心化执行的背景下。本文提出InvSol，一种专为Solidity智能合约设计的、面向部署前不变量生成的新型框架。与依赖以太坊主网上部署后交易历史的现有解决方案（即InvCon、InvCon+和Trace2Inv）不同，InvSol在部署前识别不变量，并全面覆盖Solidity语言结构（包括循环）。此外，InvSol整合了定制化模板，能有效防止不变量生成过程中的重入攻击、燃气耗尽错误及异常等关键问题。我们使用智能合约基准测试集对InvSol进行严格评估，并将其性能与前沿解决方案进行比较。研究结果表明，InvSol显著优于现有工具，在处理交易历史有限的新合约方面展现出卓越效能。值得注意的是，与InvCon+相比，InvSol在识别常见漏洞方面实现了15%的性能提升，并能通过特定不变量模板处理某些关键漏洞，其表现优于Trace2Inv。