On the Security and Complexity of Periodic Systems
On the Security and Complexity of Periodic Systems
复制标题
论周期系统的安全性和复杂性
DOI：
10.1007/s42979-022-01223-9
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Alturki M
中科院分区：
文献类型：
--
作者：
Alturki M
近年来，工业系统对各种互联组件的依赖急剧增加，从简单的传感器到更复杂的网络物理和物联网(IoT)设备，这类系统通常被称为工业4.0(I4.0)。连通性的增强和不安全组件的扩散为网络攻击提供了机会，这种攻击实际上可能造成深远的损害。本文提出了一种对I4.0应用及其安全属性进行形式化建模和分析的方法。我们引入了I4.0应用程序的形式模型，作为自动机系统(AS)，表示为多集重写(MSR)理论。我们还确定了AS的不同子类，反映了I4.0要求的不同类型，如周期性。此外，我们根据入侵者可以使用的操作数量提出了一系列入侵者模型，从而对系统面临的不同级别的威胁进行了建模。这些模型用于研究两类问题的复杂性：功能正确性(安全)和易受攻击(安全)。最后，通过使用重写工具Maude描述这些模型的可执行规范并进行各种实验，我们证明了周期系统是服从于自动验证的。
Recent years have seen a tremendous increase in the reliance of industrial systems on a variety of interconnected components ranging in complexity from simple sensors to more complex cyber-physical and Internet of Things (IoT) devices, a class of systems that is often referred to as Industry 4.0 (I4.0). Increased connectivity and the proliferation of insecure components present an opportunity for cyber attacks that could in practice inflect far-reaching damage. We present in this paper a formal modeling and analysis approach of I4.0 applications and their safety and security properties. We introduce formal models of I4.0 applications as automata systems (AS) expressed as theories in Multiset Rewriting (MSR). We also identify different subclasses of AS, reflecting different types of I4.0 requirements, such as periodicity. Furthermore, we model different levels of threats to the system by proposing a range of intruder models based on the number of actions that intruders can use. These models are used to investigate the complexity of two types of problems: functional correctness (safety) and vulnerability to attacks (security). Finally, we demonstrate that periodic systems are amenable to automated verification by describing an executable specification of these models using the rewriting tool Maude and carrying out various experiments.
登录
查看更多内容
影响因子：
0.5
作者：
M. Kanovich;Tajana Ban Kirigin;Vivek Nigam;A. Scedrov;C. Talcott;Ranko Perovic
通讯作者：
Ranko Perovic
协作系统中的有限内存 Dolev-Yao 对手
影响因子：
1
作者：
M. Kanovich;Tajana Ban Kirigin;Vivek Nigam;A. Scedrov
通讯作者：
A. Scedrov
安全协议的资源和计时方面
影响因子：
1.2
作者：
Aires Urquiza A
通讯作者：
Aires Urquiza A
距离限制协议分析中的时间、计算复杂度和概率
DOI：
--
发表时间：
2017
期刊：
Journal of computing and security
影响因子：
--
作者：
M. Kanovich;Tajana Ban Kirigin;Vivek Nigam;A. Scedrov;C. Talcott
通讯作者：
C. Talcott
OPC UA安全分析
DOI：
--
发表时间：
2017
期刊：
影响因子：
--
作者：
P. Cheremushkin
通讯作者：
P. Cheremushkin