Kivi: Verification for Cluster Management
summary
Kivi verifies Kubernetes controllers and configurations by modeling controllers, objects, and events and exhaustively exploring interleavings with model checking with SPIN. The system implements high-level controller models, modeling optimizations (atomic control loops, reduced mutable state) and an incremental scaling algorithm that proves violations appear at small sizes; across real incidents the maximum minimal reproducing topology is three nodes and six pods. Kivi runs most analyses under 100s, reproduces logs closely, and finds two new bugs in Kubernetes controllers.
AI-written summary · about
chapters (18)
- 0:00Cluster management verification
- 1:06Controller interaction failures
- 2:10Kubernetes basics
- 3:13Controller conflict example
- 5:41Single controller complexity
- 6:23Kivi safety properties
- 7:27Introducing Kivi
- 8:10Limitations of existing approaches
- 8:30Kivi workflow
- 9:55Dynamic controllers modeling
- 12:40Kubernetes verification scalability
- 13:23Model optimization
- 15:51Incremental scaling hypothesis
- 16:54Hypothesis validation
- 19:26Kivi performance evaluation
- 21:12Kivi vs Kubernetes logs
- 21:54New issues found
- 22:36Limitations and conclusion
related talks
17mAnvil: Verifying Liveness of Cluster Management Controllers
29mKubernetes as a Universal Control Plane
38mThe Verification of a Distributed System
37mKubernetesception: How to run a 1000 control planes
16mUnconference Session: Reliable K8s Operator: How to Survive Eventual Consistency
33mManaging a Kafka cluster in KRaft mode with Strimzi
31mBeyond the Limits: Scaling Kubernetes Controllers Horizontally
15mKoord: A Language for Programming and Verifying Distributed Robotics Application