0x00 Abstract
人们对使用区块链解决当今复杂系统中存在的物联网安全性和可信赖性问题的兴趣日益浓厚。区块链通过提供分布式防篡改账本来实现对等网络的信任。但是这两种新兴技术的结合可能会产生新的问题和漏洞，攻击者可能会滥用这些漏洞。
本文中旨在研究轻量级可扩展区块链（LSB）的信任机制（LSB是一种专门为物联网网络设计的区块链），以表明区块链架构中的恶意参与者有可能进行On-Off攻击并降低分布式分类帐本的完整性。选择一个远程软件更新过程作为代表此攻击的例子。最后提供了受攻击系统的模型并验证了所描述的攻击场景。
0x01 Introduction
物联网（IoT）的概念已使各种物理设备（例如传感器，调节器，移动电话等）通过互联网进行交互，以达到一个共同的目标，例如提高效率、可扩展性、用户灵活性和满意度，同时有可能降低系统开发和维护成本。预计在不久的将来，将有超过500亿个设备连接到互联网，支持智能城市、智能住宅、自动驾驶汽车、精准农业等几种不同的应用。但是考虑到异构性、复杂性和面临不同威胁的可能性，安全性成为此类系统中的关键问题之一。
区块链是一种基于密码的分布式账本技术，它利用对等（P2P）网络通信来实现不受信任的通信参与者之间的受信任的通信。区块链中的所有交易都记录为区块链，并由所有网络参与者在没有中央权限的情况下使用分布式密码协议进行管理。在这种情景中，所有参与者都需要验证要附加到区块链的信息。近年来区块链技术由于其引人注目的特性（包括信任和安全特性，去中心化，匿名性等）而成为了研究的热点，从而吸引了在银行、智能合约、智能城市以及网络安全、尤其是在物联网的关注。
尽管可以将其视为改善IoT设备安全性、信息保护和可靠性的一种有前途的方法，但它也带来了一系列新的挑战，例如如何在区块链中选择合适的共识机制。区块链中使用的共识机制使新生成的区块难以篡改之前区块的哈希值。共识机制包含规则和验证程序，以验证提供的数据并使网络参与者能够将数据放入区块链中。关于区块链需求，存在各种共识机制，例如工作量证明（PoW）或权益证明（PoS）。
PoW要求每个参与者节点提供证明，证明其完成和提交的工作使该节点有资格获得向区块链添加新交易的权利。该过程依赖复杂的数学计算，因此既昂贵又耗时，但是一旦完成，其他参与者就可以轻松地验证解决方案。另一方面，当维护公共账本到每个节点时，PoS涉及一个责任分配过程，该账本与其持有的虚拟货币代币的数量成比例。由于共识机制是区块链设计的核心组成部分，因此选择共识机制会对性能，可扩展性以及安全性产生影响。
由于与共识机制的选择有关的资源密集型过程，因此区块链技术本身在计算上是昂贵的。由于它不能很好地扩展，可能会引入相当大的带宽开销和可能的延迟，这对于物联网来说是不可接受的，因此提出了一种新颖的轻量级可扩展区块链（LSB）框架。在文中选择在物联网的背景下评估这种方法的适用性，重点是挖掘潜在的漏洞。使用建模语言Rebeca，在远程软件更新的示例中提供了LSB算法模型，并介绍了一种特定类型的攻击，称为On-Off攻击。此外使用支持模型检查工具来验证感兴趣的属性并显示LSB中可能的攻击行为。
0x02 Related Work
在本节中提供有关文献的概述，重点在于如何利用建模方法来验证不同区块链技术平台的安全性要求。从对比特币协议建模的一些相关工作进行回顾，其中评估方法与本文的工作类似。
Beukema等[1]提出了一种以mCRL2语言形式的比特币协议的形式化模型，作为中介之间的过渡系统。所分析的模型包含网络的行为，并显示当消息损坏和双花攻击发生时共识协议的行为。后来，巴斯蒂安等[2]提出了对比特币协议的随机分析，并通过连续时间马尔可夫链提供了一个模型。他们的主要贡献是对挖掘算法的分析以及防止51％攻击的解决方案。
Ellervee等[3]提出了一个综合的模型来描述区块链，使用诸如参与者、角色、服务、流程和数据模型之类的属性。他们建立了一个模型来指导业务分析师并帮助他们与开发人员进行沟通。他们在包括比特币，MultiChain，以太坊和Chain Core在内的四个区块链技术平台之间进行比较，从而明确了解了该技术及其工作流程。
一种名为UPPAAL SMC [4]的模型检查方法可以对具有随机语义的复杂实时系统的网络进行推理，它还可以对比特币协议进行一些分析。 Chaudhary等[5]研究UPPAAL SMC对比特币协议的正确性。他们计算与攻击者的计算能力有关的两次花费攻击的成功概率。该工作检查了比特币协议并将其形式化为UPPAAL模型，结果表明在最长的链中插入假交易的可能性取决于确认的数量。此外，Fehnker等[6]分析了攻击者需要多长时间才能成功创建分叉并将主链拆分为区块链。他们的工作表明，百分之二十的网络矿工的算力足以使攻击者在几天内实现目标。
Kosba等[7]使用形式化方法验证隐私属性，并提出了用于编写智能合约的编程语言Hawk。 Hawk是用于构建保护隐私的智能合约的框架，程序员可以在其中无需实现任何加密就轻松编写Hawk程序。 [8]专注于智能合约的语言并分析漏洞，表明存储在区块链上的不同实体智能合约可能会受到攻击，并可能导致财务损失。Bhargavan等[9]提出了一个框架，将以太坊中的智能合约转换为Solidity代码的子集，并进行分析以发现缺陷。
0x03 Background
在本节中介绍所需的必要背景。首先介绍区块链的概述，重点是轻量级可扩展区块链（LSB），这是一种用于IoT安全的区块链解决方案。对Rebeca建模语言进行简要描述，该语言将在本文中用于建模和验证对LSB进行On-Off攻击的示例。
A.轻量级可扩展区块链（LSB）
区块链是一种分类账本，分布在以P2P设置组织的多个节点中。每个节点都有一个分类帐的副本，并独立更新。分类帐本内容由一组块组成，这些块通过加密哈希值链接在一起。每个块记录一组交易。为了确保所有分类账本实例中的交易顺序相同，网络参与者使用共识机制。通常只有很少的节点具有足够的处理和存储能力来实施共识机制。这些节点称为矿工。
LSB是专门为物联网网络设计的区块链。由于典型的区块链共识机制需要很高的计算能力，这使其很难在物联网中使用。为了解决这个问题，Dorri等人[10]提出了一种基于时间的块生成算法。在这种算法中允许每个矿工在给定的时间段内向分类账本添加一个以上的块。此外为减少开销，将IoT节点进行群集化，群集头（CH）负责验证交易和挖掘区块。通过使用分布式信任算法，CH减少了验证事务所需的计算时间。
所提出的算法依靠直接和间接的证据来评估矿工的可信度。这些证据是通过研究每个矿工的先前行为来收集的。如果先前的行为表明某个矿工在某种程度上可以被信任，则其他矿工可以跳过对该矿工验证的某些交易的验证。跳过的交易的确切数量记录在所有矿工维护的表中。
为了说明起见，假设一个CH节点A验证了一个CH节点B生成的块。这时，该节点A具有关于该节点B的直接证据，并且根据验证结果，它可能会增加或减少其现在，假设在验证之前，已通知节点A某些其他CH节点已将该块签名为有效。基于此，节点A使用此信息作为有关节点B的间接证据。上表显示了一个信任表示例，该表将肯定证据的数量映射到应验证的交易百分比。
B. Rebeca建模语言
Rebeca是一种基于行为者的建模语言，具有形式化基础，可用于通过异步消息传递对并发和响应系统进行建模。 Rebeca模型由反应性类的定义和称为main的实例化部分组成。主要部分定义了反应式类的实例，称为rebec。rebec的行为由其消息服务器确定。
在Rebeca中，计算是由事件驱动的，这些消息可以被视为事件。每个rebec从其消息队列中获取一条消息并执行相应的消息服务器。通信是通过异步消息传递进行的，这对于发送者和接收者而言都是非阻塞的。 Rebeca模型的行为定义为并行执行rebec的已发布消息。 Rebeca具有形式化语义，使其适合用于模型检查。此外该语言使用不同的抽象技术来保留时间逻辑中的行为规范，同时减少模型的状态空间并验证所需的属性。
0x04 On-Off Attack Scenario
在On-Off攻击中，假定恶意节点首先以诚实的方式行事以赢得其他节点的信任，然后再发起攻击。由于大多数信任模型都将重点放在当前节点的行为上，而不是检查过去和最近的节点活动，因此它们容易受到On-Off攻击的影响。结果，恶意节点可以通过显示为诚实节点或保持空闲一段时间来增加其信任值，从而轻松隐藏不当行为历史记录。在本节中详细介绍了针对Dorri等人提出的分布式信任算法的On-Off攻击[11]。
请注意，考虑了节点的当前行为，而节点可以经常将其行为从良性行为更改为恶意行为，反之亦然。假设恶意节点在以下三个阶段中行为。
1）良性行为：恶意节点通常会生成新的有效块以赢得高度信任。
2）恶意行为：诚实行为一段时间后，恶意节点的信任率达到最高值。之后，恶意节点滥用信任率在构建新块时插入假交易。
3）等待期：如果成功插入了假交易，恶意节点将不执行任何操作。
在等待期间，只要其他节点检测到恶意行为，恶意节点就会再次开始表现良性以赢得他们的信任。可以基于信任表中提供的映射确定检测的可能性。考虑到表中的映射，假设恶意节点在第一阶段生成了50个块。此节点生成的事务中只有20％会被其他节点验证。
由于存在此漏洞，很少有恶意节点可以通过定期遵循上述情况，直到将伪造交易放入分布式分类帐本中，才能对系统进行大规模攻击。
应对攻击的常用缓解技术引入了一个因素，该因素考虑了节点在一段时间内执行操作的权重。换句话说，仅考虑测得的不当行为的权重，而不考虑不当行为的周期性。在[12]和[13]中，作者定义了一种自适应遗忘方案和一种惩罚策略，其中这些组件需要长时间的交互和一致的良性行为来建立信任。
在下面的示例中，展示了三个诚实节点中的恶意节点如何干扰物联网系统的完整性。在这里以远程软件更新（RSU）流程为例。该过程利用LSB的安全性和可扩展性优势来确保存储在分布式分类帐本中的软件二进制哈希的完整性。假定在这种情况下将涉及以下组成系统：智能车辆，原始设备制造商（OEM）和服务提供商（SP）。它们一起构成了P2P网络上的分布式分类帐的结构，使它们能够相互通信。
在下图所示的四个节点中，不诚实的服务提供者充当恶意对等方，并运行On-Off攻击方案。当信任率达到最高值时，该节点将更改其行为，并将生成的带有假交易的块广播到网络。虚假交易包含有害二进制代码的哈希，该哈希已经作为新近更新的软件包保存在云存储中。
云存储是区块链管理数据更改和真实性的地方，使智能汽车可以直接下载更新的软件版本。如图所示攻击执行如下：
1）Node1诚实工作，提高了信任度。
2）Node1将有害更新上传到云存储。
3）Node1将有害代码的哈希值作为事务插入到块中，并将受感染的块广播到其他节点。
4）Node2，Node3和Node4接收该块并随机验证该块的一部分。如果节点未意识到欺诈行为，则将存储该块。
5）被感染的区块存储在区块链中，节点将新更新通知智能汽车。之后，智能汽车开始下载有害软件包。
0x05 Modeling Distributed Ledger Components
在本节中描述了On-Off攻击场景的Rebeca模型，设计的Rebeca模型可以检测LSB中的恶意行为。此模型包括远程软件更新过程中涉及的CH节点的行为。
如上包含一个概述的Rebeca模型，该模型由两个参与者组成：OEM和MalSp。 OEM是LSB的CH节点，负责构建一个块并将该块广播给其他OEM。MalSp也是LSB的CH节点，并且适当地构建块以找到插入假交易的机会。 OEM和MalSp都将事务存储在挂起的池中，并在池的大小等于确定的大小时构建一个块。
该模型使用消息服务器声明参与者的实例。参与者之间的协作使通过将消息传递到消息服务器来存储事务成为可能。为OEM和MalSp参与者定义了buildblk( )，addtoBC( )和ack( )消息服务器。 OEM的buildblk( )正确遵循共识和信任算法，从挂起的池中获取事务并构建一个新块。但是，MalSp的buildblk( )在构建新区块时会检查信任率，以找到利用分布式信任算法的机会，并将受感染的区块传输到区块链（即具有至少一个假交易的区块）。
对于信任度，MalSp的行为与OEM行为相同，直到其信任度变得足够高为止。 OEM和MalSp都具有addtoBC( )消息服务器来验证块中的事务。该消息服务器接收广播块并进行块验证过程。如果区块验证成功完成，则可以将有效区块存储在区块链中。块生成器必须通过消息由块验证状态组成。 ack( )消息服务器通过发送确认消息来通知块生成器，以显示将块追加到区块链的确认。
为了对Rebeca模型进行建模，需要定义要验证的属性。旨在检查插入到区块链中的所有交易是否有效。在Rebeca模型中，区块链被定义为区块列表，其中每个区块记录为一个8元组（MinerID，BlockID，GenID1，TxID1，GenID2，TxID2，GenID3，TxID3），其中：
•MinerID指定已生成区块的矿工的ID。
•BlockID是区块链中区块的ID。
•GenID1是第一个事务生成器的ID。
•TxID1是第一个事务的ID。
•GenID2是第二个事务生成器的ID。
•T xID2是第二笔交易的ID。
•GenID3是第三个事务生成器的ID。
•TxID3是第三笔交易的ID。
例如，在Rebeca模型中，块[3、4、2、3、2、4、2、5]包含该块，事务和生成器的标识号。标识号为3（[3，∗，∗，∗，∗，∗，∗，∗，]）的CH节点从挂起的池中获取标识号为3到5的事务并构建块（[∗，∗， ∗，3，∗，4，∗，5，]）。
4表示此区块位于区块链的第二个链中（[∗，4，∗，∗，∗，∗，∗，∗，]）。这些事务由标识号为2（[∗，∗，2，∗，2，∗，2，∗，]）的节点生成。
上图显示了一个示意图，该示意图描绘了导致攻击场景参与者之间的一种可能的交互方式。根据此图，MalSp滥用最高信任率并调用buildblk(B)来构建受感染的块B。MalSp要求OEM1验证区块B，并通过addtoBC(B)消息服务器将其附加到区块链。OEM3间接链接到MalSp，并且需要验证块B。
因此，OEM3从OEM1获取消息addtoBC(B)进行验证。根据与MalSp相关的信任率，OEM1和OEM3随机选择块B的一部分进行验证，并通过发送ack(B)来显示成功验证的块来通知MalSp。OEM2接收addtoBC(B)并将消息传输到OEM3。 OEM3和OEM2都通过ack(B)响应。
假定信任率是最高值，则在OEM验证该块时，将忽略块B中的大多数事务。在OEM1，OEM2和OEM3均未检测到虚假交易的情况下，MalSp会通过接收最后一个ack(B)来通知MalSp附加到区块链的受感染区块（区块B）。
上面的断言定义为一个属性，用于检查在块验证过程中忽略哪些事务。每当所有OEM忽略假交易时，断言都会失败，并将此事件指示为反例。
如果在区块链中插入了至少一个虚假交易，则预期Rebeca模型检查器会生成一个反例，该反例违反所描述属性的情况，上图显示了有和没有假交易的区块链。图左展示了没有假交易的区块链，图右展示了上面讨论的Rebeca模型的反例。 BC是为区块链定义的8元组列表。
区块链必须在每个OEM中存储相同的有效区块。仅以OEM1.BC为例，OEM2和OEM3的BC与该BC相似。因此，MalSp插入编号3的第5块中的编号为10的交易是假交易。鉴于此，Rebeca模型演示了LSB中的漏洞导致成功的On-Off攻击的情况。设计的Rebeca模型的细节已上载并在GitHub [14]上可用。
0x06 Conclusion and Future Work
有大量现有的工业系统正在探索向物联网扩展的可能性。由于设备资源受限、不支持这种转换的标准或缺少适用于这种设置的合适的软件和硬件解决方案，因此此类系统中的主要问题之一是确保安全和信任，此外还必须考虑到安全性的动态性质，其中环境的变化和这种复杂系统中的交互可能会引入可能不会发生的对安全性至关重要的情况。
减轻此类挑战的方法之一可以在基于轻量级基于区块链的解决方案中找到，该解决方案用于资源受限的IoT设备（例如LSB）。LSB致力于通过使用分布式信任管理来提高安全性，同时减少带宽，缩短处理时间并实现无延迟服务。
本文中，在物联网架构的背景下研究所提出的方法，并以车辆领域的实例为例。使用Rebeca对方法进行建模，目的是在可能的攻击环境下探索LSB的适用性，重点是On-Off攻击。展示了如何将Rebeca用作评估分布式环境中安全属性的适当测试工具，并提供富有成果的分析。它也可以轻松地用于对涉及不同代理的复杂场景进行建模。
在将来的工作中计划在建立对分布式网络的信任时对不同的策略进行建模，并展示如何利用该模型来检查不同的缓解技术以减少发生攻击的可能性。目标是找出在值得信赖与提高性能之间进行权衡的情况下，在不同配置中遭受攻击的可能性。此外期待着将工作扩展到检查区块链正在使用的基础设施的安全性条款和功能。在这种情况下重点将转向关注对象互联网和网络物理系统的应用程序示例。
Reference
[1] W. Beukema, “Formalising the bitcoin protocol,” in 21th Twente Student Conference on IT, 2014.
[2] M. Bastiaan, “Preventing the 51%-attack: a stochastic analysis of two phase proof of work in bitcoin” in Availab le at http://referaat.cs.utwente.nl/conference/22/paper/7473/preventingthe-51-attack-a-stochasticanalysis-oftwo-phase-proof-of-work-in-bitcoin. pdf,2015.
[3] A. Ellervee, R. Matulevicius, and N. Mayer, “A comprehensive reference model for blockchain-based distributed ledger technology.,” in ER Forum/Demos, pp.306–319, 2017.
[4] A. David, K. G. Larsen, A. Legay, M. Mikucionis, and D. B. Poulsen, “Uppaal smc tutorial”,International Journal on Software Tools for Technology Transfer, vol. 17, no. 4, pp. 397–415, 2015.
[5] K. Chaudhary, A. Fehnker, J. Van De Pol, and M. Stoelinga, “Modeling and verification of the bitcoin protocol,” arXiv preprint arXiv:1511.04173,2015.
[6] A. Fehnker and K. Chaudhary “Twenty percent and a few days–optimising a bitcoin majority attack” in NASA Formal Methods Symposium, pp.157-163,2018
[7] A. Kosba, A. Miller, E. Shi, Z. Wen, and C. Papamanthou, “Hawk:The blockchain model of cryptography and privacy-preserving smart contracts”,in 2016 IEEE symposium on security and privacy (SP),pp. 839–858, IEEE, 2016.
[8] L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” in Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pp. 254–269, ACM, 2016.
[9] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi,G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote,N. Swamy, et al, “Formal verification of smart contracts: Short paper”in Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 91–96, ACM, 2016.
[10] A. Dorri, S. S. Kanhere, R. Jurdak, and P. Gauravaram, “Lsb: A lightweight scalable blockchain for iot security and privacy”,arXiv preprint arXiv:1712.02969, 2017.
[11] A. Dorri, S. S. Kanhere, and R. Jurdak, “Towards an optimized blockchain for IOT” in Proceedings of the second international conference on Internet-of-Things design and implementation, pp. 173–178, ACM,2017.
[12] Y. L. Sun, Z. Han, W. Yu, and K. R. Liu“Attacks on trust evaluation in distributed networks,” in 2006 40th Annual Conference on Information Sciences and Systems, pp. 1461–1466, IEEE, 2006.
[13] N. Labraoui, M. Gueroui, and L. Sekhri, “On-off attacks mitigation against trust systems in wireless sensor networks,” in IFIP International Conference on Computer Science and its Applications, pp. 406–415,Springer, 2015.
[14] F. Moradi, “On-off attack actors model,”https://github.com/fereidoun-moradi/On-Off-Attack, 2019.