物联网通过实时感知现实世界的各类数据,利用网络连接物理和虚拟对象,被广泛应用于商业领域(如工业物联网、智能家居等)和国家安全应用领域(如关键基础设施、军用物联网等),其中的安全问题尤为重要。研究物联网的安全,需要从系统的设计阶段开始,推进不同服务和业务流程的安全性设计及验证,实现多学科领域的交叉协作。模型检测作为形式化方法的一种,是基于严格推理和证明的数学方法,对系统的描述及刻画有严谨的语法语义,在性质验证时可由模型检测工具自动实现。针对物联网系统具有的实时性、并发性、大规模等特点,使用基于时间自动机的模型检测方法进行形式化分析,能够对这类复杂实时系统的逻辑流程与蕴含性质进行有效的建模、刻画及验证。在已有的研究工作中,将模型检测与物联网安全相结合,还存在以下几个研究难点:1)目前的物联网模型框架中,部分安全策略缺乏严格的证明推导,需要提出易于使用建模语言和逻辑公式进行描述的物联网安全建模方法。2)针对物联网系统进行抽象建模分析,其大规模状态及并发执行会引发状态空间爆炸,需要有相应的技术手段来保证模型验证的有效性。3)精确加速能够缓解状态空间爆炸,但现有方法在复杂实时模型中可能无法实施,需要提出一种能够应用于复杂实时系统模型检测的精确加速方法。为了解决上述问题,本文研究了物联网安全建模及其精确加速原理,主要研究内容与创新点如下:1)结合模型检测理论,研究基于时间自动机的物联网安全建模方法。服务计算能够对物联网安全服务的异构性进行解析,提出一种基于安全需求的物联网建模框架,可以将物联网系统的概念层次划分为服务、环境和安全需求,并描述相互之间的关联。在此基础上研究物联网安全的形式化建模方法,制定了基于行为规约的建模原则,并利用IoTSML语言进行具体实现:以时间自动机建模服务和环境,使用时序逻辑刻画安全性质,最后利用模型检测工具验证安全性质。2)为了缓解状态空间爆炸问题,研究精确加速原理,提出可加速环窗口的计算算法。精确加速原理的应用前提是可加速环窗口的大小,通过对精确加速原理的分析,提出可加速环窗口的计算算法,能够对识别出的可加速环进行精准压缩,约减与验证无关的状态和时钟,部分缓解状态空间爆炸。算法选择环内入边有时钟复位的任意节点作为起始,根据精确加速原理获取位置不变式、边界约束、时钟复位等数据,约减节点规模形成新的可加速环;通过新环能够直接计算窗口的大小,避免了人工推演,优化了模型验证时的时间和内存。3)对复杂的物联网系统进行形式化分析,研究基于覆盖环的复杂实时模型检测精确加速方法。原有的精确加速方法适用于单一的可加速环模型,若应用于复杂实时系统中,需要增加大量额外状态或时钟带,导致物理内存不足而无法进行验证。针对这一问题,提出一种基于覆盖环的精确加速方法,通过分析多个可加速环之间的加速效果差异,选取加速效率最高的可加速环进行抽象,构造单一的、长度固定的覆盖环。所构造的加速自动机模型不用依赖每一个可加速环窗口,能有效降低时空的开销,并能够验证复杂实时系统模型。4)将物联网安全建模方法和精确加速原理应用到两个实际案例中,验证所提方法的高效性。(1)研究工业物联网中的工业控制系统,通过对工控系统的控制过程进行建模,能够提取恶意代码的安全规约性质;根据验证给出的反例,能够判定恶意代码的行为,有助于对系统安全的缺陷进行提升。针对工控系统中的所有可加速环,使用可加速环窗口计算算法压缩节点规模,精简后的系统模型没有影响到规约性质的验证。(2)研究物联网网关安全系统,设计了物联网网关安全技术框架,系统的逻辑流程采用轮询的方式;对物联网网关系统进行形式化分析及验证,可以嵌入不同的安全协议或算法,提升了网关的安全性能。针对嵌入多种服务的复杂实时系统,使用基于覆盖环的精确加速方法进行状态约减,能够有效减少内存消耗,提升验证效率。