Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness

WANG Changjing; OUYANG Junyuan; ZHANG Qufa; ZUO Zhengkang; CHENG Zhuo; LU Jiaxing

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

您当前的位置：

首页 >

文章列表页 >

Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness

Correspondences | 更新时间：2024-11-14

- Role-based abstract modeling of blockchain auction contracts and verification of temporal security and fairness
- Journal on Communications Vol. 45, Issue 10, Pages: 225-242(2024)
- 作者机构：
  
  1.江西师范大学计算机信息工程学院，江西南昌 330022
  2.东华理工大学软件学院，江西南昌 330013
  3.江西师范大学国家网络化支撑软件国际合作基地，江西南昌 330022
- 作者简介：
- 基金信息：
  
  The National Nature Science Foundation of China(62462037;62462036);Project for Academic and Technical Leader in Major Disciplines in Jiangxi Province(20232BCJ22013);Jiangxi Provincial Natural Science Foundation(20242BAB26017);Science and Technology Project of Education Department of Jiangxi Province(GJJ2200303;GJJ210340)
- DOI：10.11959/j.issn.1000-436x.2024074
  CLC： TP311
- Received：29 December 2023，
  
  Revised：2024-03-14，
  
  Published：25 October 2024
- 稿件说明：
移动端阅览
王昌晶,欧阳俊媛,张取发等.基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证[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 .

Views

734

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Edge computing offloading policies and resource allocation considering system fairness in trusted environments

User-centric energy efficiency fairness in backscatter-assisted wireless powered communication network

Multipath congestion control algorithm based on link capacity

Distributed congestion control strategy using network utility maximization theory in VANET

Fair and efficient opportunistic interference alignment algorithm based on round-robin scheduling

Related Author

Fukang LI

Ruimin REN

Shouyi YANG

Guangyue LU

Liqin SHI

Yinghui YE

Qingyun YUAN

Zhu WANG

Related Institution

School of Electrical and Information Engineering, Zhengzhou University

Shaanxi Key Laboratory of Information Communication Network and Security,Xi’an University of Posts ＆Telecommunications

School of Cyber Security, University of Chinese Academy of Sciences

Institute of Information Engineering, Chinese Academy of Sciences

College of Information Engineering,Dalian Ocean University

AI问答

⁰