Modeling and Formal Verification of DHCP using SPIN
Syed Mohammed Shamsul Islam, Mohammed H. Sqalli, Sohel Khan · 2006
The Dynamic Host Configuration Protocol (DHCP) is a widely used communication protocol. In this paper, a portion of the protocol is chosen for modeling and verification, namely the assignment of new IP address to a newly arriving host. PROcess Meta LAnguage (PROMELA) is used for modeling and the verification is performed using SPIN. SPIN can verify most of the communication protocols either by performing random simulations or by generating a C program. It can perform an exhaustive verification that can establish with mathematical certainty whether or not a given behavior is error-free. PROMELA is used to specify a system behavior in a formal validation model that defines interactions of processes in a distributed system and allows for the dynamic creation of concurrent processes. We have analyzed and verified various properties of the DHCP protocol such as absence of deadlock, livelock, and improper termination under various conditions such as message loss or arbitrary errors. We obtained the expected execution of the protocol using simulation. No invalid end-state or Non-progress cycle were found. We have also formalized a linear time temporal logic (LTL) to verify whether messages are exchanged properly and whether two clients may get the same IP address at the same time. No violation of the first claim was found, but the latter was violated.