Cilium 与 VDM -- 关于 Cilium 策略的形式化分析
分布式、并行与集群计算
2024-10-17 v1 软件工程
摘要
工业控制系统正变得更加分布式和互联，以便与现代计算基础设施进行交互。此外，由于集成更多传感器以及基于预测数据模型提高系统可靠性的需求，这些系统生成的数据量正在增加。为适应这种数据和互联性的增加，一个挑战是这些系统从单体架构向基于组件的分布式系统架构的转变。诸如如何部署和运行包含众多子组件的分布式系统等问题随之而来。一个方法是使用 Kubernetes 来编排作为容器运行的不同组件。然而，工业控制系统的关键性质通常需要严格的组件隔离和网络分段，以满足安全要求。Cilium 是 Kubernetes 生态系统中流行的网络覆盖层，使能够定义在运行于 Kubernetes pod 之间的不同组件的网络策略。网络策略对于维护系统的安全运行至关重要，但对已部署策略的分析往往缺乏。本文探索了使用 VDM-SL 对 Cilium 网络策略进行形式化分析的可能性。我们提供了 Cilium 策略的示例，阐述了它们如何使用 VDM-SL 进行形式化，以及分析了几个情景以验证这些策略是否符合简单真实系统的模型。
关键词
引用
@article{arxiv.2410.12009,
title = {Cilium and VDM -- Towards Formal Analysis of Cilium Policies},
author = {Tomas Kulik and Jalil Boudjadar},
journal= {arXiv preprint arXiv:2410.12009},
year = {2024}
}