Automated Formal Verification of the DHCP Failover Protocol Using Timeout Order Abstraction

Abstract

In this paper, we present automated formal verification of the DHCP Failover protocol. We conduct bounded model-checking for the protocol using Timeout Order Abstraction (TO-Abstraction), a technique to abstract a given timed model in a certain sub-class of loosely synchronized real-time distributed systems into an untimed model. A resulting untimed model from TO-abstraction is a finite state machine, and therefore one can verify the model using a conventional model-checker. We have verified the protocol by bounded model-checking up to depth 20. We also experimented with "mutating" the original code to examine the efficiency of bug-finding using TO-Abstraction. We used two mutated pieces of the original code. The first one represents a model that uses a stronger failure assumption. The second one represents a model that the protocol implementer has forgot to add a certain check of a received message. We found one counterexample for each of two pieces of mutated code. In particular, the counterexample that was found for the second mutated code had a complex scenario, and we believe that it is considerably difficult to find the counterexample by human or simulations.