The AODV model

This section describes the AODV model for three implementations of the AODV protocol: mad-hoc (Version $1.0$) [21], Kernel AODV (Version $1.5$) [20], and AODV-UU (Version $0.5$) [13]. The mad-hoc implementation runs as a user space daemon and contains approximately $5500$ lines of code. The Kernel AODV implementation is built by NIST and is based on the mad-hoc implementation. It contains $7500$ lines of code and runs as a loadable kernel module in Linux and ARM based PDAs. The AODV-UU implementation runs as a user space daemon on Linux and has been ported to the ns-2 [22] simulator. It contains roughly $7700$ lines of code.

The AODV model was reused with minor modifications for all three implementations. The model is built as follows:

Table 1: Properties checked in AODV.

Types of Checks	Examples
Generic Assertions	Segmentation violations, memory leaks, dangling pointers.
Routing Loop Invariant	The routing tables of all nodes do not form a routing loop.
Assertions on Routing Table Entries	At most one routing table entry per destination.
	No route to self in the AODV-UU implementation.
	The hop count of the route to self is $0$, if present.
	The hop count is either infinity or less than the number of nodes in the network.
Assertions on Message Fields	All reserved fields are set to $0$.
	The hop count in the packet can not be infinity.

Table 2: The set of event handlers used in AODV model checking.

Enabling Condition	Event
Invalid or no route to destination	Initiation of route request
Pending message in the network	Receipt of AODV message
Pending message in the network	Message loss
Valid route in the routing table	Timeout of a route
Always enabled	Detection of link failure
Always enabled	Node reboot

Correctness Properties: Table 1 lists the correctness properties checked by the AODV model. Apart from the generic assertions checked by CMC, the model contains a global invariant that checks for routing loops. The model also performs sanity checks on the routing table entries and the network messages, such as range violations of the fields.

The Environment: The environment of the model consists of a network modelled as a bounded-length, unordered message queue. The model simulates a message loss by nondeterministically dequeuing a message. The message queue is shared by all of the nodes and thus models a completely connected topology.

The implementations use a wrapper function to send network packets. The model provides an alternate definition to the wrapper function to copy packets to the network model. Additionally, for the Kernel AODV implementation, the model provides implementations for twenty-two kernel functions (such as kmalloc and printk) and a user space version of the socket buffer library.

Initialization Functions and the Event Handlers: All three implementations have an event dispatch loop that calls various event handlers. The initialization functions of the model are obtained by executing the code before the event dispatch loop. The model maps every event handler called from the dispatch loop to a transition. The model simulates a node reboot by calling the initialization function which implicitly resets the contents of the routing table. The list of transitions and their respective enabling conditions is shown in Table 2.

Table 3: Lines of implementation code vs. CMC modelling code.

Protocol	Checked	Correctness	Environment			State
	Code	Specification	network	stubs	skbuff	Canonicalization
mad-hoc	3336	301	400	100	-	165
Kernel AODV	4508	301	400	266	1210	179
AODV-UU	5286	332	400	128	-	185

Table 3 shows the lines of code from the three implementations executed within our framework against the lines of code for the model itself. The correctness specifications are mostly shared by the three implementations. AODV-UU uses a different representation of the routing table and thus required additional correctness specifications. The network model of the environment is shared by all implementations.

Dealing with State Space Explosion

The state space of the AODV protocol is essentially infinite. The protocol allows an arbitrary number of nodes in a network. Also, each node has two types of unbounded counters, a sequence number to measure the freshness of a route and a broadcast id that is incremented by a node on each broadcast. To do any effective search in such an infinite state space, it is necessary to bound the search. In our experiments, we downscaled the AODV model to run with $2$ to $4$ processes. The model discarded any state in which the sequence numbers or the broadcast ids exceeded a predefined limit. Also, the size of the message queue in the network was bounded to sizes of $1$ to $3$. These processes may cause CMC to miss errors. However, even after applying such bounds, the remaining state space contained enough interesting behavior to uncover numerous bugs (Section 6).

Time values stored in the state are another source of state space explosion. For instance, every route response (RREP) contains a lifetime field that determines the freshness of the route. On receipt of this packet, a node adds the lifetime to the current clock value to determine the time at which the route becomes stale. This absolute value is stored in the routing table and can thus increase the state space size. The AODV model gets around this problem by modelling route timeouts as nondeterministic events and setting all time variables to predefined constants. Also, the environment of the model contains a definition of the gettimeofday() function that always returns a constant value. The handling of time in the model can miss timing related errors and can potentially lead to false positives when an error reported can be caused by a sequence of timeouts that is impossible in the real protocol.

Also, the AODV model contains hand-written code to traverse the routing table (implemented as a linked list in the mad-hoc and Kernel AODV implementations, and as a hash table in the AODV-UU implementation). This traversal code created a canonicalized representation of the routing table, which along with the global variables formed the state of an AODV node of the model. The amount of lines required for this traversal code is shown in the last column of Table 3.

Table 4: Number of bugs of each type in the three implementations of AODV. The figures in parenthesis show the number of bugs that are instances of the same bug in the mad-hoc implementation.

	mad-hoc	Kernel AODV		AODV-UU
Mishandling malloc failures	4	6		2
Memory Leaks	5	3		0
Use after free	1	1		0
Invalid Routing Table Entry	0	0		1
Unexpected Message	2	0		0
Generating Invalid Packets	3	2	(2)	1
Program Assertion Failures	1	1	(1)	1
Routing Loops	2	3	(2)	1	(1)
Total	18	16	(5)	6	(1)