Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking : a case study

Internet protocols are intrinsically complex to understand and validate, due both to the potentially unbounded number of entities involved, and to the complexity of interactions amongst them. Yet, their safety is indispensable to guarantee the proper behavior of a number of critical applications. In this work, we apply formal methods to verify the safety of the Address Resolution Protocol (ARP), a standard protocol of the TCP/IP stack i.e. the communication protocols used by any Internet Host, and we are able to formally prove that the ARP protocol, as defined by the standard Request for Comments, exhibits various vulnerabilities which have been exploited since many years and still are the main ingredient of many attack vectors. As a complementary result we also show the feasibility of formal verification methods when applied to real network protocols.