基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证

王昌晶; 欧阳俊媛; 张取发; 左正康; 程着; 卢家兴

doi:10.11959/j.issn.1000-436x.2024074

您当前的位置：

首页 >

文章列表页 >

基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证

学术通信 | 更新时间：2024-11-14

- 基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证
- Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness
- 通信学报 2024年45卷第10期页码：225-242
- 作者机构：
  
  1.江西师范大学计算机信息工程学院，江西南昌 330022
  2.东华理工大学软件学院，江西南昌 330013
  3.江西师范大学国家网络化支撑软件国际合作基地，江西南昌 330022
- 作者简介：
  
  [ "王昌晶（1977- ），男，江西丰城人，博士，江西师范大学教授、博士生导师，主要研究方向为可信软件、智能化软件等。" ]
  [ "欧阳俊媛（1999- ），女，江西萍乡人，江西师范大学硕士生，主要研究方向为模型检测、区块链智能合约等。" ]
  [ "张取发（1997- ），男，江西上饶人，江西师范大学硕士生，主要研究方向为模型检测、区块链智能合约安全性验证、下一代互联网等。" ]
  [ "左正康（1980- ），男，江西抚州人，博士，江西师范大学副教授、硕士生导师，主要研究方向为形式化方法、智能化软件等。" ]
  [ "程着（1988- ），男，湖北随州人，博士，江西师范大学讲师，主要研究方向为形式化方法、实时系统、边缘计算等。" ]
  [ "卢家兴（1976- ），男，江西九江人，江西师范大学副教授，主要研究方向为模型检测、区块链智能合约安全性验证、下一代互联网等。" ]
- 基金信息：
  
  国家自然科学基金资助项目(62462037;62462036);江西省主要学科学术与技术带头人培养基金资助项目(20232BCJ22013);江西省自然科学基金资助项目(20242BAB26017);江西省教育厅科技基金资助项目(GJJ2200303;GJJ210340)
- DOI：10.11959/j.issn.1000-436x.2024074
  中图分类号： TP311
- 收稿：2023-12-29，
  
  修回：2024-03-14，
  
  纸质出版：2024-10-25
- 稿件说明：
移动端阅览
王昌晶,欧阳俊媛,张取发等.基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证[J].通信学报,2024,45(10):225-242.

WANG Changjing,OUYANG Junyuan,ZHANG Qufa,et al.Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness[J].Journal on Communications,2024,45(10):225-242.
王昌晶,欧阳俊媛,张取发等.基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证[J].通信学报,2024,45(10):225-242. DOI： 10.11959/j.issn.1000-436x.2024074.

WANG Changjing,OUYANG Junyuan,ZHANG Qufa,et al.Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness[J].Journal on Communications,2024,45(10):225-242. DOI： 10.11959/j.issn.1000-436x.2024074.

摘要

为提升拍卖合约时间安全性验证效率及验证公平性，提出基于角色的拍卖合约抽象建模及其验证方法。首先，对合约源代码进行基于账户角色的抽象建模，转换为时间自动机网络模型，并对时间安全性进行形式化描述，用UPPAAL工具验证。其次，提取合约源代码机制，建立智能合约机制模型，同样转换为时间自动机网络模型，并对4种公平性进行形式化描述，再用UPPAAL验证。最后，通过2个经典案例证明了所提方法的可行性和有效性。

Abstract

To enhance the efficiency of time security verification and fairness verification of auction contracts

an abstract modeling and verification method for role-based auction contracts was proposed. Firstly

the source code of the contract was abstractly modeled based on account roles and converted into a timed automaton network model. Formal descriptions of time security were provided and verified using the UPPAAL tool. Secondly

the mechanisms in the source code of the contract were extracted to establish a smart contract mechanism model

which was also converted into a timed automaton network model. Formal descriptions of four types of fairness were provided and verified using UPPAAL. Finally

the feasibility and effectiveness of the proposed method were demonstrated through two classic cases.

关键词

Keywords

references

TOLMACH P , LI Y , LIN S W , et al . A survey of smart contract formal specification and verification [J ] . ACM Computing Surveys , 2021 , 54 ( 7 ): 148 .

CHRISTOPH F S . Introducing Ethereum and solidity: foundations of cryptocurrency and blockchain programming for beginners [J ] . Computing Reviews , 2019 , 60 ( 1 ): 3 .

MEHAR M I , SHIER C L , GIAMBATTISTA A , et al . Understanding a revolutionary and flawed grand experiment in blockchain [J ] . Journal of Cases on Information Technology , 2019 , 21 ( 1 ): 19 - 32 .

丁伟 . 基于区块链的网络资源公平拍卖与交易框架研究 [D ] . 合肥 : 安徽大学 , 2020 .

DING W . Research on fair auction and trade framework of network resources based on blockchain [D ] . Hefei : Anhui University , 2020 .

BARTOLETTI M , CARTA S , CIMOLI T , et al . Dissecting Ponzi schemes on Ethereum: identification, analysis, and impact [J ] . Future Generation Computer Systems , 2020 , 102 : 259 - 277 .

LIU Y , LI Y , LIN S W , et al . Towards automated verification of smart contract fairness [C ] // Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering . New York : ACM Press , 2020 : 666 - 677 .

WU S K , CHEN Y J , WANG Q , et al . CReam: a smart contract enabled collusion-resistant e-auction [J ] . IEEE Transactions on Information Forensics and Security , 2019 , 14 ( 7 ): 1687 - 1701 .

郑红军 , 张乃孝 . 软件开发中的形式化方法 [J ] . 计算机科学 , 1997 , 24 ( 6 ): 90 - 96 .

ZHENG H J , ZHANG N X . Formal methods in software development [J ] . Computer Science , 1997 , 24 ( 6 ): 90 - 96 .

PAULSON L C . Isabelle: The next 700 theorem provers [J ] . Computer Science , 1990 , 31 : 361 - 386 .

DEBBI H . Counterexamples in model checking-a survey [J ] . Informatica: An International Journal of Computing and Informatics , 2018 , 42 ( 2 ): 145 - 166 .

赵颖琪 , 朱雪阳 , 李广元 , 等 . 智能合约的时间约束模式及其形式化验证 [J ] . 软件学报 , 2022 , 33 ( 8 ): 2875 - 2895 .

ZHAO Y Q , ZHU X Y , LI G Y , et al . Time constraint patterns of smart contracts and their formal verification [J ] . Journal of Software , 2022 , 33 ( 8 ): 2875 - 2895 .

SAYEED S , MARCO-GISBERT H , CAIRA T . Smart contract: attacks and protections [J ] . IEEE Access , 2020 , 8 : 24416 - 24427 .

BADRUDDOJA S , DANTU R , HE Y Y , et al . Making smart contracts smarter [C ] // Proceedings of the 2021 IEEE International Conference on Blockchain and Cryptocurrency (ICBC) . Piscataway : IEEE Press , 2021 : 1 - 3 .

MOSSBERG M , MANZANO F , HENNENFENT E , et al . Manticore: a user-friendly symbolic execution framework for binaries and smart contracts [C ] // Proceedings of the 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE) . Piscataway : IEEE Press , 2019 : 1186 - 1189 .

TSANKOV P , DAN A , DRACHSLER-COHEN D , et al . Security: practical security analysis of smart contracts [C ] // Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security . New York : ACM Press , 2018 : 67 - 82 .

OSTERLAND T , ROSE T . Model checking smart contracts for Ethereum [J ] . Pervasive and Mobile Computing , 2020 , 63 : 101129 .

CIMATTI A , CLARKE E , GIUNCHIGLIA F , et al . NuSMV: a new symbolic model verifier [C ] // Proceedings of the 11th International Conference on Computer Aided Verification . Berlin : Springer , 1999 : 495 - 499 .

LIU Z T , LIU J . Formal verification of blockchain smart contract based on colored petri net models [C ] // Proceedings of the 2019 IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC) . Piscataway : IEEE Press , 2019 : 555 - 560 .

SHISHKIN E . Debugging smart contract’s business logic using symbolic model checking [J ] . Programming and Computer Software , 2019 , 45 ( 8 ): 590 - 599 .

ZHU W J . PPTL model checking for blockchains [C ] // Proceedings of the 2020 IEEE 5th Information Technology and Mechatronics Engineering Conference (ITOEC) . Piscataway : IEEE Press , 2020 : 792 - 795 .

李书霞 , 王国卿 , 庄雷 . 区块链智能合约安全的逆向实时模型检测方法 [J ] . 小型微型计算机系统 , 2020 , 41 ( 10 ): 2030 - 2035 .

LI S X , WANG G Q , ZHUANG L . Reverse real-time model detection method for blockchain smart contract security [J ] . Journal of Chinese Computer Systems , 2020 , 41 ( 10 ): 2030 - 2035 .

吴皓 , 周世龙 , 史东辉 , 等 . 符号执行技术及应用研究综述 [J ] . 计算机工程与应用 , 2023 , 59 ( 8 ): 56 - 72 .

WU H , ZHOU S L , SHI D H , et al . Review of symbolic execution technology and applications [J ] . Computer Engineering and Applications , 2023 , 59 ( 8 ): 56 - 72 .

KALRA S , GOEL S , DHAWAN M , et al . ZEUS: analyzing safety of smart contracts [C ] // Proceedings of 2018 Network and Distributed System Security Symposium . Reston : Internet Society , 2018 : 1 - 12 .

VUJIČIĆ D , JAGODIĆ D , RANĐIĆ S . Blockchain technology, Bitcoin, and Ethereum: a brief overview [C ] // Proceedings of the 2018 17th International Symposium INFOTEH-JAHORINA (INFOTEH) . Piscataway : IEEE Press , 2018 : 1 - 6 .

周匀 . 基于承诺的区块链智能合约研究 [D ] . 上海 : 上海交通大学 , 2018 .

ZHOU Y . Research on commitment-based blockchain smart contract [D ] . Shanghai : Shanghai Jiao Tong University , 2018 .

MATTEW O . Mechanism theory [M ] . Pasadena : Humanities and Social Sciences , 2000 .

BENGTSSON J , LARSEN K , LARSSON F , et al . UPPAAL—a tool suite for automatic verification of real-time systems [C ] // International Hybrid Systems Workshop . Berlin : Springer , 1995 : 232 - 243 .

王晓楠 , 符劲轩 , 虞红芳 , 等 . 基于抽象原则和模型检测的网络协议安全分析 [J ] . 北京邮电大学学报 , 2021 , 44 ( 2 ): 40 - 46 .

WANG X N , FU J X , YU H F , et al . Network protocol security analysis based on abstract principle and model detection [J ] . Journal of Beijing University of Posts and Telecommunications , 2021 , 44 ( 2 ): 40 - 46 .

张潆藜 , 马佳利 , 刘子昂 , 等 . 以太坊Solidity智能合约漏洞检测方法综述 [J ] . 计算机科学 , 2022 , 49 ( 3 ): 52 - 61 .

ZHANG Y L , MA J L , LIU Z A , et al . Overview of vulnerability detection methods for ethereum solidity smart contracts [J ] . Computer Science , 2022 , 49 ( 3 ): 52 - 61 .

浏览量

734

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

信任环境下考虑系统公平性的边缘计算卸载策略和资源分配

反向散射辅助的无线供能通信网络中用户能效公平性研究

基于链路容量的多路径拥塞控制算法

基于网络效用最大化理论的分布式车联网拥塞控制策略

基于轮询机制的公平高效机会干扰对齐算法