基于软件的1类物联网设备远程证明机制研究

欢迎大家来到IT世界,在知识的湖畔探索吧!

物联网在日常生活、医疗保健、农业等领域发挥着重要的作用。然而，在物联网中存在一个隐患：1类物联网设备，它们拥有支持因特网安全通信所需的最低限度的资源，但又缺乏安全硬件的保护，并且不支持任何的硬件修改或扩展，极易受到攻击。

因此，确保这些设备的安全并尽早检测它们是否遭到攻击显得极为重要。

远程证明

远程证明是一种挑战响应协议，由一个被称为验证者的可信实体远程验证被称为证明者实体的软件完整性。

验证者通常被默认为是可信实体，作为远程证明的发起者和决策者，验证者通常具有强大的计算能力，还拥有海量的存储能力，通常为大型服务器设备，具有安全硬件以及极强的自我防护能力。

证明者通常为不可信设备，它们具有较弱的计算能力和有限的存储空间，大多数设备均是不具备安全硬件的1类物联网设备，极易受到攻击，它们需要向验证者证明自身软件的完整性。

远程证明具有许多优势，包括灵活、可扩展、实现简单和成本低廉，通常只需要更新设备软件或添加少许的安全硬件即可实现大部分主流的远程证明方案。远程证明方案的主要过程如图所示。

对称密码体制

对称密码体制也被称为私钥密码体制，加解密采用的是相同的密钥，是最快速、最简单的一种加密方式。对称密码体制的优势在于计算量小、加密速度快，但也存在密钥管理复杂等缺陷。对称密码体制的具体流程如图所示。

从图中可以看出，在加密过程中，发送方会使用密钥对明文进行加密，之后将密文发送给接收方，接收方会使用同一密钥解密密文。

形式化分析工具：Tamarin

Tamarin是一个用来自动分析密码协议安全性的工具，可以建立无限验证、可变全局状态、归纳和循环引用。Tamarin内置了“Dolev-Yao”敌手模型，在该模型中，敌手能够完全控制通信网络，可以对公共信道中的消息执行窃听、修改和拦截等操作。

Tamarin提供了交互模式和全自动模式这两种构造证明的方法。如图2.3所示，当用户将协议和安全目标输入Tamarin后，Tamarin会对安全目标进行验证，在验证完成后输出验证结果。

在Tamarin模型中内置了哈希hashing、非对称加密asymmetric-encryption、签名signing、签名验证revealing-signing、对称加密symmetric-encryption等多个密码操作。

用户可以通过重写规则Rule来设定协议中所有实体的操作，并且使用安全属性lemma来描述协议的安全目标。Tamarin针对每个lemma都有两种验证结果：verified和falsified，verified表示协议满足该lemma，falsified表示验证失败，协议不满足该lemma。

基于软件的远程证明方案

本文的远程证明系统由四部分组成，管理中心、验证节点、证明节点和观测节点。其中各部分主要功能如下：管理中心：管理中心是网络的核心管理者，负责系统中所有节点的注册、密钥管理以及对验证节点的证明授权。

该中心具有极强的计算能力和海量的存储能力，具有安全硬件以及极强的自我防护能力，在远程证明中默认为可信设备。

验证节点：验证节点是远程证明的发起者，具有极强的计算能力和海量的存储能力，具有安全硬件以及极强的自我防护能力，以及较高的时间精度。在远程证明中默认为可信设备。

证明节点：证明节点是方案中向验证节点证明自身软件完整性的一方，缺少安全硬件的支持。通常为1类物联网设备等资源受限的物联网设备，计算能力和存储空间有限，在远程证明中默认为不被信任的一方。

观测节点：观测节点和证明节点属于同一类型的节点，验证节点在远程证明请求阶段选择它来观测网络延迟。同样也缺乏安全硬件的支持。

无线网络环境下代理攻击的应对

远程证明流程通常由验证节点发起，验证节点会生成校验和挑战并发送给证明节点，证明节点在收到挑战后会根据自己的内存空间内容计算校验和响应，计算完毕后将响应发回给验证节点进行验证。

但是，对于受到了攻击的节点来说，通常会被置入恶意代码，导致在远程证明过程中无法计算正确的校验和响应。

通常在这种时候攻击者会选择使用代理攻击作为解决方案，即会在集群周围放置一个代理节点，它具有比证明节点更强的硬件配置，如更大的内存空间，更高性能的处理器。

代理节点会存有证明节点所有内存空间的内容，以及证明节点的密钥等隐私数据。下图展示了一个代理攻击的完整过程。

从图中可以看出，在进行代理攻击时，证明节点会将来自验证节点的校验和挑战转发给代理节点，由代理节点根据记录的证明节点内存内容计算正确的校验和响应，再发回给证明节点，最后由证明节点转发给验证节点，从而达到欺骗验证节点的目的。

代理攻击是远程证明中最为棘手的攻击之一，通常只有基于严格的时间控制的这类远程证明方案能有所应对，但是对于存在随机网络延迟的无线网络环境，由于没有考虑到延迟耗时的因素，现有的这类方案也失去了其作用。

为了有效抵御代理攻击，本文采用了VIPER方案中的思路，并且将应用场景扩展至无线网络环境下。

对于代理攻击来说，只要令恶意节点执行代理攻击流程的时间开销大于节点正常执行远程证明流程的时间开销，就会产生一个可被检测到的时间差，从而辅助方案判断证明节点是否在进行代理攻击，这是本文抵御代理攻击的核心思路。

分析了验证节点、证明节点和代理节点在远程证明中的各自时间线，其中在执行代理攻击时，证明节点和代理节点的行为均会有所改变。在方案模型中增加了无线网络中特有的网络延时，并且引入了观测节点对网络延时进行评估。

方案实现

为了开发和测试本文提出的基于软件的远程证明方案，本文使用了UNO-R3来进行实现，这是一个由ATmega328p微控制器构成的物联网开发板，运行频率为16MHz，随机存取存储器大小为2KB，闪存大小为32KB，具有9600-的波特率。

本文将它作为证明节点和观测节点。至于验证节点和代理节点则由一台搭有Interi59400CPU、500G固态硬盘的主机担任。

远程证明由验证节点发起，证明节点在收到校验和挑战后立即转发挑战至代理节点处。为了证明本方案在最极端场景下的适用性，本文赋予代理节点无穷大的算力，即代理节点会在收到校验和挑战后立马返回预置的校验和响应，无需进行计算。

验证节点在收到校验和响应后会立刻向观测节点发送延迟观测请求，并且记录收到的响应时间。在实现过程中令所有节点在发送数据包前随机休眠一段时间来模拟网络延迟场景。

经过测试发现，使用校验和函数一次验证所有的内存需要花费9.244ms，验证节点发送8字节数据，证明节点收到后不做任何处理，立刻返回相同的数据，再由验证节点收到这一过程共花费约4.1ms，执行一次AES加解密共花费0.9ms。

下图是在无网络延迟情况下，证明节点执行代理攻击时，设置不同的校验轮数，所获得的证明节点的延迟与观测节点的延迟的对比。可以看到，为了能检测到代理攻击，至少需要分四轮完成校验和请求过程。

形式化验证分析工具Tamarin

为了进一步证明本方案的安全性，本文使用了一个非常著名的形式化验证工具Tamarin对所提出的方案进行形式化安全分析。该工具可以精确分析各种协议的保密性和认证等特性。Tamarin工具还支持一些密码算子的等式指定，例如Diffifie-Hellman取幂和双线性对。

在一台搭有Interi59400CPU、500G固态硬盘的主机上进行Tamarin验证，操作系统为Ubuntu18.04，运行在虚拟机上。

仿真中编写了两个实体：验证节点和证明节点。仿真模拟了本方案的认证阶段中的全部通信流程、加解密过程、HMAC校验等操作。

通信流程结束后，仿真对本方案中使用的加密密钥EK和完整性密钥IK的安全性进行了验证，同时验证了本方案的存活性、弱一致性、非单射一致性、单射一致性。本方案的Tamarin验证结果如图所示。

其中secrecy_EK以及secrecy_IK用于证明加密密钥EK和完整性密钥IK的保密性，aliveness用于证明方案的存活性，weak_agreement用于证明方案的弱一致性，noninjective_agreement用于证明方案的非单射一致性，injective_agreement用于证明方案的单射一致性。

从图中可以看出，加密密钥EK和完整性密钥IK在协议过程中不存在被泄露的风险，证明本方案能够保障密钥安全。

方案的单射一致性验证通过，证明协议具有抵抗重放攻击的能力。同时方案的存活性、弱一致性、非单射一致性均能验证通过，证明本方案能够实现验证节点和证明节点的双向认证并抵抗多种协议攻击。

方案实现

为了实现和验证本文提出的基于时钟偏差的设备指纹认证方案，本文使用了UNO-R3物联网开发板进行实现，它含有一个ATmega328p微控制器，运行频率为16MHz，随机存取存储器大小为2KB，闪存大小为32KB，具有9600-的波特率，本文将它作为证明节点。

至于验证节点则由一台搭有Interi59400CPU、500G固态硬盘的主机担任，主机的操作系统为windows10。验证节点和证明节点之间通过串口进行连接通信，双方的波特率均设置为。

验证节点的协议则选择使用C语言进行开发，为了获取相对精确的时钟偏差，需要有较高的时间精度，因而方案定义的精度需求为微秒级别，验证节点可通过windows中基于CPU级的方法来获取精确的当前时间。

结语

本文研究了在无线网络环境下，1类物联网设备在远程证明中遇到的挑战，针对远程证明中遇到的常见攻击，尤其是代理攻击展开了研究。还通过引入设备指纹来对远程证明仅能验证软件完整性，而无法认证设备身份的缺陷进行了弥补。

本文提出了一种新的基于软件的远程证明方案，可以适用于所有物联网设备，尤其适合于资源受限的1类物联网设备。本文在远程证明中提出延迟观测机制从而解决了传统的基于软件的远程证明方案无法应用于无线网络环境的限制。

通过执行多轮校验和挑战从而解决了代理攻击的问题。同时本文提出了一种证明时填充机制，对所有的存储器（RAM，ROM，EEPROM）都进行填充并认证从而解决通过返回导向编程隐藏恶意代码的攻击。

本文提出的方案预计能适用于所有物联网设备，尤其是针对资源受限的1类物联网设备会具有显著的优势。同时考虑到集体远程证明的需求，在集群网络环境畅通的情况下，本方案对集体远程证明具有一定的适用性。

但是由于网络拥塞和网络延迟的影响，随着集群中设备数量的增加，对网络环境的要求也会随之提高。