Kano: Efficient Cloud Native Network Policy Verification

Cloud-native computing has become a prevailing paradigm with lightweight runtime-level isolation and fast delivery for scalable applications. Cloud-native network policies (CNNPs) are used to realize network isolation with respect to security and availability. Due to the dynamic environment, CNNPs are label-based instead of IP-based and take the form of attribute-based access control (ABAC) to obtain good expressivity. To ensure the correctness of network isolation, CNNP verification is an essential but challenging problem given the large scale and frequent updates of cloud-native environments and the operation automation demand. Thus, we design Kano, an efficient, i.e., easy-to-use and fast-to-execute, system for verifying large scale CNNPs at runtime. Kano is operation-friendly, with a proposed intent-based verification language. A bit matrix model with a prefiltration algorithm and a partial-update method is proposed to support fast complete and incremental verification. Kano also generates fix plans for violations to assist operators. Kano is implemented as a CNNP verification system that is used in ABAC cloud-native platforms and is integrated into the popular Kubernetes orchestrator. An evaluation on a large scale network of 100k nodes and about 68k policies shows the efficiency of Kano, with 12.51 seconds for all reachable invariant verification and 0.299 milliseconds for policy addition verification.