VeriReach: A Formally Verified Algorithm for Reachability Analysis in Virtual Private Cloud Networks

Virtual Private Cloud (VPC) has become a widely used cloud computing service, serving as a foundational web infrastructure for many organizations. Nevertheless, the growing problem of reachability issues poses significant threats to the security and reliability of VPC networks, potentially resulting in critical security concerns such as data breaches and service outages. Although there has been substantial progress in recent reachability analysis, existing methods lack validation of correctness. Moreover, current analyses are tailored for One-to-One reachability where both the source and the destination are fixed, and fail to efficiently answer One-to-Multi reachability queries, which involve computing all reachable destinations for a given source node. To address the above challenges, we propose VeriReach, the first formally verified algorithm that provides comprehensive and efficient reachability analysis in large-scale VPC networks. The reachability analysis result of VeriReach is proved to be equivalent to the original reachability semantics of the VPC networks, ensuring its correctness (i.e., soundness and completeness). The fine-grained formalization of VeriReach and its fully mechanized correctness proofs are carried out in Isabelle/HOL theorem prover with 282 lemmas/theorems and $\sim 4,900{\mathrm{LoC}}$. We further implement VeriReach in C++ and the evaluations indicate that VeriReach is more efficient and scalable than MonoSAT, the state-of-the-art SMT solver, when applied to large-scale VPC networks for reachability analysis.