The Taub Faculty of Computer Science Events and Talks

The Internet infrastructure relies almost entirely on network protocols that are based on open standards. However, the majority of network devices on the Internet, e.g. routers and switches, are proprietary and closed source. Hence, there is no straightforward way to analyze them. Specifically, one cannot easily and systematically identify deviations of a network device's protocol implementation from the protocol's standard. Such deviations may degrade the security or resiliency of the network. In this talk I will present our work on a formal analysis of black boxes in the network. We develop a formal black-box method to unearth non-standard protocol deviations in closed-source network devices. The method relies only on the ability to test the targeted protocol implementation and observe its output. We use a model-based testing approach, which relies on a formal model of the protocol in question. We develop optimizations that are tailored to the analysis of network protocols, to allow reducing the number of generated tests without loss of functionality cover of the model. We evaluate our method against the OSPF protocol. We search for deviations in the OSPF implementation of Cisco - the largest networking vendor in the world. Our evaluation identified numerous significant deviations. Some of them can be abused to compromise the security of a network. The deviations were acknowledged by Cisco to exist in the versions we tested. I will briefly describe other topics in my thesis.