LFVeri: Network Configuration Verification for Virtual Private Cloud Networks

The Virtual Private Cloud (VPC) service enables users to configure shared resources within public clouds on demand, providing isolation between users. However, configuring the VPC network is a complex and error-prone task, and misconfiguration has been the leading cause of cloud network security issues. The large number of complex network components and configurations makes it difficult to perform scalable, efficient, and accurate fault verification of the network behavior. To address this issue, we design a comprehensive and automated fault diagnosis and localization tool, called <monospace xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">LFVeri</monospace>, which is built upon an innovative modular network model that accurately captures the logic functions of real components within VPC networks, and propose eleven functions to verify network reachability and security requirements. We conduct performance testing of <monospace xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">LFVeri</monospace> on various datasets and compared it with other verification tools. The experiments show that <monospace xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">LFVeri</monospace> outperforms in modeling and analyzing real VPC scenarios while also possessing the fastest verification speed. It can model and analyze large VPC networks with tens of thousands of components and millions of configuration rules in less than half an hour.