Security Analysis for Distributed IoT-Based Industrial Automation
Security Analysis for Distributed IoT-Based Industrial Automation
复制标题
DOI：
10.1109/tase.2021.3106335
复制
发表时间：
2021-09-02
影响因子：
5.6
通讯作者：
Pajic, Miroslav
中科院分区：
文献类型：
--
作者：
Lesi, Vuk;Jakovljevic, Zivana;Pajic, Miroslav
物联网（IoT）技术使可重构制造系统的开发成为可能——新一代模块化工业设备适合高度定制制造。这些系统中的顺序控制主要基于离散事件，而它们的正式执行语义被指定为控制解释Petri网（CIPN）。尽管业界广泛使用基于CIPN形式的编程语言，但不支持在存在对抗性活动的情况下对此类控制应用程序进行正式验证。因此，在本文中，我们将介绍基于cipn的顺序控制应用程序的安全感知建模和验证技术。具体而言，我们展示了如何将联网工业物联网控制器的CIPN模型转换为基于时间Petri网（TPN）的模型，并与工厂和安全感知通道模型组成，以便在存在基于网络的攻击时实现系统级安全属性验证。此外，我们引入了使用非确定性捕获对抗行为的现实通道特定攻击模型。此外，我们还展示了如何利用验证结果来引入安全补丁并促进攻击检测器的设计，从而提高系统弹性并满足关键安全属性。最后，我们通过一个工业案例研究来评估我们的框架。
Internet of Things (IoT) technologies enable development of reconfigurable manufacturing systems--a new generation of modularized industrial equipment suitable for highly customized manufacturing. Sequential control in these systems is largely based on discrete events, whereas their formal execution semantics is specified as control interpreted Petri nets (CIPN). Despite industry-wide use of programming languages based on the CIPN formalism, formal verification of such control applications in the presence of adversarial activity is not supported. Consequently, in this article, we introduce security-aware modeling and verification techniques for CIPN-based sequential control applications. Specifically, we show how CIPN models of networked industrial IoT controllers can be transformed into time Petri net (TPN)-based models and composed with plant and security-aware channel models in order to enable system-level verification of safety properties in the presence of network-based attacks. Additionally, we introduce realistic channel-specific attack models that capture adversarial behavior using nondeterminism. Moreover, we show how verification results can be utilized to introduce security patches and facilitate design of attack detectors that improve system resiliency and enable satisfaction of critical safety properties. Finally, we evaluate our framework on an industrial case study.