5G网络中区块链和智能合约的策略规范和验证

⃝可在www.sciencedirect.com上在线获取ScienceDirectICTExpress 6（2020）43www.elsevier.com/locate/icte5G网络中区块链和智能合约的策略规范和验证Devrim Unala， Mohammed Hammoudehb，Mehmet Sabir Kirazca卡塔尔多哈卡塔尔大学KINDI计算研究中心b英国曼彻斯特城市大学计算与数学系c英国莱斯特德蒙福特大学网络技术学院接收日期：2019年5月30日;接受日期：2019年在线提供2019年摘要区块链为金融交易的创新提供了前所未有的机会。一个全新的世界的机会，银行，贷款，保险，汇款，投资和股票市场等待。然而，区块链大规模采用的潜力受到网络安全和隐私问题的阻碍。我们概述了风险和安全要求，并展望了未来的研究，这可能有助于解决一些挑战。我们还提出了一种基于智能合约的金融交易c2020年韩国通信与信息科学研究所（KICS）。出版社：Elsevier B.V.这是一个开放的访问CC BY-NC-ND许可证下的文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。关键词：区块链;安全策略;智能合约; 5G网络1. 介绍数字化转型是所有经济体和金融体系的持续趋势。根据华为牛津经济学报告据报道，全球经济的25%是数字化的，到2025年，这一数字估计将达到25%（23万亿美元）。数字经济预计将更具竞争力;投资回报率高，环境平衡，社会可及性和包容性，数字经济预计将提供新的变革机会。数字经济的未来，特别是在激烈的区域和全球竞争中，将取决于他们对强大基础设施的理解、准备和存在。数字经济包括有形数字资产和无形数字资产及其相关基础设施。无形资产（数据、知识、软件、知识产权、数字货币和代币等）一些国家的投资份额已达到∗通讯作者。电子邮件地址：dunal@qu.edu.qa（D.Unal），m. mmu.ac.uk（M.Hammoudeh），mehmet. dmu.ac.uk（M.S.Kiraz）。同行评审由韩国通信和信息科学研究所（KICS）负责https://doi.org/10.1016/j.icte.2019.07.002高达GDP的15%，数字经济这一部分的增长率正在上升[2]。各国监管机构和全球标准制定机构已经达成共识，认为区块链技术为社会和经济带来了巨大的新机遇。然而，区块链技术的不受控制的使用可能会加速社会经济问题，特别是洗钱、欺诈、网络犯罪和市场不稳定。区块链提出利用破坏性的加密货币应用潜力，不仅可以抵消其负面可能性，还可以抵消这些创新的积极潜力5G技术带来的宽带移动互联网需要移动数字支付解决方案的补充。区块链是缩小这一差距的一种技术最近，各种硬件加密货币钱包提供商和智能手机制造商发布了手机硬件这一进展表明，将有大量的区块链交易通过5G网络进行。最近的一项研究[3]调查了区块链和网络安全之间的相互作用，并指出最关注安全的区块链应用是关于物联网，数据存储和共享，网络安全，用户隐私和互联网访问。所有这些应用领域也有望成为5G网络中采用区块链技术的驱动因素。2405-9595/2020韩国通信和信息科学研究所（KICS）。出版社：Elsevier B.V.这是一个开放的访问CC BY-NC-ND许可证下的文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。44D. Unal，M.Hammoudeh和M.S.Kiraz/ICT Express 6（2020）43在5G网络中实现区块链的各种安全问题包括，手机应用程序和操作系统的软件漏洞[4]，对热钱包的黑客攻击以将价值存入区块链，以及对区块链交易的安全策略执行不足。区块链上的安全策略执行由于终端用户设备的移动性和移动网络的多域性质，在移动网络环境中尤其具有挑战性。此外，由于公共区块链是每个人都可以访问的分布式账本，因此访问控制成为控制区块链上允许的操作的重要问题。最近，移动边缘网络中用于网络安全的区块链应用引起了研究人员的兴趣。在[5]中，作者提出了一种基于区块链的移动边缘计算（MEC）架构。在[6]中，作者提出了一个名为“EdgeChain”的物联网框架这条工作线很有趣，但它并不与我们提出的方法竞争。我们的方法可以在这样的框架中使用，用于规范和验证智能合约的策略。我们不知道以前在这方面有这样的工作在本文中，我们研究了5G网络中基于区块链的交易的安全问题，特别是在移动边缘。我们提出了一种在下一代移动网络中基于智能合约的交易策略规范和验证方法。我们的方法学不同于现有的工作，它是基于形式逻辑，并支持形式化验证的智能合约政策。本文的其余部分组织如下。第2节讨论了区块链的一些安全威胁和风险。第3节讨论通过安全策略规范和验证来遵守安全标准。第4节介绍了智能合约政策规范和验证的拟议方法。最后，在结论部分，对本文的研究方法进行了分析，并提出了进一步的研究方向.2. 支持5G的区块链的安全威胁和风险与区块链平台和技术相关的一些风险包括：洗钱是由于高度的匿名性，这使得监管机构难以识别使用该协议进行非法价值转移的个人。一些加密货币可用于洗钱目的，这对执行金融制裁构成了挑战。逃税可能是匿名的副作用。为了应对加密货币的全球现象，许多国家推出了各种加密货币税收计划。货币和金融稳定性的风险，包括对流通中货币数量的潜在失控，这可能导致通货膨胀-随着加密货币市场规模的增加以及经济中使用加密货币的信贷增加，这一问题将更加突出。对法定货币越来越不信任。法定货币和加密货币之间有许多相似之处。首先，加密货币是一种价值的数字表示，可以在网上交易，至少具有一些公认的货币功能;它作为价值储存、交换媒介和账户单位，但在任何法律秩序中都不具有法定货币地位。因此，加密货币的广泛使用以及与之相关的一系列新问题可能会反弹，破坏人们对传统货币的普遍信心。加密货币环境中的新中介机构可能会给消费者、金融机构和政府带来巨大风险。加密货币与法定货币、数字钱包服务提供商、支付系统和定价指数以及其他加密货币交易清算所的交易平台和交易所取代了传统的、通常是国家的金融中介机构，如中央银行和商业银行。新的中介机构面临着新的问题，例如黑客攻击的风险。截至撰写本文时，有许多加密货币黑客事件，其中最大的一次事件（Coincheck）损失约5亿美元[7]。2019年最新的黑客事件是针对币安的，损失超过4000万美元的资产，市场损失额外40亿美元。这些事件主要是由于安全策略执行不力和使用热钱包（连接到互联网的钱包）来存储用户数据而引起的。加密资产3. 遵守安全标准3.1. 现有安全标准和安全政策的遵守情况在通信和标准领域，最重要的探索领域之一是探索如何将金融领域的安全标准应用于5G网络中基于区块链的金融交易。主要目标这些标准的目的是保护客户数据免受可能的危害和威胁。例如，在金融部门，涉及接受、处理和存储支付卡信息的任何商业实体都需要遵守支付卡行业数据安全标准（PCI-DSS）。此外，对于通用软件，组织可以采用信息技术安全评估通用标准（简称为通用标准或CC-ISO/IEC 15408）进行计算机安全认证。对于策略合规性检查和验证，基于自动化工具的方法对于测试商业区块链应用和加密货币应用是有价值的。可以在广泛的正式领域内解决这个问题;从非常非正式的方法，例如基于场景的测试，到基于数学方法的非常正式的方法来证明软件的安全性。在本文中，我们将提出一个更正式的方法，也支持自动化。此外，所有这些标准····D. Unal，M.Hammoudeh和M.S.Kiraz/ICT Express 6（2020）4345Fig. 1. 安全要求过程。和方法需要用于互操作性和分析的结构化策略文档格式。因此，基于结构化策略声明并支持错误验证的智能合约安全策略规范和验证框架将是实现安全标准合规性的重要推动因素。3.2. 智能合约定义智能合约的安全要求是解决安全风险的必要条件，也是一个重要组成部分的风险解决。从标准合规性的角度来看，安全要求在许多标准中是强制性的，例如ISO 27001控制项14.1.1（信息安全要求分析和规范）[8]。安全策略也在安全需求过程中定义在图1中，我们提供了安全要求流程的概述。在安全要求过程中需要考虑的区块链环境中的一些资产是：分布式账本、信息资产、业务规则、服务和功能、源代码、知识产权、加密密钥、有关人员及其能力的信息、账户信息以及与账户和交易日志相关的资金。在这方面，我们确定了5G网络中金融交易区块链的关键安全要求的一些示例，如下所示：功能安全要求：FR-2访问控制FR-3智能合约非功能性安全需求：NFR-1数据保护NFR-2移动性和基于位置的接入结构化策略规范4. 我们的方法：智能合约对于智能合约进行的每笔交易，都需要通过形式化分析来检查单个策略以及策略之间正式图二. 5G网络中智能合约的策略合规性检查和验证的总体方法智能合约策略的建模和分析需要智能合约策略的正式模型和语言智能合约的安全策略由系统的代理（用户和智能合约）、事件和对象组成;它旨在定义允许和禁止的行为。定义安全策略规则时，有两类约束：1. 用户和智能合约在对对象执行操作时必须满足的约束。2. 用户和智能合约在与其他用户和智能合约交互时必须满足的约束责任、授权、等级权力）。在5G网络环境中对智能合约策略进行形式化和验证的完整建议流程如图所示。二、在所提出的流程中，首先通过网络和服务发现从5G网络获得网络和服务配置。配置文件、智能合约规范和安全性46D. Unal，M.Hammoudeh和M.S.Kiraz/ICT Express 6（2020）43∈}={∈={∈ ∈}|⋄|∧|====-∧|=--策略规范被输入到正式规范生成器，该正式规范生成器生成正式授权条款和约束。然后将正式规范输入到正式验证器，正式验证器生成策略遵从性报告。在下面的小节中，我们将介绍一些示例策略声明，并解释如何正式指定和验证这些声明的合规性。形式化和验证方法基于FPM-RBAC模型[9]。因此，我们首先简要介绍一下如何在此模型中指定安全策略规则4.1. FPM-RBAC中的形式化安全策略规则FPM-RBAC中的安全策略规则是通过一个授权项结构来定义的，它是形式化规范的基础。FPM-RBAC中的授权术语集定义如下：AT（as，ao，act，co，fo）：as AS，ao AO，act ACT，（co，fo）C。这里，AS是可以对授权对象进行操作的授权主体的集合。 AO是授权对象的集合，或者等价地，授权主体在其上执行操作的资源。服务定义本质上是资源的子集。ACT表示智能合约可以执行的一组操作，例如读、写、存款或取款。约束定义了执行操作必须满足的条件 智能合约。C定义了在移动网络中执行智能合约的约束集合，其中C（co，fo）：co PL，fo AL。谓词逻辑（PL）中规定了服务访问、域和用户组成员资格、移动网络访问等通用条件。基于位置和时间的策略约束通过在环境逻辑[10]（AL）中指定的位置公式（fo4.2. 在5G网络中使用智能合约的场景我们现在定义一个虚拟场景，用户可以从家中、智慧城市和工作中的多个无线网络访问她的加密钱包。该场景符合5G网络架构，其中多种无线网络接入技术将集成在基于云的基础设施和基于服务的计算上。用户Alice对于在她移动时从不同位置在家里，她有一个5G移动网络连接。在她在家的时候，她需要照顾她年迈的母亲和年幼的孩子，因此她有一个共享的加密钱包，可以由日托专业人员访问，以便在她的控制下进行必要的支出在智慧城市周围，她使用手机从日常加密钱包中支付交通、医疗保健和其他日常交易等服务。在工作中，她可以访问她的投资加密钱包，在那里她存储和出售各种加密代币用于长期投资，并将必要的金额转移到她的其他两个钱包。该场景建立在多域移动网络架构上，并将通过5G技术提供的无缝连接而成为可能。然而，通过智能合约进行的加密资产上的金融交易需要受到访问控制，并且应该结合指定的策略来验证操作。特别是验证是必要的，因为区块链上的交易一旦记录在区块链上就不可变。4.3. 安全策略声明对于第五代移动网络的融合网络架构，智能合约结构化策略规范需要支持基于位置和时间的策略以及服务访问策略。下面我们将介绍一些此类政策规则的示例。R1（基于位置的访问策略）：R2（基于服务的访问策略）“日托人员仅允许将加密资产用于家庭成员的医疗保健服务”R3（基于时间的访问策略）：4.4. 安全政策声明在这一节中，我们提出了正式的移动性，位置和基于时间的服务访问策略在前一节。对于形式化，我们使用FPM-RBAC形式授权条款。在这个模型中的移动性，位置和时间为基础的约束公式指定通过环境逻辑，这是一种形式的模态逻辑，能够指定基于位置和时间的移动性。在这个模态逻辑中，有三个结构特别有趣：Parallel（）、Somewhere（）和Sometime（）。并行构造指定同一位置的两个实体。somewhere构造指定位置内的任何实体。sometime构造指定流程的执行以在其执行期间满足时间约束。这些结构共同提供了一种强大的形式主义，可以为在各种5G网络域内执行的智能合约指定策略。上一节中策略规则的正式安全策略声明如下：R1：（as Alice，ao Shared Wallet，sa + deposit，coActiveDomainUser（as，Home Profile），fo AliceApartment [as[]] 5Gmobile Internet[as [] ao[]]）R2 ： （ 如达 凯 尔 岛Shared Wallet ， 美 国+withdraw ， co ActiveDomainUser （ as ， Home Profile ）ServiceUser （ as ， Healthcare ） ， UserGroup （ user 1 ，familymember ） ， fo Al- ice Apartment [as[] user 1[]]5Gmobile Internet [as [] ao[]]）R3：（as=*，ao=投资钱包，sa=+提款，co=ActiveDomainUser（as，Business Profile），允许的时间（营业时间），fo=as[]|ao[]允许的次数）···D. Unal，M.Hammoudeh和M.S.Kiraz/ICT Express 6（2020）4347|为|为4.5. 安全政策声明在我们提出的方法中，安全策略语句的验证形式规格说明是形式规格说明生成器的输出，由形式过程规格说明和形式策略规格说明组成。正式流程规范代表网络和服务配置的状态以及智能合约规范。正式的策略规范由上一节介绍的正式的安全策略声明组成。为了检查在服务和网络配置的给定状态下是否满足策略语句，需要计算基本上是结构化同余关系的这是通过模型检查器实现的。模型检查器检查P是否A（过程P满足公式A）。形式化过程规范表示为P，形式化策略声明中的约束表示为A。当流程规范P中的所有策略规则都得到满足时，我们可以得出结论，给定服务和网络配置中的智能合约执行符合策略。该模型检测器已用Java语言实现。空间逻辑语句在Ambient Calculus模型检查器中进行验证。时态逻辑语句被转换为NuSMV时态模型检查器语句，随后使用NuSMV模型检查器进行验证。5. 结论在本文中，我们提出了一种在5G网络中对智能合约进行策略合规性检查和验证的方法。我们的方法建立在正式规范语言和通过模型检查器验证的结构化策略规范。我们的工作补充了5G网络区块链领域的现有研究。竞合利益作者声明，本文中不存在利益冲突。引用[1] 华为公司和牛津经济学，数字溢出：衡量数字经济的影响，9月。2017. http ： //www.hkj.com/ 胡 阿 威 岛 com/minisite/gci/en/digital-spilover/index. HTML. 2019年5月30日访问[2] Jonathan Haskel，Stian Westlake，Capitalism Without Capital：TheRiseof the Intangible Economy ， Princeton University Press ，Princeton，NewJersey，USA，2018。[3] Paul J. Taylor ， Tooska Dargahi ， Ali Dehghantanha ， Reza M.Parizi，Kim-Kwang Raymond Choo，区块链网络安全的系统性文献综述，Digit。Commun. 网络（2019年）。[4] Douglas A. Ashbaugh ， Security Software Development AssessingandManagingSecurity Risks，CRC Press，2009，（第2.4章）.[5] Z. Xiong，Y. Zhang，L. Niyato，P. Wang，Z.当移动区块链遇到边缘计算时，IEEE Commun。Mag. 56（8）（2018）33-39.[6] J. Pan，J. Wang，A.海丝特岛阿尔克马尔岛Liu，Y.赵，边链：基于区块链和智能合约的边缘物联网框架和原型，IEEE InternetThings J。（2019年）。[7] How to Steal $500 Million in Cryptocurrency，Fortune Magazine，URL：http：//fortune. com/2018/01/31/coincheck-hack-how/。2019年5月30日访问。[8] ISO/IEC，ISO/IEC 27001，ISO/IEC，瑞士，2013。[9] D. 密 歇 根 大 学 尤 纳 尔 分 校 FPM-RBAC ： A formal role-basedaccesscontrol model for security policies in multi-domain mobilenetworks，ElsevierComput. 网络57（1）（2013）。[10] L. Cardelli，A.D. Gordon，Ambient logic，Math.Struct.Comput. Sci.（2006年）。