强化 Solidity 不变量生成：从部署前至部署后
软件工程
2024-09-18 v2 编程语言
摘要
不变量对于确保 Solidity 智能合约的安全与正确性至关重要，尤其是在区块链不可变性与去中心化执行的背景下。本文引入 InvSol—a 专为 Solidity 智能合约设计的部署前不变量生成框架。不同于现有方法（如 InvCon、InvCon+ 和 Trace2Inv），后者依赖以太坊主网的事后部署交易历史，InvSol 在部署前识别不变量，并提供 Solidity 语言 construct 的全面覆盖，包括循环结构。此外，InvSol 集成自定义模板，有效防止不变量生成期间出现的关键问题，如重入攻击、资源耗尽错误及异常。我们使用基准智能合约集合对 InvSol 进行严格评估，并与最先进的解决方案进行比较。我们的发现表明，InvSol 在处理交易历史有限的新型合约方面显著优于这些工具，显示现实效能。值得注意的是，InvSol 在识别常见漏洞方面比 InvCon+ 提高了 15%，并能使用特定不变量模板处理某些关键漏洞，优于 Trace2Inv。
引用
@article{arxiv.2409.01804,
title = {Strengthening Solidity Invariant Generation: From Post- to Pre-Deployment},
author = {Kartik Kaushik and Raju Halder and Samrat Mondal},
journal= {arXiv preprint arXiv:2409.01804},
year = {2024}
}