摘要
文章研究了区块链智能合约重入漏洞的形式化验证优化方法。重入漏洞由函数调用和状态更新逻辑问题引发,依据以太坊虚拟机机制确定关键影响因素,采用线性时序逻辑、计算树逻辑等逻辑公式进行建模。文章提出动态语义增强建模、分层验证架构结合剪枝策略、跨合约交互验证扩展等优化方式,使用Coq等定理证明器完成形式化证明。基于EtherBleed和ReentrancyBench数据集开展实验,以漏洞检出率等指标进行量化评估,通过对比实验验证了优化方法的效果。
The study focuses on the optimization methods of formal verification for reentrancy vulnerabilities in blockchain smart contracts.These vulnerabilities are caused by issues in function calls and state update logic.Key influencing factors are identified based on the ethereum virtual machine mechanism,and modeling is conducted using logical formulas such as linear temporal logic and computation tree logic.The paper proposes optimization approaches including dynamic semantic enhancement modeling,a layered verification architecture combined with pruning strategies,and cross-contract interaction verification extension.Formal proofs are completed using theorem provers like Coq.Experiments are carried out based on the EtherBleed and ReentrancyBench datasets,with quantitative evaluation using metrics such as vulnerability detection rate.The effectiveness of the optimized methods is verified through comparative experiments.
作者
吴浩鸣
WU Haoming(School of Computer Science,Wuhan Donghu College,Wuhan Hubei 430212,China)
出处
《信息与电脑》
2025年第19期73-75,共3页
Information & Computer
关键词
区块链
智能合约
重入漏洞
形式化验证
验证优化
blockchain
smart contract
reentrancy vulnerability
formal verification
verification optimization
