文献类型：期刊文献

中文题名：基于CPN的智能合约交易顺序依赖漏洞的验证

英文题名：Verification of Transaction Ordering Dependence Vulnerability of Smart Contract Based on CPN

作者：郑红[1];刘泽润[1];黄建华[1];钱诗慧[1]

机构：[1]华东理工大学信息科学与工程学院,上海200237

年份：2022

卷号：34

期号：7

起止页码：1629

中文期刊名：系统仿真学报

外文期刊名：Journal of System Simulation

收录：CSTPCD;;Scopus;北大核心:【北大核心2020】；CSCD:【CSCD2021_2022】；

基金：国家自然科学基金(61472139);产学研项目:区块链关键技术研究(H300-41819)。

语种：中文

中文关键词：区块链;智能合约;着色Petri网;形式化验证;交易顺序依赖漏洞

外文关键词：blockchain;smart contract;colored Petri nets;formal verification;transaction ordering dependence vulnerability

摘要：智能合约的形式化验证工作主要集中在编程语言层面的漏洞研究,而交易顺序依赖作为区块链层面的漏洞更不易被检测。基于着色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.