Industrial control systems are becoming more distributed and interconnected to allow for interaction with modern computing infrastructures. Furthermore, the amount of data generated by these systems is increasing due to integration of more sensors and the need to increase the reliability of the system based on predictive data models. One challenge in accommodating this data and interconnectivity increase is the change of the architecture of these systems from monolithic to component based, distributed systems. Questions such as how to deploy and operate such distributed system with many sub-components arise. One approach is the use of kubernetes to orchestrate the different components as containers. The critical nature of the industrial control systems however often requires strict component isolation and network segmentation to satisfy security requirements. Cilium is a popular network overlay for kubernetes that enables definition of network policies between different components running as kubernetes pods. The network policies are crucial for maintaining the secure operation of the system, however analysis of deployed policies is often lacking. In this paper, we explore the use of a formal analysis of Cilium network policies using VDM-SL. We provide examples of Cilium policies, an approach how they could be formalised using VDM-SL and analyse several scenarios to validate the policies against a model of simple real-life system.

翻译：工业控制系统正日益分布化和互联化，以实现与现代计算基础设施的交互。此外，由于集成更多传感器以及基于预测数据模型提升系统可靠性的需求，这些系统生成的数据量持续增长。应对数据量与互联性增长的一个挑战在于系统架构从单体式向基于组件的分布式系统转变。随之产生的问题包括如何部署和运行这种包含众多子组件的分布式系统。一种解决方案是使用Kubernetes将不同组件作为容器进行编排。然而，工业控制系统的关键特性通常要求严格的组件隔离与网络分段以满足安全需求。Cilium是一种流行的Kubernetes网络覆盖层，支持为运行在Kubernetes Pod中的不同组件定义网络策略。网络策略对维护系统安全运行至关重要，但已部署策略的分析往往不足。本文探讨利用VDM-SL对Cilium网络策略进行形式化分析的方法。我们提供了Cilium策略实例、基于VDM-SL的形式化建模方法，并通过多个场景分析验证了策略在简化现实系统模型中的有效性。