Validating Interior Gateway Routing Protocols via Equivalent Topology Synthesis

Routers, relying on routing protocols to determine how data packets travel across the Internet, serve as the backbone of modern networks. Vulnerable routing protocols can lead to serious consequences, including data leaks and network congestion. This work focuses on validating the implementation of a key class of routing protocols known as Interior Gateway Protocols (IGPs). Unlike communication protocols such as TCP/IP, which define structured data packets and state machines to facilitate communication, IGPs are designed to automatically manage the network topology. Thus, conventional techniques, which primarily focus on communication correctness, cannot be applied directly to IGPs. We propose ToDiff, a differential validation technique to uncover IGP bugs in three steps: (1) it uses a network generation algorithm to create random yet valid IGP networks, (2) it applies a semantics-guided program synthesizer to generate equivalent topological programs, and (3) it simulates the network via the equivalent topological programs, with any discrepancies suggesting the presence of a potential bug. We have evaluated ToDiff on the implementation of two common IGP protocols, OSPF and IS-IS. The results demonstrate that ToDiff outperforms existing approaches. To date, our tool has successfully identified 26 bugs, all confirmed or fixed by developers.