RegLang监管合约规则冲突检测方法

doi:10.19678/j.issn.1000-3428.0065584

摘要/Abstract

摘要： RegLang是一种面向监管规则设计的智能合约编程语言，旨在支撑监管规则数字化与合约化，已在金融等领域取得初步应用。然而，在实际应用中，金融监管领域的“适用冲突”“多轨规制”等规则冲突问题可能对区块链金融应用造成严重影响，在增加从业机构合规成本的同时，对监管合约的有效性带来挑战。针对上述问题，提出监管合约变量类型依赖分析方法与基于依赖图的变量类型传播分析方法，推断监管合约中所有变量的可能类型，并根据可满足性模理论求解器支持的符号类型实现监管合约中变量、语句和规则的符号化。基于符号分析的规则冲突检测方法，将监管规则冲突问题转换为可满足性问题，从而检测监管合约中规则的自冲突、完全冲突和局部冲突，并针对多个监管规则间完全冲突检测中的状态空间爆炸问题提出子集划分算法进行优化。实验结果表明，RegLang监管合约规则冲突检测方法可以有效检测各类监管规则冲突，在对代码行数为300行的监管规则进行冲突检测时，自冲突、完全冲突和局部冲突的平均检测耗时分别为1 234.9 ms、1 977.8 ms和2 364.5 ms，在实际应用中是可接受的，能够为实现监管规则数字化提供有效保障。

关键词: RegLang监管合约, 智能合约, 冲突检测, 符号分析, 区块链, 监管科技

Abstract: RegLang is a regulatory-oriented smart contract programming language for the digitization and contractualization of regulatory rules with preliminary applications in finance and other fields. However，in practice，the rule conflicts such as "scope conflict" and "multi-track regulation" in the financial field may have a serious impact on blockchain applications.While increasing the compliance cost，such conflicts also diminish the effectiveness of the regulatory contract. To address these problems，the variable type dependency and propagation analysis methods are proposed based on the dependency graph to infer the potential types of variables in regulatory contracts and realize the symbolization of variables，statements，and rules according to the symbol types supported by Satisfiability Module Theories（SMT） solvers.A rule conflict detection method is proposed based on symbol analysis，which transforms the regulatory rule conflict problems into satisfiability problems and detects the self-conflict，complete conflict，and partial conflict problems.Moreover，a subset partitioning method is proposed to optimize the state space explosion in detecting complete conflicts among multiple regulatory rules.The experimental results show that the proposed methods can effectively detect various regulatory rule conflicts.When the conflict detection is performed on the regulatory rules with 300 lines of code，the average time of detecting self-conflict，complete conflict，and partial conflict is 1 234.9 ms，1 977.8 ms，and 2 364.5 ms，respectively. The time consumption is acceptable in practical applications and can provide a validity guarantee for the digitalization of regulatory rules.

Key words: RegLang regulatory contract, smart contract, conflict detection, symbolic analysis, blockchain, regulatory technology

中图分类号:

TP311

高健博, 张家硕, 李青山, 陈钟. RegLang监管合约规则冲突检测方法[J]. 计算机工程, 2023, 49(5): 12-21,28.

GAO Jianbo, ZHANG Jiashuo, LI Qingshan, CHEN Zhong. Detection Method for Rule Conflicts in RegLang Regulatory Contracts[J]. Computer Engineering, 2023, 49(5): 12-21,28.

http://www.ecice06.com/CN/Y2023/V49/I5/12

图/表 12

20230515184438

20230515184442

20230515184445

20230515184449

20230515184452

20230515184456

20230515184459

20230515184503

20230515184509

20230515184513

20230515184517

20230515184520

参考文献

[1] YEUNG K.Regulation by blockchain:the emerging battle for supremacy between the code of law and code as law[J].The Modern Law Review,2019,82(2):207-239.
[2] 高健博,张家硕,李青山,等.RegLang:一种面向监管的智能合约编程语言[J].计算机科学,2022,49(S1):462-468. GAO J B,ZHANG J S,LI Q S,et al.RegLang:a smart contract programming language for regulation[J].Computer Science,2022,49(S1):462-468.(in Chinese)
[3] HAINES F,GURNEY D.The shadows of the law:contemporary approaches to regulation and the problem of regulatory conflict[J].Law & Policy,2003,25(4):353-380.
[4] 李有,程金华.行政、司法与金融规制冲突:对金融借款利率上限的实证研究[J].交大法学,2020,11(3):121-142. LI Y,CHENG J H.Conflicts of administrative and judicial powers in Chinese financial regulatory regime:an empirical study on the interest rate ceiling of financial borrowings[J].SJTU Law Review,2020,11(3):121-142.(in Chinese)
[5] 刘乃梁.银行业反垄断规制的冲突及其协调[J].法商研究,2019,36(1):43-53. LIU N L.The conflict and coordination of the anti-monopoly regulation in banking industry[J].Studies in Law and Business,2019,36(1):43-53.(in Chinese)
[6] 张亮,刘百祥,张如意,等.区块链技术综述[J].计算机工程,2019,45(5):1-12. ZHANG L,LIU B X,ZHANG R Y,et al.Overview of blockchain technology[J].Computer Engineering,2019,45(5):1-12.(in Chinese)
[7] 张健,张超,玄跻峰,等.程序分析研究进展[J].软件学报,2019,30(1):80-109. ZHANG J,ZHANG C,XUAN J F,et al.Recent progress in program analysis[J].Journal of Software,2019,30(1):80-109.(in Chinese)
[8] 张林,曾庆凯.软件安全漏洞的静态检测技术[J].计算机工程,2008,34(12):157-159. ZHANG L,ZENG Q K.Static detecting techniques of software security flaws[J].Computer Engineering,2008,34(12):157-159.(in Chinese)
[9] 陈建敏,舒辉,熊小兵.基于符号化执行的Fuzzing测试方法[J].计算机工程,2009,35(21):33-35. CHEN J M,SHU H,XIONG X B.Fuzzing test approach based on symbolic execution[J].Computer Engineering,2009,35(21):33-35.(in Chinese)
[10] ATZEI N,BARTOLETTI M,CIMOLI T.A survey of attacks on Ethereum smart contracts[C]//Proceedings of International Conference on Principles of Security and Trust.Berlin,Germany:Springer,2017:164-186.
[11] CHINEN Y,YANAI N,CRUZ J P,et al.RA:hunting for re-entrancy attacks in Ethereum smart contracts via static analysis[C]//Proceedings of 2020 IEEE International Conference on Blockchain.Washington D.C.,USA:IEEE Press,2020:327-336.
[12] ZHANG W,BANESCU S,PASOS L,et al.MPro:combining static and symbolic analysis for scalable testing of smart contract[C]//Proceedings of the 30th IEEE International Symposium on Software Reliability Engineering.Washington D.C.,USA:IEEE Press,2020:456-462.
[13] KRUPP J,ROSSOW C.TEETHER:gnawing at Ethereum to automatically exploit smart contracts[C]//Proceedings of the 27th USENIX Conference on Security Symposium.New York,USA:ACM Press,2018:1317-1333.
[14] GAO J B,LIU H,LIU C,et al.EASYFLOW:keep Ethereum away from overflow[C]//Proceedings of the 41st IEEE/ACM International Conference on Software Engineering.Washington D.C.,USA:IEEE Press,2019:23-26.
[15] ZOU W Q,LO D,KOCHHAR P S,et al.Smart contract development:challenges and opportunities[J].IEEE Transactions on Software Engineering,2021,47(10):2084-2106.
[16] HILDENBRANDT E,SAXENA M,RODRIGUES N,et al.KEVM:a complete formal semantics of the Ethereum virtual machine[C]//Proceedings of the 31st IEEE Computer Security Foundations Symposium.Washington D.C.,USA:IEEE Press,2018:204-217.
[17] MA F C,FU Y,REN M,et al.EVM:from offline detection to online reinforcement for Ethereum virtual machine[C]//Proceedings of the 26th IEEE International Conference on Software Analysis,Evolution and Reengineering.Washington D.C.,USA:IEEE Press,2019:554-558.
[18] LUU L,CHU D H,OLICKEL H,et al.Making smart contracts smarter[C]//Proceedings of 2016 ACM SIGSAC Conference on Computer and Communications Security.New York,USA:ACM Press,2016:254-269.
[19] MOURA L D,BJØRNER N.Z3:an efficient SMT solver[C]//Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin,Germany:Springer,2008:337-340.
[20] MOSSBERG M,MANZANO F,HENNENFENT E,et al.Manticore:a user-friendly symbolic execution framework for binaries and smart contracts[C]//Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering.Washington D.C.,USA:IEEE Press,2020:1186-1189.
[21] ConsenSys/mythril[EB/OL].[2022-07-24].https://github.com/ConsenSys/mythril.
[22] Ethereum yellow paper[EB/OL].[2022-07-24].https://ethereum.github.io/yellowpaper/paper.pdf.
[23] RO U G,ERBĂNUTĂ T F.An overview of the K semantic framework[J].The Journal of Logic and Algebraic Programming,2010,79(6):397-434.
[24] KOLLURI A,NIKOLIC I,SERGEY I,et al.Exploiting the laws of order in smart contracts[C]//Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis.New York,USA:ACM Press,2019:363-373.
[25] LI J,ZHAO B D,ZHANG C.Fuzzing:a survey[J].Cybersecurity,2018,1(1):1-13.
[26] HE J X,BALUNOVIĆ M,AMBROLADZE N,et al.Learning to fuzz from symbolic execution with application to smart contracts[C]//Proceedings of 2019 ACM SIGSAC Conference on Computer and Communications Security.New York,USA:ACM Press,2019:531-548.
[27] TORRES C F,SCHÜTTE J,STATE R.Osiris:hunting for integer bugs in ethereum smart contracts[C]//Proceedings of the 34th Annual Computer Security Applications Conference.New York,USA:ACM Press,2018:664-676.
[28] TSANKOV P,DAN A,DRACHSLER-COHEN D,et al.Securify:practical security analysis of smart contracts[C]//Proceedings of 2018 ACM SIGSAC Conference on Computer and Communications Security.New York,USA:ACM Press,2018:67-82.
[29] 王翀,吕荫润,陈力,等.SMT求解技术的发展及最新应用研究综述[J].计算机研究与发展,2017,54(7):1405-1425. WANG C,LÜ Y R,CHEN L,et al.Survey on development of solving methods and state-of-the-art applications of satisfiability modulo theories[J].Journal of Computer Research and Development,2017,54(7):1405-1425.(in Chinese)

选择文件类型/文献管理软件名称

选择包含的内容