|Ph.D Student||Sosnovich Adi|
|Subject||Finding Security Vulnerabilities in Network Protocols|
Using Methods of Formal Verification
|Department||Department of Computer Science||Supervisor||PROFESSOR EMERITUS Orna Grumberg|
|Full Thesis text|
The routers and networks of the Internet are clustered into connected sets. Each such set is called an autonomous system (AS). Routing of data packets on the Internet works in two levels. The Border Gateway Protocol (BGP) is the routing protocol that determines through which ASes the packets will traverse. The Open Shortest Path First (OSPF) protocol is a widely used routing protocol that determines the path taken by the packets within each AS. Finding security vulnerabilities and attack strategies in these routing protocols is an important task and is significant for the Internet security.
Formal verification methods were originally developed to prove correctness of systems based on formal specifications. A very common approach in formal verification is model checking. Model checking is an efficient algorithm, that given a system model and a required specification, determines whether the system satisfies the specification requirements or not. When the answer is no, there is also a counterexample in the form of an undesired behavior of the system. In this thesis, we develop several methods to apply a systematic and automatic security analysis of these Internet routing protocols. We use methods and tools from the field of formal verification.
We first develop a security analysis method for finding built-in vulnerabilities in the OSPF protocol using model checking. We model parts of the OSPF standard and use a model checker tool to automatically find vulnerabilities which are inherent to the design of the protocol on simple network topologies. We then extend our analysis to more general network topologies. We develop a novel technique for parameterized networks that allows finding general attacks which are applicable to families of networks.
Next, we develop a security analysis method for the BGP protocol. We focus on traffic attraction attacks, where an attacker sends false routing advertisements to gain attraction of extra traffic in order to increase its revenue from customers, drop, tamper, or snoop on the packets. We use model checking to perform exhaustive search for attraction attacks on BGP. To deal with scalability issues of the entire Internet topology, we propose static methods to identify and automatically reduce Internet fragments of interest. Using a model checking tool we identify attacks as well as show that certain attraction scenarios are impossible on the Internet under the modeled attacker capabilities.
Finally, we propose a formal black box method to reveal 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. We cope with scalability issues using optimizations that are tailored to analysis of network protocols. They 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.