Development and Evaluation of Methodologies for Vulnerability Analysis of Ad-hoc Routing Protocols

Abstract

This thesis presents a number methodologies for computer assisted vulnerability analysis of routing protocols in ad-hoc networks towards the goal of automating the process of finding vulnerabilities (possible attacks) on such network routing protocols and correcting the protocols. The methodologies developed are (each) based on a different representation (model) of the routing protocol, which model predicated the quantitative methods and algorithms used. Each methodology is evaluated with respect to effectiveness feasibility and possibility of application to realistically sized networks. The first methodology studied is based on formal models of the protocols and associated symbolic partially ordered model checkers. Using this methodology, a simple attack in unsecured AODV is demonstrated. An extension of the Strands model is developed which is suitable for such routing protocols. The second methodology is based on timed-probabilistic formal models which is necessary due to the probabilistic nature of ad-hoc routing protocols. This second methodolgy uses natural extensions of the first one. A nondeterministic-timing model based on partially ordered events is considered for application towards the model checking problem. Determining probabilities within this structure requires the calculation of the volume of a particular type of convex volume, which is known to be #P-hard. A new algorithm is derived, exploiting the particular problem structure, that can be used to reduce the amount of time used to compute these quantities over conventional algorithms. We show that timed-probabilistic formal models can be linked to trace-based techniques by sampling methods, and conversely how execution traces can serve as starting points for formal exploration of the state space. We show that an approach combining both trace-based and formal methods can have faster convergence than either alone on a set of problems. However, the applicability of both of these techniques to ad-hoc network routing protocols is limited to small networks and relatively simple attacks. We provide evidence to this end. To address this limitation, a final technique employing only trace-based methods within an optimization framework is developed. In an application of this third methodology, it is shown that it can be used to evaluate the effects of a simple attack on OLSR. The result can be viewed (from a certain perspective) as an example of automatically discovering a new attack on the OLSR routing protocol.