顾兆军，孙浩然

(1.中国民航大学信息安全评测中心，天津300300；
2.中国民航大学中欧航空工程师学院，天津300300)

工业控制系统(Industrial Control System，ICS)是由各种自动化控制组件以及实时数据采集组件和监控控制组件共同构成的信息系统[1]。一般来说，工业控制系统的核心组件包括数据采集与监控系统(Supervisory Control And Data Acquisition，SCADA)、分布式控制系统(Distributed Control System，DCS)、可编程逻辑控制器(Programmable Logic Controller，PLC)、远程终端(Remote Terminal Unit，RTU)、智能电子设备(Intelligent Electronic Device，IED)和确保各组件通信的接口等技术系统[2]。

SCADA系统是一个典型的工业控制系统[3]。SCADA系统优点在于逻辑范围广，系统应用软件多，但系统内硬件结构复杂，系统所处环境多样，一旦遭到攻击，将会对现实物理世界造成巨大危害。2007年，加拿大的水利SCADA控制系统遭到黑客入侵，攻击者利用恶意软件破坏供水控制计算机，致使水利系统一度陷入瘫痪。2010年，震网病毒(Stuxnet)[4]攻击伊朗浓缩铀工厂，超过1000台离心机遭到攻击而瘫痪，伊朗核工业发展遭受重创。2011年，黑客入侵美国伊利诺伊水厂SCADA系统，导致水泵被破坏，污水泄漏。2017年，Wannacry[5]勒索病毒爆发，数以万计加油站因遭受攻击而无法为用户提供正常服务。

SCADA系统是工业控制系统的核心，是国家关键基础设施的重要组成部分，加强对SCADA系统的安全防护，是我国信息安全保障建设的重大课题[6]。从“两化融合[7]”到“中国制造2025计划[8]”的推广，我国对于工控网络安全保护策略的制定和相关技术的研发处于起步阶段。随着两化融合，工业控制网络安全形势也变得越来越严峻[9]，工控网络安全逐渐成为产业界和学术界共同关注的焦点，对于工控网络安全评估研究成为热门研究领域。

Ralston[10]等人给出了SCADA和DCS系统风险评估概要，提出基于妥协表的分析方法。Byres[11]等人对SCADA系统通信协议进行安全评估，指出SCADA系统中Profibus协议脆弱性。白佳林[12]等人总结了人为干预、通信、内部元器件等因素是导致电力系统安全性降低的原因。Nie L[13]等人提出使用贝叶斯加权攻击路径建模技术模拟攻击过程。

工业安全领域中常用形式化分析方法对系统安全性进行评估，形式化分析方法包括攻击树[14]、攻击图[15]、时间自动机[16]等。其中时间自动机是自动机的理论扩展模型，其优点在于有一些有效软件工具帮助构建时间自动机模型并完成模型验证，因此利用时间自动机对工业控制系统安全性验证在近些年得到了广泛应用。

本文提出一种基于时间自动机的形式化验证方法，对SCADA系统安全属性变化进行分析与验证。首先以机场供油自控系统为例，将系统分为监视层、控制层、现场设备层，对每个层级进行时间自动机建模，三个层级的时间自动机一同构成了时间自动机网络。其次根据常见的网络攻击方式，建立针对工控系统的攻击模型，分析工控网络攻击对机场供油自控系统造成的影响。针对工控网络攻击提出防御手段，构建防御模型并分析验证在引入防护措施后航油自控系统安全属性。最后利用UPPAAL工具验证该工控系统在正常环境下、遭受攻击条件下以及引入防御措施条件下的安全属性变化。

2.1 时间自动机

时间自动机是由ALUR和ADIL提出的一种基于自动机理论的自然扩展，用于构建实时系统模型[17]。

设X是一个时钟变量集，x表示X当中的一个时钟值，c表示有理数集Q中的常量，φ1，φ2表示时钟约束。时钟约束集合Φ(x)的约束公式如下：

δ∶=x≤c|c≤x|x

(1)

时钟变量集X上的一个时钟解释v表示为从X到R+的一个映射，如果对于v所提供的任意的时钟赋值，时钟约束δ布尔值为真，则称v是X上的一个时钟约束。

时间自动机是一个六元组：A=，其中C是时钟变量集合，L是有穷状态集合，L0是起始位置，A是有穷动作时间集合，I是使每个l∈L都有一个时钟的约束条件，即对L中的每一个状态节点，都有一个Φ(A)中的时钟约束L→Φ(A)与之映射；
E是边界的规则转换集合。式(2)是时间自动机的Φ(A)是时钟约束集合，其中c是有理数集合Q当中的任意元素，对A当中任意的元素a都有

Φ(A)∶=a≤c|c≤a|a

(2)

2.2 UPPAAL工具介绍

UPPAAL[18]是基于时间自动机理论的模型形式化验证工具，主要包括编辑器、模拟器和验证器。首先利用指令和共享变量将基于时间自动机建立的设备模型连接在一个网络中。其次，通过穷举法验证系统模型的逻辑性和安全性。同时UPPAAL工具利用了CTL语法，具体如表1所示。

表1 CTL属性说明表

3.1 机场供油自控系统介绍

机场供油过程一般由机场油库、输送管网、输送装置和过滤装置构成[19]，如图1所示。

中转油库接收货轮来油和铁路来油，煤油进入中转油库后在储油罐内沉降，经化验合格后通过送油泵和长运输管道输送至使用油库。使用油库继续对煤油进行沉降，直到油库内煤油检验合格后，煤油才可以通过送油泵输送到停机坪供油系统向飞机加油。由于飞机用油对煤油清洁度要求较高，利用过滤装置对煤油进行过滤除杂质，保证煤油含杂质量降低到要求水平之下。

图1 机场供油流程图

机场供油自控系统网络拓扑简如图2所示，自控系统由监控管理层、直接控制层和现场设备层组成。监控管理层能够监视生产过程，通过访问服务器获取生产数据，可以迅速地掌握现场设备的工作状态以及储油库内煤油的情况。直接控制层完成信号的分配、控制运算和执行控制命令等。现场设备层包括了储油罐内智能温度传感器、流量传感器、温度传感器、压力传感器和泵。通过传感器完成信息量的采集，通过阀门开启或关闭泵。

机场供油自控系统采用了冗余网络结构，其中以太网网络带宽为100M，利用Modbus协议进行网络通信，航油自控系统数据传输过程如下：

图2 供油系统网络拓扑简图

1)储油罐内智能传感器将测得航油参数上传至Modbus服务器中。

2)工程师站从Modbus服务器获取储油罐内航油参数。

3.2 安全属性

为保证机场供油自控系统能够完成正常的生产流程，从完整性、可用性两个方面对系统安全属性进行描述，结合正常的工艺流程，控制系统应满足以下安全条件：

1)机场供油自控系统应严格按照正常生产流程进行操作；

2)进油泵和送油泵开启前，传感器应处于工作状态；

3)储油罐内智能传感器损坏，自控系统关闭油泵；

4)储油罐内航油参数超过危险值时，自控系统关闭油泵；

根据归纳总结，系统安全属性如表2所示。

表2 系统安全属性

3.3 攻击方式

网络攻击分为主动攻击与被动攻击，主动攻击通常带有恶意的攻击目的，破坏系统正常运行，造成巨大安全隐患[20]，主动攻击通常可以分为以下四类：拒绝服务、消息篡改、伪装、重放。

拒绝服务攻击影响系统或通讯设备正常工作，让目标计算机或网络无法提供正常的服务或资源访问，使目标系统服务系统停止响应甚至崩溃。消息篡改指对传输数据修改或者改变数据传输顺序来进行攻击。伪装是一个实体冒充另一个实体，通常伪装攻击不会单独出现，一般伴有其它类型的攻击，例如伪装成服务器截取传输数据，冒充合法服务器进行攻击[21]。重放是攻击人通过重新发送已经被认证过的消息来欺骗系统，从而完成身份认证。主动攻击的攻击方式以及攻击结果如表3所示

表3 主动攻击攻击方式及结果

4.1 时间自动机模型

为了描述机场供油自控系统的工作流程，建立了多个时间自动机模型，每个时间自动机模型功能不同，各个时间自动机共同模拟供油自控系统。时间自动机由内部状态节点和信号指令组成，自动机内部节点通过函数以及信号指令会自发的发生状态之间的转移。

4.2 机场供油自控系统建模

机场供油自控系统共分为三个层次，分别是监控层，直接控制层，现场设备层，利用时间自动机理论分别对上述三个层次进行建模。

1)监控层模型

监控层模型当中包含了工程师站模型与Modbus服务器模型，工程师站对生产过程监控，Modbus服务器通过以太网将其它设备连接到计算机以及保存传感器测得的数据。

①工程师站时间自动机

工程师站可以创建、发送和接收响应，与Modbus服务器建立通信，工程师站时间自动机模型见图3。

从Start开始，设置时钟变量t=0，发送modbus＿c2s请求与Modbus服务器建立单向连状态，如果等待时间超过20s，则判定为连接超时，进入Restart状态准备重新开始。如果在20s内收到服务器发送的modbus＿s2c请求时，进入Connected状态，说明此时已与Modbus服务器建立双向通信，工程师站向服务器发送控制指令msg。

图3 工程师站时间自动机

当工程师站接收数据时，首先向服务器发送data＿c2s请求进入Wait＿data状态等待数据包，如果在30s内收到data＿s2c请求，完成一次建立通信的过程，工程师站通过Download指令从服务器下载数据；
如果超过30s仍没收到data＿s2c请求，则回到Restart状态准备重新开始。

②Modbus服务器时间自动机

Modbus服务器与接收到直接控制层传输来的数据信息，并由工程师站完成数据的下载，其时间自动机模型如图4所示。

服务器接收工程师站发送的modbus＿c2s请求并向工程师站发送mobus＿s2c请求，完成一次与工程师站建立双向通信，并接收控制指令msg。服务器接收控制器发送signal＿control请求并向其发送signal＿controlback请求，完成一次与直接控制层的双向通信，利用update指令将数据从控制器上传至服务器当中。通过data＿s2c请求、data＿c2s请求和download指令完成工程师站从服务期内获取数据的过程。

2)直接控制层模型

图4 Modbus服务器时间自动机

直接控制层作为机场供油自控系统的大脑，对生产过程完成自动控制。其行为过程见图5。当控制器收到智能传感器传来的数据之后，有以下几种自动控制行为。

如果储油内传感器所测得的参数正常，则不改变泵的工作状态，通过向服务器发送signal＿control请求、接收signal＿control＿back请求，完成控制器与Modbus服务器的双向通信，之后将传感器测量到的煤油数据上传到服务器当中。

如果储油罐内传感器所测的参数超过危险值，控制器向进油泵或送油泵发送signal＿stop＿pump＿in指令或者signal＿stop＿pump＿out指令，关闭油泵并通知工程师站。

如果没有收到传感器传送的测量数据，表明传感器损坏，控制器向进油泵和送油泵发送signal＿stop＿pump＿in指令以及signal＿stop＿pump＿out指令，关闭油泵并通过通知工程师站。

3)现场设备层模型

图5 控制器时间自动机

现场设备层由储油罐内的智能传感器以及现场控制设备组成。智能传感器是具有信息处理功能的传感器，相对于仅提电压信号的传统传感器，智能传感器充分利用当代集成技术、微处理器技术，将感知、信息处理融为一体，能提供具有一定知识级别的信息[21]。

智能传感器包括了智能温度传感器、智能压力传感器、智能流量传感器、智能液位传感器器。智能传感器系统时间自动机模型如图6所示，传感器工作原理如图5所示。

传感器每10s钟对油库内煤油进行一次测量并进入Wait状态，如果在10s内传感器没有测量到值，说明此时传感器损坏，智能传感器系统发送fault指令，控制器关闭油泵；

图6 智能传感器模型

如果智能传感器系统在十秒内所测得数据超过危险值，智能传感器系统向控制器发送back指令，控制器关闭油泵；

如果传感器在10s内测的数据符合规定值，智能传感器系统向控制器发送show＿level指令告知系统处于正常工作情况，并将测得的数据传输至控制器中。

现场控制设备由进油泵和送油泵组成，进油泵收到signal＿start＿pump＿in指令，进油泵阀门由Close状态转换到Open状态，送油泵开启；
当接收到signal＿stop＿pump＿in指令，进油泵阀门由Open状态转换到Close状态，进油泵关闭。进油泵和送油泵的时间自动机模型见图7。

图7 控制设备模型

4.3 攻击建模

1) Synflood攻击建模

Synflood攻击属于拒绝服务(Denial of Service，Dos)的一种，攻击者利用Modbus/TCP传输协议当中TCP“三次握手”机制漏洞，对服务器进行攻击。Synflood攻击模型如图8所示。

2) 篡改攻击建模

图8 Synflood攻击模型

篡改攻击模型见图9，当攻击者与控制器建立双向通信之后，攻击者通过向控制器发送控制指令，对原有的控制指令的进行篡改，影响控制器正常的控制行为。

3) 重放攻击建模

图9 篡改攻击模型

重放攻击是指攻击者收集有效数据包并重新发送或延迟发送，从而欺骗系统，并通过网络监听来破坏身份认证过程，重放攻击模型见图10。

图10 重放攻击模型

4.4 防御措施建模

1)防Synflood模块

防Synflood攻击措施见图11，通过设立CloudFlare模块代替服务器完成“三次握手”，保证服务器内没有“半连接”消耗服务器网络资源，从而避免服务器遭受到synflood攻击。

2)防篡改模块

图11 防Synflood模型

防篡改模块见图12，通过过设置白名单机制，完成对篡改攻击的防御。如果IP不是白名单内的IP，说明遭受到篡改攻击，当对消息进行舍弃；
当IP地址是白名单内的IP地址，说明消息来自工程师站，对该信息保留。防篡改模型时间自动机见图12。

4) 防重放模块

图12 防篡改模型

针对重放攻击，利用加随机数的方法防重。服务器和控制器都定义一个初始序列号i，传输数据结束后，如果服务器接收到的i没有变化，抛弃该请求；
如果服务器接收到的i满足i=i+1，说明此时没有遭到重放攻击，重放防御模型时间自动机见图13。

图13 防重放模型

5.1 安全属性验证

实验使用因特尔酷睿i5 5257U处理器CPU 2.70GHz，在Java13.0.1环境下安装UPPAAL4.1.9，根据机场供油自控系统工作原理在UPPAAL建立时间自动机模型并验证。

利用UPPAAL检查器对系统进行安全性验证，其中机场供油自控系统要满足可用性、完整性、保密性。机场供油自控系统安全属性结果如表4所示。

表4 系统验证结果

从表7可以看出，系统在正常工作时，完整性、可用性满足性质，供油自控系统运转正常。但是Modbus协议在网络上以明文方式传输，不存在加密以及身份认证的措施，不能够通过UPPAAL验证器对机场供油自控系统保密性进行验证。

5.2 存在攻击者的模型验证结果

进而在航油自控系统中引入攻击者模型，用Dos-Synflood攻击、篡改攻击、重放攻击对系统进行破坏，并对其安全属性进行验证，验证结果如表5所示。

表5 攻击验证结果

从表8可以看出，攻击导致机场供油自控系统安全属性变化：其中Dos-Synflood攻击导致网络无法提供正常的服务及资源访问，传感器测量数据无法传递，破坏系统完整性，但是没有破坏系统的自控功能，可用性没有遭到破坏；
篡改攻击导致自控系统与现场设备通信受阻，攻击者对设备进行自由控制，例如攻击者篡改指令泵的阀门一直处于开启状态，导致正常指令无法传递，系统不能够按照正常的业务逻辑进行控制，破坏了自控系统的完整性和可用性。重放攻击通过将已发送的数据包进行重新发送，导致数据的泄露，破坏了系统的数据完整性，进而破坏了系统的完整性。

5.3 防御措施下的模型验证结果

在对机场自控系统设置一系列防御措施后，重新对系统的安全属性进行验证，验证结果如表6所示。

表6 防御措施验证结果

在引入以上三种防御措施后，自控系统的安全属性恢复，具体来说：防Dos-Synflood攻击措施恢复了系统的完整性，防篡改措施恢复了系统的完整性和可用性，防重放措施保证了自控系统数据不被泄露，保证了数据的完整性。

通过对比实验可知，常见的网络攻击手段对系统的安全属性均有影响：Dos-Synflood攻击会导致系统内存耗尽，发生死锁现象，对系统的完整性均造成影响。篡改攻击导致工程师站发送给现场设备的命令被篡改，系统进入不可控状态从而导致引发危险事件，破坏了系统的可用性。重放攻击导致了系统数据包泄露，威胁到信息完整性。但是由于机场自控系统采用Modbus协议，该协议本身不具备身份认证与加密功能，系统的保密性不能够被验证。

针对以上三种攻击方式，分别建立了防Dos-Synflood攻击模块、防火墙防篡改攻击模块、防重放攻击模块。验证结果表明在引入防御措施后，系统已满足的完整性、可用性的要求，系统的安全属性恢复。对于保密性而言，防重放措施可以保护数据的可用性，增强系统的完整性。

本文基于时间自动机理论对机场供油自控系统建模，针对常见的网络攻击手段，构建Synflood攻击模型、篡改攻击模型和重放攻击模型并对机场供油自控系统进行攻击，在此基础上建立相应的防御措施，利用UPPAAL软件验证机场供油自控系统在正常生产、遭受攻击和引入防御措施后安全属性的变化，发现Synflood攻击影响系统完整性，篡改攻击影响系统的完整性和可用性，重放攻击影响系统的完整性。在引入防御措施后，机场供油自控系统的安全属性恢复，在构建的防御措施下可以完成正常的工作，可见所构建的防御措施可以加强机场供油自控系统的安全性。但由机场供油自控系统采用Modbus明文传输协议，所以无法验证系统保密性的变化，后续将对更为复杂的工控系统进行安全性分析与研究。

猜你喜欢自动机供油油泵{1，3，5}-{1，4，5}问题与邻居自动机数学物理学报(2021年3期)2021-07-19汽轮机主油泵损毁事故分析及解决办法探索科学(学术版)(2021年5期)2021-06-10关于交直流高压油泵分析及建议水电站机电技术(2019年11期)2019-12-02一种基于模糊细胞自动机的新型疏散模型智富时代(2019年4期)2019-06-01一种基于模糊细胞自动机的新型疏散模型智富时代(2019年4期)2019-06-01广义标准自动机及其商自动机西北大学学报（自然科学版）(2018年2期)2018-04-18糯扎渡水电站推力外循环油泵启动逻辑优化水电站机电技术(2018年2期)2018-03-05油泵壳体的冲压工艺及模具设计广东技术师范大学学报(2016年5期)2016-08-22亚洲船供油市场航运交易公报(2014年10期)2014-04-02中国船供油市场航运交易公报(2014年10期)2014-04-02