Formal Verification for Preventing Misconfigured Access Policies in Kubernetes Clusters
Kubernetes clusters now underpin the bulk of modern production workloads, recent 2024 Cloud Native Computing Foundation surveys report >96% enterprise adoption, stretching from 5G edge nodes and AI/ML pipelines to heavily-regulated fintech and healthcare back-ends. Every action in those e...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2025-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/11122676/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | Kubernetes clusters now underpin the bulk of modern production workloads, recent 2024 Cloud Native Computing Foundation surveys report >96% enterprise adoption, stretching from 5G edge nodes and AI/ML pipelines to heavily-regulated fintech and healthcare back-ends. Every action in those environments funnels through the API server, so a single access-control slip can jeopardise an entire fleet. Yet most deployments still rely on a patchwork of Role-Based Access Control (RBAC) rules and policy-as-code admission controllers such as OPA Gatekeeper or Kyverno. In practice these controls are brittle: minor syntactic oversights, wildcard privileges, or conflicting rules can silently create privilege-escalation paths that elude linters and manual review. This paper presents a framework that models both RBAC and admission policies as first-order logic and uses an SMT solver to exhaustively search for counter-examples to stated security invariants before policies reach the cluster. The approach detects policy conflicts, unreachable denies, and unintended permissions. Three real-world case studies are presented to illustrate how the framework reveals latent misconfigurations and validates the soundness of the corrected rules. These case studies include a supply-chain image bypass, an RBAC “shadow-admi” escalation, and a multi-tenant namespace breach. To aid replication and further study, we release a fully scripted GitHub testbed: a Minikube cluster, AuthzForce PDP, admission-webhook adapter, and Z3-backed CLI that recreates each scenario and verifies policies end-to-end. While the framework does not address runtime threats, it closes a critical verification gap and substantially raises the bar for attackers targeting the most widely deployed orchestration platform. |
|---|---|
| ISSN: | 2169-3536 |