Towards a query-driven approach for the verification of Kubernetes configuration

Securing production Kubernetes clusters is a critical and increasingly complex task. The decentralized and fragmented nature of security policies, such as Role-Based Access Control (RBAC) and NetworkPolicy resources, creates a significant semantic gap between high level security requirements and the low level reality of the cluster configuration. Manual verification is cognitively demanding, error prone, and does not scale, while existing automated tools are often siloed within a single domain, leaving blind spots at the intersection of authorization and network reachability. To bridge this gap, this thesis introduces a query-based verification approach that assesses cross-domain security properties, specifically across RBAC and NetworkPolicy, through a unified cluster model. This methodology is built upon three core components. First, a high-level, declarative query language has been established, engineered for modularity and extensibility to enable operators to formulate single-domain and cross-domain security questions. Second, a typed and unified graph model has been designed to normalize disparate Kubernetes configuration objects and policies into a unified and consistent representation of the cluster’s state. Third, SWI-Prolog is employed as the formal engine to evaluate these high-level queries. To achieve this, we materialize the graph model as a SWI-Prolog knowledge base and compile the query language into a fixed set of Prolog rules. Operator questions are then posed as queries against this knowledge base and evaluated by the SWI-Prolog engine. Although this work unifies the critical domains of RBAC and NetworkPolicy, the core architecture was designed for modularity, making it straightforward to incorporate additional Kubernetes policy and configuration domains. This modular design is validated by a Proof-of-Concept (PoC) that effectively answers both single- and cross-domain questions on realistic configurations, establishing a solid foundation for future integration.