Network protocols are based on open standards. However, the Internet runs mostly on proprietary and closed-source network devices such as routers and switches of big-name vendors like Cisco. A slight deviation in a vendor's implementation of a standard protocol may weaken the robustness and security of the protocol, thus creating a logical vulnerability an attacker may be able to exploit. Such logical vulnerabilities will likely affect many models of devices made by that vendor. However, finding these logical vulnerabilities in protocol implementations of routers demands great efforts to reverse-engineer them.
In this work, we present a method that leverages a formal black-box method to unearth deviations of protocol implementations in closed-source network devices with no need to access the binary or source code of the device. Our method finds such deviations in a fully automatic manner while leveraging a model-based testing approach. We applied the method to several routers to check their routing protocols' implementations (specifically OSPF) using the tool we found logical vulnerabilities in routers by Cisco and Quagga. The vulnerabilities affect in total dozens of models of routers. This is a joint work with Adi Sosnovich and Orna Grumberg.