强化Solidity不变量生成：从部署后到部署前
Strengthening Solidity Invariant Generation: From Post- to Pre-Deployment
AI总结：
针对现有Solidity智能合约不变量生成依赖部署后交易历史的局限，本文提出部署前生成框架InvSol，覆盖完整语言结构并内置漏洞防范模板，在基准测试中表现优于现有工具，漏洞识别率提升15%。
摘要：
在区块链的不可篡改性与去中心化执行的背景下，不变量对于确保Solidity智能合约的安全性和正确性至关重要。本文提出了InvSol，这是一种专门针对Solidity智能合约设计的新型部署前不变量生成框架。现有方案（即InvCon、InvCon+和Trace2Inv）依赖以太坊主网上的部署后交易历史，与之不同，InvSol可在部署前识别不变量，且能全面覆盖包括循环在内的Solidity语言结构。此外，InvSol内置了自定义模板，可有效防范重入、gas不足错误以及不变量生成过程中的异常等关键问题。我们使用一组智能合约基准集对InvSol进行了严格评估，并将其性能与前沿解决方案进行对比。结果表明，InvSol的表现显著优于这些工具，证明了其在处理交易历史有限的新合约时的有效性。值得注意的是，在识别常见漏洞方面，InvSol相比InvCon+实现了15%的提升，并且能够借助特定的不变量模板解决部分关键漏洞，表现优于Trace2Inv。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
