摘要
智能合约的形式化验证工作主要集中在编程语言层面的漏洞研究,而交易顺序依赖作为区块链层面的漏洞更不易被检测。基于着色Petri网对智能合约中潜在的交易顺序依赖漏洞进行形式化验证。以Decode悬赏合约为对象,分析合约中潜在的漏洞,自顶向下地对合约本身及其执行环境建立着色Petri网模型,并引入攻击者模型来考虑合约遭受攻击的情况。通过运行模型以验证合约存在交易顺序依赖漏洞,最后基于Remix平台在以太坊网络中证实结论的正确性。
The formal verification of smart contracts researches mainly focus on programming languagelevel vulnerabilities,and the transaction ordering dependence is more difficult to be detected as a blockchain-level vulnerability.The latent transaction ordering dependence vulnerability in smart contracts is formally verified based on colored Petri nets.The latent vulnerability in the Decode reward contractis analyzed,anda colored Petri net model of the contract itself and its execution environment is established from top to bottom.The attacker model is introduced to consider the situation that the contract is attacked.By running the model to verify the existence of transaction ordering dependence vulnerability in the contract,thecorrectness of the conclusion is finally verified in the Ethereum network based on Remix platform.
作者
郑红
刘泽润
黄建华
钱诗慧
Zheng Hong;Liu Zerun;Huang Jianhua;Qian Shihui(School of Information Science and Engineering,East China University of Science and Technology,Shanghai 200237,China)
出处
《系统仿真学报》
CAS
CSCD
北大核心
2022年第7期1629-1638,共10页
Journal of System Simulation
基金
国家自然科学基金(61472139)
产学研项目:区块链关键技术研究(H300-41819)。
关键词
区块链
智能合约
着色PETRI网
形式化验证
交易顺序依赖漏洞
blockchain
smart contract
colored Petri nets
formal verification
transaction ordering dependence vulnerability
