2023/11/06 by Bingzhe Liu, Gangmuk Lim, Liu, Bingzhe +5 · 1 citation
Computer Science · #Cloud Computing and Resource Management #Cloud Data Security Solutions #Distributed #FOS: Computer and information sciences #Parallel #Software System Performance and Reliability #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.2311.02800
openalex publication_date 2023/11/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Modern cloud infrastructure is powered by cluster management systems such as Kubernetes and Docker Swarm. While these systems seek to minimize users' operational burden, the complex, dynamic, and non-deterministic nature of these systems makes them hard to reason about, potentially leading to failures ranging from performance degradation to outages. We present Kivi, the first system for verifying controllers and their configurations in cluster management systems. Kivi focuses on the popular system Kubernetes, and models its controllers and events into processes whereby their interleavings are exhaustively checked via model checking. Central to handling autoscaling and large-scale deployments is our design that seeks to find violations in a smaller and reduced topology. We also develop several model optimizations in Kivi to scale to large clusters. We show that Kivi is effective and accurate in finding issues in realistic and complex scenarios and showcase two new issues in Kubernetes controller source code.