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!
|
| _version_ | 1849340363538432000 |
|---|---|
| author | Aditya Sissodiya Eric Chiquito Ulf Bodin Johan Kristiansson |
| author_facet | Aditya Sissodiya Eric Chiquito Ulf Bodin Johan Kristiansson |
| author_sort | Aditya Sissodiya |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-5f3afb67d674472ea367a4d8e7eff6f8 |
| institution | Kabale University |
| issn | 2169-3536 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj-art-5f3afb67d674472ea367a4d8e7eff6f82025-08-20T03:43:55ZengIEEEIEEE Access2169-35362025-01-011314179814181310.1109/ACCESS.2025.359750411122676Formal Verification for Preventing Misconfigured Access Policies in Kubernetes ClustersAditya Sissodiya0https://orcid.org/0009-0009-9695-2308Eric Chiquito1https://orcid.org/0000-0003-0215-9798Ulf Bodin2https://orcid.org/0000-0001-5408-0008Johan Kristiansson3https://orcid.org/0009-0001-1674-2506Department of Computer Science, Electrical, and Space Engineering, Luleå University of Technology, Luleå, SwedenDepartment of Computer Science, Electrical, and Space Engineering, Luleå University of Technology, Luleå, SwedenDepartment of Computer Science, Electrical, and Space Engineering, Luleå University of Technology, Luleå, SwedenDepartment of Computer Science, Electrical, and Space Engineering, Luleå University of Technology, Luleå, SwedenKubernetes 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.https://ieeexplore.ieee.org/document/11122676/Attribute-based access controlcloud-native securityformal verificationkubernetespolicy-as-coderole-based access control |
| spellingShingle | Aditya Sissodiya Eric Chiquito Ulf Bodin Johan Kristiansson Formal Verification for Preventing Misconfigured Access Policies in Kubernetes Clusters IEEE Access Attribute-based access control cloud-native security formal verification kubernetes policy-as-code role-based access control |
| title | Formal Verification for Preventing Misconfigured Access Policies in Kubernetes Clusters |
| title_full | Formal Verification for Preventing Misconfigured Access Policies in Kubernetes Clusters |
| title_fullStr | Formal Verification for Preventing Misconfigured Access Policies in Kubernetes Clusters |
| title_full_unstemmed | Formal Verification for Preventing Misconfigured Access Policies in Kubernetes Clusters |
| title_short | Formal Verification for Preventing Misconfigured Access Policies in Kubernetes Clusters |
| title_sort | formal verification for preventing misconfigured access policies in kubernetes clusters |
| topic | Attribute-based access control cloud-native security formal verification kubernetes policy-as-code role-based access control |
| url | https://ieeexplore.ieee.org/document/11122676/ |
| work_keys_str_mv | AT adityasissodiya formalverificationforpreventingmisconfiguredaccesspoliciesinkubernetesclusters AT ericchiquito formalverificationforpreventingmisconfiguredaccesspoliciesinkubernetesclusters AT ulfbodin formalverificationforpreventingmisconfiguredaccesspoliciesinkubernetesclusters AT johankristiansson formalverificationforpreventingmisconfiguredaccesspoliciesinkubernetesclusters |