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.
Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking : a case study / D.M. Bruschi, A. Di Pasquale, S. Ghilardi, A. Lanzi, E. Pagani - In: Integrated Formal Methods / [a cura di] N. Polikarpova, S. Schneider. - Prima edizione. - [s.l] : Springer, 2017 Sep. - ISBN 9783319668444. - pp. 391-406 (( Intervento presentato al 13. convegno International Conference on Integrated Formal Methods tenutosi a Torino nel 2017.
|Titolo:||Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking : a case study|
|Parole Chiave:||ARP; Man-in-the-Middle attack; Denial-of-Service attack; Formal verification; Model evaluation; Satisfiability Modulo Theories|
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||set-2017|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1007/978-3-319-66845-1_26|
|Tipologia:||Book Part (author)|
|Appare nelle tipologie:||03 - Contributo in volume|