[1] Qingzhao Zhang, Xiao Zhu, Mu Zhang, and Z. Morley Mao. 2022. Automated Runtime Mitigation for Misconfiguration Vulnerabilities in Industrial Control Systems. In Proceedings of the 25th International Symposium on Research in Attacks, Intrusions and Defenses (RAID ’22). Association for Computing Machinery, New York, NY, USA, 333–349.
今天给大家介绍22年的一篇发表于RAID上的对工业控制系统中的参数配置的验证保护框架SmtConf
背景介绍
工业控制系统（ICS）包含控制单元PLC与人机界面HMI，其中之前大部分工作都是针对PLC进行例如保护控制逻辑等，而对于可以更改关键参数的HMI的保护却很少。而且修改配置参数，并不会引起原有的PLC保护机制的警报。为了检测这些错误的参数配置，需要将参数配置和PLC 控制逻辑以及物理定律作为一个整体来考虑，从而完整地枚举 ICS 的行为，而不是仅仅关注 PLC 或传感器。
本文设计模型检查方法，通过综合考虑程序逻辑、物理定律和时间依赖性来分析复杂 ICS 环境中配置更改的影响。基于形式化方法，本文构建了各种应用程序，包括配置操作的快速检测和最佳安全参数的推荐。
案例
图1中的单元是SMART， 由罗克韦尔自动化（北美领先的工业自动化供应商）构建的制造业测试平台。包括两个门（即阻止和停止）、一个拾放机械臂、一台计算机数控 (CNC) 机器以及包括一个射频识别 (RFID) 收发器的传感器。
该单元执行以下步骤来处理一个零件：
(1) 装有零件的托盘沿着传送带移动并通过阻挡门；
(2) 然后托盘被挡块阻挡，RFID 收发器更新零件 RFID的状态；
(3) 机械臂从托盘上拾取零件并将其传送至无人占用的 CNC；
(4) CNC加工零件；
(5) 机械臂将CNC加工出来的成品零件送回到托盘上；
(6) 当零件进入RFID收发器的检测范围时再次更新RFID；
(7) 最后，停止释放托盘。
Listing 1 显示了协调单元中设备的PLC 控制逻辑（伪代码），该代码处理 RFID 更新过程，当零件进入 RFID 收发器的检测范围（第 8 行）时触发该过程。为了确保 RFID 更新正常工作，每次零件进入检测范围时，UpdateStep_RFID 应重置为零。为了实现此重置行为，计时器 UpdateFinishedDelay 记录自未检测到任何部件以来的累积时间（第15行）。当累计时间达到阈值（即 4 秒）时，UpdateStep_RFID 被重置（第 18 行）。现在有一项安全规范是，当每个部件进入 RFID 收发器的检测范围时，应重置 RFID 更新过程。但这个规范可能会被违反的。由于计时器UpdateFinishedDelay 有 4 秒的超时时间，因此两个事件“Part Leave RFID range”和“RFID_UpdateStep Reset”具有 4 秒的固定间隔。因此，“零件离开 RFID 范围”和“零件进入 RFID 范围”之间的总时间（包括CNC 加工时间）必须长于 4 秒才能满足规范。当电机频率为3,000 rpm时，CNC加工时间约为4秒，始终满足规格。然而，如果提高 CNC 的电机频率，将 CNC 加工时间缩短到 2.5 秒，则有可能零件进入 RFID 检测范围，但 RFID 不会重置。
攻击模型
对于 ICS 安全性，目标是时间安全属性。本文针对的 ICS 具有可在运行时配置的参数，通常通过 HMI。由于安全隐患是基于时间的，因此更关注影响时间属性的配置参数，例如各种计时器、移动设备的速度。重点关注通过预定义的用户界面在运行时不正确地修改某些参数的攻击场景，考虑两种类型的对手：恶意的外部人和良性的内部人。恶意外部者是通过一般网络攻击侵入用户界面以恶意更改系统配置参数的攻击者；良性的内部人员是粗心的操作员，他们以合法的方式不正确地更改配置参数，如上文案例所示。
本文不防御可以物理访问防御系统的恶意内部人员。本文假设来自 SmtConf 的通信具有适当的完整性检查和身份验证。攻击者无法破坏SmtConf的通信，因此SmtConf可以观察到真实的系统状态。本文也不防御传感器欺骗攻击和控制逻辑注入。攻击者可能会发起自适应攻击，即精确操纵参数以在不被发现的情况下破坏系统，SmtConf 通过健全的模型保证了作为验证方法的检测的完整性来抵御自适应攻击。攻击者可能会持续更改配置值以重复触发检测算法，希望造成拒绝服务（DoS），但DoS攻击很容易被管理员发现。
SmtConf
图2展示了SmtConf的架构。
系统建模
是生成 ICS 系统模型的半自动过程。先对PLC 代码进行程序分析，对运行时数据跟踪进行数据挖掘，以提取系统行为。然后构建一个称为符号事件序列图（SESG）的有向图，其路径代表 ICS 的可能执行。然而，数据挖掘并不能保证准确，因此需要要求开发人员根据自动验证过程的反馈修改模型。
1. 系统状态：包括设备间的信号、内存变量、和物体的物理状态
2. PLC 执行模型：使用SCADMAN中的技术，通过合并它们的变量集和代码逻辑来生成一个组合的PLC执行模型。PLC的配置参数包括：推送到远程设备/机器的参数、PLC代码中定时器的超时值、和作为条件的参数
3. 时间事件：首先直接从 PLC 代码中的定时器中提取一组可中断事件。其次解析所有可用的数据跟踪，识别所有触发器和操作的时间戳，并获取每个统计相关的触发器操作对的最大/最小时间间隔。
4. 符号事件序列图 (SESG)：SESG 是系统状态集 S 上的有向图G = (V , E, α, β, γ )，时间间隔 T ，以及 T 上的一组约束 C 。 V 是 SESG 的顶点，α : V → S 是将顶点映射到系统状态的标记函数。 E ⊆ V ×V 是 SESG 的边。标签函数 β : E → T 将每条边与一个非负符号时间相关联间隔，而标记函数 γ : E → C 将每条边与一个防护相关联，这是对符号变量（即时间间隔和配置参数）的约束。一条路径 π = (v0, v1, …) 其中 v0, v1,·····∈ V 是由边连接的系统状态序列。该路径表示 ICS 的一次执行，它从一个初始状态 v0 开始，并沿着路径上的边缘移动系统状态。此外，只有当满足路径约束时，执行才是可行的。
构建SESG的算法如Algorithm 1 中所示。最初，有一组初始顶点指示初始系统状态。然后算法循环执行，在每次迭代中尝试将新顶点连接到图。首先，每个顶点记录其触发事件（图3中的绿色框）以及自触发以来的累积时间（即触发时间）。其次，每个顶点都有一个不变量。当相应的不变量可满足时，系统状态可达。在每次循环迭代中，算法都会选择一个可能具有子顶点的顶点 (vc )，并执行以下步骤：（1）检查顶点是否触发新事件（第5-12行）（2）生成可以作为 vc 之后的下一个系统状态的新顶点（第 15-26 行）（3）考虑时间约束检查状态转换的有效性（第 27-36 行）。最后，使用真实世界的数据跟踪来验证 SESG。
离线安全限制
SmtConf 的规范采用定时命题时序逻辑 (TPTL) 语法。根据规范的语义，它为每条路径生成一个违反约束（SMT表达式），该约束的任何解决方案都是违反规范的具体执行路径。考虑到一条路径是安全的，当且仅当该路径可行时不违反规范，并且当所有路径都是安全时，系统才是安全的，即公式1。生成的规则如表2所示。
违规限制：
路径限制：
在线检测
给定配置参数及其具体值，SmtConf 会检查配置是否违反任何安全规范。 SmtConf 构建一个配置约束（用 C_W 表示），将每个符号配置参数限制为等于具体值。当在特定配置下永远不会违反安全约束时（即公式 2 不可满足），ICS 被验证为无违规。
在线推荐
给定配置参数的搜索范围（用 C_W 表示）和优化目标（配置参数的函数，用 f (W ) 表示），SmtConf 为在该范围内无违规的配置生成具体值，并针对该范围进行优化目标函数。
验证
本文从三个方面评估 SmtConf：（1）检测和推荐的正确性，（2）效率 – SmtConf 流程的时间成本，以及（3）自动化 – 所需的手动工作量。并从SMART 和 Fischertechnik (§7.2) 构建了 18 个测试用例，分别评估 SmtConf 的组件。在表 3 中列出的三个 ICS 上测试SmtConf。 (1) 在一个 SMART 单元中进行零件处理。 (2) 零件通过 SMART 中具有两个出口的一个转向器。分流器的任务是根据零件的 RFID 状态将其运送到正确的目的地。 (3) 在 Fischertechnik 中进行零件加工。
（1）正确性：SmtConf 在 18 个病例中显示出 100% 的真阳性率和 0% 的假阳性率（表4）。
（2）效率：由于安全约束是离线生成的，在线检测是一个轻量级的约束满足求解过程，在18种情况中最多花费0.45秒。由于同样的原因，时间成本主要取决于安全约束的复杂性，因此对于相同ICS下的测试用例来说，时间成本几乎相同。
（3）与VetPLC比较：时间远低于VetPLC，如图5所示。
（4）自动化：对于三个测试的 ICS，数据挖掘正确地提取了 67 个事件中的 49 个 (80%)。开发人员添加了 13 个有关物理动力学的事件（例如，机器人手臂移动部件），开发人员平均为每个 ICS 花费两个工时来补充挖掘的事件。对于检测和推荐，规范是使用 TPTL 语法手动编写的。
总结
SmtConf，这是一个针对 ICS 错误配置漏洞的自动运行时缓解框架，用于检测违反安全规范的行为并自动生成优化的安全参数。 SmtConf 通过考虑运行时可能被不当修改的动态参数，改进了 ICS 上基于模型的验证技术。通过分析动态配置参数的影响，SmtConf是可以指导开发人员安全配置复杂ICS的有效工具。
原文始发于微信公众号（COMPASS Lab）：SmtConf：对工业控制系统中的参数配置的验证保护框架
