一种面向物联网应用规则的漏洞检测方法及系统

摘要

本发明公开了一种面向物联网应用规则的漏洞检测方法及系统，方法包括：从物联网控制平面获取应用源代码、设备描述信息和用户配置信息；从应用源代码中提取出过程间控制流图；结合用户配置信息和设备描述信息，将过程间控制流图转换为规则形式；建立物理空间本体模型，将规则形式集合融合到物理空间本体模型上，建立规则执行模型；对所述规则执行模型切片，得到多个不存在依赖关系的子FSM模型；对子FSM模型进行模型变量空间的压缩，和威胁表达式对比判断是否存在威胁漏洞，本发明方法通过实现物理属性感知的模型检测方法，能够对物联网应用中漏洞实现自动准确的检测，为物联网在不同领域中应用提供安全保障。

说明书

技术领域

本发明属于物联网技术领域，具体涉及一种面向物联网应用规则的漏洞检测方法及系统。

背景技术

随着以智能家电、智能网联汽车、智能可穿戴设备等为代表的数以万亿计的新设备接入网络，物联网(Internet of Things,IoT)形成了海量的信息数据以及丰富的人与物、物与物的交互模式，开启了万物互联的时代。随着物联网应用需求的全面升级，一种基于规则(``触发-动作”)的终端用户编程框架被引入物联网中，使其服务供应进入一个新的应用化时代，物联网服务不再是固定地编码在专用设备中，实现了面向用户可编程的服务供应。基于规则的服务供应使得物联网技术更高效地融合了物理空间和信息空间，但也使物理空间的传统安全威胁和信息空间的非传统安全威胁相互交织，信息空间任何的安全隐患在物理空间极可能被放大成极高风险的安全威胁。通过设计物联网应用规则的漏洞自动检测方法，对强化物联网安全性、提高物联网应用部署效率具有重要意义。

基于规则的物联网应用安全性分析工作目前引起了国内外的广泛关注，研究者从从不同的角度审视基于规则的物联网安全隐患问题，代表性工作包括数据流缺陷、规则交互威胁、隐私泄漏、动态安全策略执行和规则自动化生成等。然而，现有方法大多集中在规则在信息空间中的执行安全性研究上，通过利用静态软件分析或形式化方法实现规则语义层面的逻辑安全性分析。但是，在实际的物联网环境下，应用规则的执行行为与物理空间的特性紧密相连，现有方法在实际应用中存在局限性。另外一方面，由于物联网涉及复杂的网络环境和物联感知数据，现有通过简化规则模型(如将并发的规则执行行为建模为串行的形式化模型)，牺牲检测的全面性来确保漏洞检测的可扩展性。因此，为了解决物联网应用规则的漏洞检测问题，有必要设计一种能够全面分析应用规则在信息空间和物理空间上的执行行为，实现应用规则的严谨漏洞检测方法。

发明内容

为了解决上述的技术问题，本发明提供了一种面向物联网应用规则的漏洞检测方法及系统。从物联网应用中静态提取规则信息，融合物理空间本体特性，形成规则的执行模型，进而利用形式化方法实现规则模型的安全性检测。

一种面向物联网应用规则的漏洞检测方法，包括如下步骤：

从物联网控制平面获取应用源代码、设备描述信息和用户配置信息；

从应用源代码中提取出过程间控制流图；

结合用户配置信息和设备描述信息，将过程间控制流图的入口、路径条件以及终点函数转换为“触发-条件-动作”形式的应用规则，多个应用规则组成应用规则集合；

建立物理空间本体模型，应用规则集合融合到物理空间本体模型上，建立规则执行模型；

对所述规则执行模型切片，得到多个不存在依赖关系的子FSM模型；对子FSM模型进行模型变量空间的压缩，得到状态空间优化后的规则执行模型；

建立威胁表达式，将上述状态空间优化后的规则执行模型与所述威胁表达式进行对比匹配，如果匹配到某一威胁表达式，则认为可能存在漏洞，然后利用该威胁表达式生成安全属性或活属性，与规则执行模型进行模型检测，确认漏洞的有效性。

本发明进一步的实施例中，所述过程间控制流图的具体获取方式如下：

遍历所述应用源代码的抽象语法树，通过执行路径敏感的分析方法，提取出应用源代码中每个函数的控制流图和函数之间的调用图，由控制流图和调用图组合成进程间控制流图。

本发明进一步的实施例中，根据进程间控制流图入口函数类型的不同，将进程间控制流图分为应用初始化、事件调度和事件处理三种类型。

本发明进一步的实施例中，所述应用规则构建为如下“触发-条件-动作”的形式：

式中，t表示由事件或状态变化而构成的触发；a为规则形式需要采取的动作；l为时间语义；c

本发明进一步的实施例中，设备描述信息由设备属性、取值范围以及设备命令三部分组成；用户配置信息是规则约束条件中使用的常量；

按如下方法将过程间控制流图转换为规则形式：

对于过程间控制流图中用于应用初始化的路径，将规则触发t和条件c设为空，将变量赋值语句按照设备描述信息中的命令信息和用户配置信息的常量转换为动作a，形成初始化的规则；

对于过程间控制流图中用于事件调度的路径，建立一个空触发和条件的规则，将其延迟l设为路径上设定的调度延迟，动作则是调度所对应函数中的设备命令或系统状态修改的赋值语句，形成事件调度的规则；

对于过程间控制流图中用于事件处理的路径，提取系统函数subscribe中定义的入口事件，设为触发t，然后提取路径上的分支条件作为条件c，路径末端的命令为动作a，形成事件处理的规则。

本发明进一步的实施例中，规则执行模型的具体构建方式如下：

构建包括物理信道、物理设备连接的物理空间本体模型；

物理信道的模型形式描述为：

其中，

物理连接的模型形式描述为：

式中，

基于物理信道、物理设备连接，将应用规则集合转换有限状态机模型

如果当前状态s能够将规则r

利用构建的物理通道和物理连接信息，建立规则之间的依赖关系，其形式表达为：

其中，规则r

本发明进一步的实施例中，对所述规则执行模型切片的具体方式如下：

1)建立表达式依赖边集合E

2)建立规则依赖边集合E

3)模型切片：该步骤使用E

本发明进一步的实施例中，对子FSM模型进行模型变量空间的压缩具体方式如下：

对子FSM模型中存在的用于描述物理属性的变量进行判定，若变量未涉及任何赋值语句或约束判断，则删除该变量；若该变量为一个枚举型，且只有一部分的元素被模型使用，则删除其枚举列表流未使用的元素；若该变量为一个数值变量，则将涉及到的数值压缩到一个最小的连续数值空间内，并以该数值空间重新申明该变量。

本发明进一步的实施例中，所述威胁表达式共有7种：动作触发交互威胁、动作调度扰乱威胁、动作覆盖威胁、动作中断威胁、条件动态堵塞威胁、调度条件堵塞威胁和设备禁用威胁。

本发明提供的另一个技术方案是：

一种用于所述面向物联网应用规则的漏洞检测方法的系统，包括：

应用和配置信息爬虫模块，用于从物联网控制平面获取应用源代码、设备描述信息和用户配置信息；

控制流图构建模块，用于从应用源代码中提取出过程间控制流图；

规则构建模块，用于结合用户配置信息和设备描述信息，将过程间控制流图的入口、路径条件以及终点函数转换为“触发-条件-动作”形式的应用规则；

模型构建模块，用于建立物理空间本体模型，将从应用源代码中提取出的应用规则集合融合到物理空间本体模型上，建立规则执行模型；

模型压缩模块，用于对所述规则执行模型切片，得到多个不存在依赖关系的子FSM模型；对子FSM模型进行模型变量空间的压缩，得到状态空间优化后的规则执行模型；

漏洞检测模块，用于建立威胁表达式，将规则执行模型与所述威胁表达式进行对比匹配，如果匹配到某一威胁表达式，则认为可能存在漏洞，然后利用该威胁表达式生成安全属性或活属性，与规则执行模型进行模型检测，确认漏洞的有效性。

与现有技术相比，本发明有以下有益效果：

1)本发明通过从物联网控制平面获取应用源代码、设备描述信息和用户配置信息，能够实现自动化的应用规则信息提取，实现规则逻辑信息的准确刻画。

2)本发明建立了物理空间本体模型，实现规则在物理空间上的执行行为的刻画，为物联网环境下的漏洞检测提供完全准确的安全分析空间。

3)本发明设计了基于物理特性的模型切片和变量空间压缩方法，可以实现高效的规则模型压缩优化方法，降低模型检测的复杂度。

4)本发明设计了多种新型的规则执行威胁模式，实现规则安全属性的准确规约。同时，基于安全属性和活属性的模型检测，确保漏洞检测的全面性，能够为物联网用户提供准确全面的安全分析结果。

综上所述，本发明通过实现物理属性感知的模型检测方法，能够对物联网应用中漏洞实现自动准确的检测，从而为物联网在不同领域中应用提供安全技术保障。

附图说明

构成本申请的一部分的说明书附图用来提供对本发明的进一步理解，本发明的示意性实施例及其说明用于解释本发明，并不构成对本发明的不当限定。在附图中：

图1为本发明实施例面向物联网应用规则的漏洞检测方法的原理图。

图2为本发明实施例中模型切片示意图。

图3为本发明实施例中物联网应用规则交互威胁模式示意图。其中，3a动作覆盖，3b动作调度扰乱，3c动作中断，3d动作触发交互，3e设备禁用，3f条件动态堵塞，3g调度条件堵塞。

图4为本发明实施例中漏洞检测结果示意图。

图5为本发明实施例中规则漏洞检测系统性能分析示意图。

具体实施方式

下面将参考附图并结合实施例来详细说明本发明。需要说明的是，在不冲突的情况下，本申请中的实施例及实施例中的特征可以相互组合。

以下详细说明均是示例性的说明，旨在对本发明提供进一步的详细说明。除非另有指明，本发明所采用的所有技术术语与本申请所属领域的一般技术人员的通常理解的含义相同。本发明所使用的术语仅是为了描述具体实施方式，而并非意图限制根据本发明的示例性实施方式。

为了便于本领域普通技术人员理解和实施本发明，下面结合附图及实施例对本发明作进一步的详细描述，应当理解，此处所描述的实施示例仅用于说明和解释本发明，并不用于限定本发明。

如图1所示，本发明实施例提供了一种面向物联网应用规则的漏洞检测方法及系统，方法包括：从物联网控制平面获取应用源代码、设备描述信息和用户配置信息；从应用源代码中提取出过程间控制流图；结合用户配置信息和设备描述信息，将过程间控制流图的入口、路径条件以及终点函数转换为“触发-条件-动作”形式的应用规则，多个应用规则组成应用规则集合；建立物理空间本体模型，应用规则集合融合到物理空间本体模型上，建立规则执行模型；对所述规则执行模型切片，得到多个不存在依赖关系的子FSM模型；对子FSM模型进行模型变量空间的压缩，得到状态空间优化后的规则执行模型；建立威胁表达式，将上述状态空间优化后的规则执行模型与所述威胁表达式进行对比匹配，如果匹配到某一威胁表达式，则认为可能存在漏洞，然后利用该威胁表达式生成安全属性或活属性，与规则执行模型进行模型检测，确认漏洞的有效性。

本发明实施例中，采用来自三星的SmartThings和IFTTT两种不同的物联网平台的应用作为实施对象，确保本发明方法的普适性。本发明实施例的具体实现包括如下步骤：

步骤1：规则信息自动提取与形式构建。

(1)控制流图构建：为了提取物联网应用中的进程间控制流图(inter-proceduralcontrol flow graph,ICFG)，本发明实施例采用基于Groovy代码编译器的抽象语法树遍历器，允许通过编译器钩子插入额外的代码传递。利用该抽象语法树遍历器，在编译器对物联网应用代码进行语义分析阶段中遍历该应用源代码的抽象语法树，通过执行路径敏感的分析方法，提取出应用源代码中每个函数的控制流图和函数之间的调用图，进而组合成进程间控制流图。

其中，本发明根据ICFG入口函数类型的不同，将ICFG分为应用初始化、事件调度和事件处理三种类型：应用初始化ICFG用于初始化信息空间变量和物联网设备状态信息；事件调度ICFG利用系统函数subscribe实现事件处理函数的调度；事件处理ICFG用于描述根据不同的事件或状态变化，应用所执行的代码。

(2)规则形式构建：本实施例中，一条规则是以触发-条件-动作范例的来定义。当触发产生时，并且系统状态满足条件时，系统发出动作执行命令。因此，本发明将应用规则构建为如下“触发-条件-动作”的形式：

其中，t表示为由事件或状态变化而构成的“触发”；c＝c

由于规则的执行行为与赛博空间多种特性相关联，在触发产生时，由于物联网控制平台自身可能存在延迟或者用户设定的规则延迟，规则的动作不一定是被立即执行；或者动作的执行需要在一定时间内才能执行完成，如热水器加热。物联网是一个并发的系统，延迟的不同对刻画准确的规则执行过程有着重要影响。因此，本发明在公式(1)中引入了时间语义l，将c拆分为c

基于上述形式化刻画的规则，本发明将从物联网应用中提取出的ICFG转换为公示(1)所示的规则。具体方式如下：

首先，该系统从物联网控制端获取物联网设备描述信息和用户配置信息。其中每条设备描述信息由设备属性、取值范围、以及设备命令三部分组成。用户配置信息则是规则约束条件中使用的常量，如温度阈值、动作延迟等。基于上述信息，该步骤按如下方法将ICFG转换为公式(1)所示规则：

1)对于ICFG中用于应用初始化的路径，将规则的触发t和条件c设为空，将变量赋值语句按照设备描述信息中的命令信息和用户配置的常量转换为动作a，形成初始化的规则；

2)对于ICFG中用于事件调度的路径，建立一个空触发和条件的规则，将其延迟l设为路径上设定的调度延迟，动作则是调度所对应函数中的设备命令或系统状态修改的赋值语句，形成事件调度的规则；

3)对于ICFG中用于事件处理的路径，提取系统函数subscribe中定义的入口事件，设为触发t，然后提取路径上的分支条件作为该规则条件c，该路径末端的命令为该规则动作a，形成事件处理的规则。如果该路径上存在延迟，引入延迟l。

步骤2：规则执行模型的构建；

物联网系统由上而下分为控制层、设备层和物理环境三部分。分析规则执行在控制层、设备层和物理环境的行为特性，建立规则执行模型与压缩方法。具体方式如下：

首先，建立物理信道和物理设备连接的物理空间本体模型。

物理信道模型是指规则r

其中，由于环境属性

物理连接模型是指设备

上述的两类关联关系描述了由物理环境特性而产生的规则执行依赖关系。

基于上述物理空间本体模型，将应用规则集合转换有限状态机(FSM)模型

如果当前状态s可以将规则r

然后，利用构建的物理通道和物理连接信息，建立规则之间的依赖关系，其形式表达为：

表示规则r

对于一个基于信道的依赖关系d

对于一个基于连接的依赖关系d

步骤3：模型状态空间的优化与压缩；

由于诸多属性变量的非确定性状态，规则执行模型是并行的，可以准确描述规则实际的执行过程。但是并行模型也导致巨大的模型状态空间。因此，进一步引入模型切片和状态压缩方法，建立一种混合的规则模型，如图2所示。具体方式如下：

首先，通过上述在物理空间本体模型上建立的规则执行模型，实现规则执行模型的切片，分为三个步骤完成：

1)建立表达式依赖边集合E

2)建立规则依赖边集合E

3)模型切片：使用E

然后，在切片后的模型上，进行模型变量空间的压缩。由于FSM模型中存在诸多用于描述物理属性的变量，这些变量通常具备巨大的值范围(如时间，光照度等)，这会导致模型中存在巨大且冗余的状态空间。因此，为了压缩这些变量带来的状态空间，通过压缩这些变量的值范围来避免状态空间爆炸问题。具体来说，该步骤通过分析这些变量在模型中涉及到的所有值：若一个变量未涉及任何赋值语句或约束判断，则表明该变量是冗余的，删除该变量；若一个变量为一个枚举型，且只有一部分的元素被模型使用，则删除其枚举列表流未使用的元素；若一个变量为一个数值变量，则将其涉及到的数值压缩到一个最小的连续数值空间内，并以该数值空间重新申明该变量。

步骤4：规则威胁模式建立与多属性驱动的漏洞检测。

通过分析不同规则动作与触发之间、动作与动作之间、动作与条件之间的交互影响，首先建立规则执行的威胁模式。如图3所示，本发明实施例中提出了七种规则威胁模式：动作触发交互威胁、动作调度扰乱威胁、动作覆盖威胁、动作中断威胁、条件动态堵塞威胁、调度条件堵塞威胁、和设备禁用威胁。

如图3所示，将这七种威胁模式和现有威胁模式进行概述，形式地描述为如下所示的7种威胁表达式：

1)T1动作重复：r

2)T2动作冲突：r

3)T3动作-触发交互：r

4)T4动作覆盖：r

5)T5动作中断：r

6)T6条件堵塞：r

7)T7设备禁用：r

基于上述7种威胁表达式，首先将待检测的规则执行模型与威胁表达式进行对比匹配，检测是否存在匹配的情况。如果存在，则将匹配到的威胁表达式，利用线性时序逻辑(LTL)和分支时序逻辑(CTL)描述为一个安全属性或活属性，；然后基于该生成的属性，利用现有模型检测算法对规则执行模型进行形式化验证，确认该威胁表达式在规则执行模型中带来的漏洞的有效性。

例如，当一个应用中断威胁漏洞发现后，生成一个活属性“a

实现效果：

本发明实施例中，对SmartThings和IFTTT的开源的1108个物联网应用进行漏洞检测。图4为本发明检测出的结果：V-I为动作重复和动作冲突威胁的规则漏洞，本发明发现了136个动作重复漏洞和52个动作冲突漏洞；V-II为动作-触发交互的规则漏洞，本发明发现了67个漏洞；V-III为动作覆盖，本发明发现了52个规则漏洞；V-IV为动作中断漏洞，本发明发现了45个漏洞；V-V为条件堵塞漏洞，本发明发现了89个漏洞；V-VI为设备禁用漏洞，本发明发现了共61个漏洞。

此外，本发明还对该漏洞检测系统的性能进行分析。通过分别测试本发明在对模型不进行优化、对模型仅进行切片、对模型仅进行压缩、和对模型同时进行切片和压缩后的四种情况下的漏洞分析时间，其性能分析结果如图5所示。可见，在本发明设计的模型切片和状态空间压缩方法下，本发明的漏洞检测可以将原先需要分钟级别的漏洞检测时间降低到毫秒级别，大大缩减了漏洞检测的时间。

本发明实施例还提供了一种用于所述面向物联网应用规则的漏洞检测方法的系统，包括：

应用和配置信息爬虫模块，用于在用户给定用户名和密码信息后，自动从物联网控制平面获取应用源代码、设备描述信息和用户配置信息；

控制流图构建模块，用于利用代码静态分析方法，从应用源代码中提取出过程间控制流图，用于记录应用初始化、调度、以及事件处理逻辑信息；

规则构建模块，用于结合用户配置信息和设备描述信息，将过程间控制流图的入口、路径条件以及终点函数转换为“触发-条件-动作”形式的应用规则，实现应用规则的准确描述；

模型构建模块，用于建立物理空间本体模型，包括物理空间属性的变化特性、物理信道以及物理设备连接，将从应用源代码中提取出的应用规则集合融合到物理空间本体模型上，建立规则执行模型；应用规则集合包括了多个“触发-条件-动作”形式的应用规则；

模型压缩模块，用于对所述规则执行模型切片，得到多个不存在依赖关系的子FSM模型；对子FSM模型进行模型变量空间的压缩，得到状态空间优化后的规则执行模型，从而提高模型检测的效率；

漏洞检测模块，用于建立威胁表达式，将规则执行模型与所述威胁表达式进行对比匹配，如果匹配到某一威胁表达式，则认为可能存在漏洞，然后利用该威胁表达式生成安全属性或活属性，与规则执行模型进行模型检测，确认漏洞的有效性；当检测出存在逻辑缺陷时，将具体的规则信息和用户配置信息，以有限状态转移图的方式，呈现给用户，用以改进应用规则和配置信息。

由技术常识可知，本发明可以通过其它的不脱离其精神实质或必要特征的实施方案来实现。因此，上述公开的实施方案，就各方面而言，都只是举例说明，并不是仅有的。所有在本发明范围内或在等同于本发明的范围内的改变均被本发明包含。