Kivi: Verification for Cluster Management in Kubernetes

Explore a groundbreaking presentation on Kivi, the first system for verifying controllers and configurations in cluster management systems, with a focus on Kubernetes. Learn how Kivi models controllers and events into processes, exhaustively checking their interleavings through model checking. Discover the innovative modeling optimizations and design strategies employed to identify violations in reduced topologies, enabling effective handling of autoscaling and large-scale deployments. Gain insights into Kivi's effectiveness and accuracy in uncovering issues within complex, realistic scenarios, including two newly discovered problems in Kubernetes controller source code. Delve into the challenges of modern cloud infrastructure powered by cluster management systems like Kubernetes and Docker Swarm, and understand how Kivi addresses the complexities that can lead to performance degradation and outages.

USENIX ATC '24 - Kivi: Verification for Cluster Management