Cilium and VDM -- Towards Formal Analysis of Cilium Policies

TL;DR

This paper explores formal analysis of Cilium network policies in Kubernetes-based industrial control systems using VDM-SL, aiming to improve security and correctness in distributed, component-based architectures.

Contribution

It introduces a formalisation approach for Cilium policies with VDM-SL and demonstrates analysis scenarios to validate policy correctness in industrial systems.

Findings

Formalisation of Cilium policies using VDM-SL

Validation of policies against real-life system models

Identification of potential policy issues through analysis

Abstract

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.