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 (LECTURE NOTES IN COMPUTER SCIENCE). - 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 [10.1007/978-3-319-66845-1_26].

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

D.M. Bruschi;S. Ghilardi;A. Lanzi;E. Pagani
2017

Abstract

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.
ARP; Man-in-the-Middle attack; Denial-of-Service attack; Formal verification; Model evaluation; Satisfiability Modulo Theories
Settore INF/01 - Informatica
set-2017
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/524647
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact