Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study -

  • Danilo Bruschi
  • Andrea Di Pasquale
  • Silvio Ghilardi
  • Andrea Lanzi
  • Elena PaganiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


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 


  1. 1.
    Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721–736. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71209-1_56 CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Haziza, F., Holík, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476–495. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-35873-9_28 CrossRefGoogle Scholar
  3. 3.
    Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-28644-8_3 CrossRefGoogle Scholar
  4. 4.
    Alqahtani, A.H., Iftikhar, M.: TCP/IP attacks, defenses and security tools. Int. J. Sci. Mod. Eng. (IJISME) 1(10) (2013)Google Scholar
  5. 5.
    Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474–488. Springer, Heidelberg (2005). doi: 10.1007/11562948_35 CrossRefGoogle Scholar
  6. 6.
    Bellovin, S.M.: Security problems in the TCP/IP protocol suite. ACM SIGCOMM Comput. Commun. Rev. 19(2), 32–48 (1989)CrossRefGoogle Scholar
  7. 7.
    Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015)Google Scholar
  9. 9.
    Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-27813-9_29 CrossRefGoogle Scholar
  10. 10.
    Cheshire, S.: IPv4 Address Conflict Detection. RFC 5227, July 2008Google Scholar
  11. 11.
    Cheshire, S., Aboba, B., Guttman, E.: Dynamic Configuration of IPv4 Link-Local Addresses. RFC 3927, May 2005Google Scholar
  12. 12.
    Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Invariants for finite instances and beyond. In: Proceedings of FMCAD (2013)Google Scholar
  13. 13.
    Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31424-7_55 CrossRefGoogle Scholar
  14. 14.
    Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 67–82. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-71070-7_6 CrossRefGoogle Scholar
  15. 15.
    Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14203-1_3 CrossRefGoogle Scholar
  16. 16.
    Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. J. Log. Methods Comput. Sci. 6(4) (2010)Google Scholar
  17. 17.
    Islam, S.M.S., Sqalli, M.S., Khan, S.: Modeling and formal verification of DHCP using SPIN. Int. J. Comput. Sci. Appl. 3(6), 145–159 (2006)Google Scholar
  18. 18.
    Alford, M.W., Ansart, J.P., Hommel, G., Lamport, L., Liskov, B., Mullery, G.P., Schneider, F.B.: Formal foundation for specification and verification. In: Paul, M., et al. (eds.) Distributed Systems. LNCS, vol. 190, pp. 203–285. Springer, Heidelberg (1985). doi: 10.1007/3-540-15216-4_15 CrossRefGoogle Scholar
  19. 19.
    Plummer, D.C.: An Ethernet Address Resolution Protocol - or - Converting Network Protocol Addresses to 48.bit Ethernet Address for Transmission on Ethernet Hardware. RFC 826, November 1982Google Scholar
  20. 20.
    Wagner, R.: Address Resolution Protocol Spoofing and Man-in-the-Middle Attacks. The SANS Institute, Reston (2001)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Danilo Bruschi
    • 1
  • Andrea Di Pasquale
    • 1
  • Silvio Ghilardi
    • 2
  • Andrea Lanzi
    • 1
  • Elena Pagani
    • 1
    Email author
  1. 1.Università degli Studi di MilanoMilanoItaly
  2. 2.Università degli Studi di MilanoMilanoItaly

Personalised recommendations