Formal Black-Box Analysis of Routing Protocol Implementations
Adi Sosnovich, Orna Grumberg, Gabi Nakibly

TL;DR
This paper introduces a formal black-box testing method tailored for analyzing closed-source routing protocol implementations, successfully identifying deviations that could compromise network security.
Contribution
It presents novel optimizations for model-based testing, enabling efficient and automatic detection of deviations in complex routing protocol implementations.
Findings
Discovered significant deviations in Cisco's OSPF implementation
Identified deviations in Quagga Routing Suite's OSPF implementation
Some deviations confirmed by major vendors like Cisco, IBM, Lenovo, Huawei
Abstract
The Internet infrastructure relies entirely on open standards for its routing protocols. However, the majority of routers on the Internet are closed-source. Hence, there is no straightforward way to analyze them. Specifically, one cannot easily identify deviations of a router's routing functionality from the routing protocol's standard. Such deviations (either deliberate or inadvertent) are particularly important to identify since they may degrade the security or resiliency of the network. A model-based testing procedure is a technique that allows to systematically generate tests based on a model of the system to be tested; thereby finding deviations in the system compared to the model. However, applying such an approach to a complex multi-party routing protocol requires a prohibitively high number of tests to cover the desired functionality. We propose efficient and practical…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Software Reliability and Analysis Research · Software System Performance and Reliability
