Formal verification of the Address Resolution Protocols through SMT-based model checking - A case study -


Valid XHTML 1.0 Strict
Valid CSS!

  Abstract

In this work, we apply formal methods to verify the safety of the Address Resolution Protocol – used in any communication between hosts in Internet – showing on one hand the feasibility of formal verification of network protocols, and on the other hand the vulnerabilities suffered by this specific protocol with the aim of contributing to the development of a safer Internet.

The developed models and the results obtained in our experiments are described in the paper [1] by Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi and Elena Pagani, Formal verification of the Address Resolution Protocols through SMT-based model checking - A case study -, accepted for publication in the Proceedings of the 13th International Conference on integrated Formal Methods (iFM), 2017.

  Index

In this work, we analyze the safety of different versions of the Address Resolution Protocol (ARP) as it is described in the different standard documents. Safety is defined in terms of the capability of the protocol in coping with (i) Man-in-the-Middle attacks - where a malicious host convinces one or both ends of a conversation that the IP address of the other part corresponds to its own MAC address, thus deviating and intercepting the traffic destined to the victim part - and (ii) Denial-of-Service attacks - where a malicious host convinces another host that they have the same IP address, thus forcing the victim to dismiss its address and temporarily disconnect from the network while configuring an alternative address.
The standard documents under verification are:

In the Code section and Results section there are respectively the files we used with MCMT and some experimental statistics. In the Tools section, links for the use of MCMT are available.

  Code

In this section, the models developed for the formal verification of the Address Resolution Protocol are supplied. In order to replicate our experiments, the MCMT model checker for infinite state systems must be used (see Tools section).
The codes for models M2 and M3 allows verification with respect to both MitM and DoS attack; the appropriate conjunct describing bad states must be uncommented while the other must be commented before running the model.

No warranty disclaim: this software is free and, as such, it comes with no warranty. By using this software, you are accepting the terms stated here. Because the program is licensed free of charge, there is no warranty for the program, to the extent permitted by applicable law. The entire risk as to the quality and performance of the program is with you. Should the program prove defective, you assume the cost of all necessary servicing, repair or correction directly or indirectly derived from its use.

Algorithm Condition Model
ARP [RFC 826] no malicious host [Download]
ARP [RFC 826] malicious host sending broadcast Requests [Download]
ARP [RFC 826] malicious host sending unicast Requests [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M1 - no malicious host [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M1 - malicious host sending broadcast messages [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M1 - malicious host sending unicast messages [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - no malicious host [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - malicious host sending broadcast messages [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - malicious host sending unicast messages [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - no malicious host [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - malicious host sending broadcast messages [Download]
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - malicious host sending unicast messages [Download]
Address Conflict Detection [RFC 5227] M4 - no malicious host [Download]
Address Conflict Detection [RFC 5227] M4 - malicious host sending broadcast messages [Download]
Address Conflict Detection [RFC 5227] M4 - malicious host sending unicast messages [Download]

  Tools

The supplied code can be run using MCMT [4]. For basic information about how to use MCMT, please refer to the following website, where the executable code for MCMT may be downloaded for different architectures.
MCMT must be linked to the SMT solver Yices; in details, it uses Yices version 1.0.40.

  Results

The supplied code was run on an Intel Core i7 running Linux Ubuntu 14.04 64 bits. For safety with respect to DoS attacks, a threshold=5 was used. The reported results show: the considered standard protocol, the modeled condition, the type of attack for which safety is tested, the safety result, the running time, the maximum depth of the analyzed status tree, the number of tree nodes explored, the number of calls to the SMT tool, and the maximum length (in number of literals) of the formulas passed to the SMT tool.

Algorithm Condition Property Outcome Time (s.) Max. depth Nodes SMT calls # literals
ARP [RFC 826] no malicious host MitM safe 0.222 2 3 249 7
ARP [RFC 826] malicious host sending broadcast Requests MitM unsafe 0.211 5 12 395 10
ARP [RFC 826] malicious host sending unicast Requests MitM unsafe 0.150 5 12 457 10
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M1 - no malicious host MitM safe 0.392 2 4 508 7
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M1 - malicious host sending broadcast messages MitM unsafe 0.260 3 7 638 8
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M1 - malicious host sending unicast messages MitM unsafe 0.379 2 5 698 8
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - no malicious host MitM safe 0.268 2 4 741 8
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - malicious host sending broadcast messages MitM unsafe 0.439 3 6 870 8
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - malicious host sending unicast messages MitM unsafe 0.311 2 5 895 9
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - no malicious host DoS safe 0.330 2 3 737 7
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - malicious host sending broadcast messages DoS unsafe 44.85 18 1008 30569 23
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M2 - malicious host sending unicast messages DoS unsafe 104.93 19 1450 74162 24
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - no malicious host MitM safe 0.380 2 5 1111 8
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - malicious host sending broadcast messages MitM unsafe 0.417 3 7 1236 8
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - malicious host sending unicast messages MitM unsafe 0.409 2 6 1219 9
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - no malicious host DoS safe 0.419 2 3 1092 8
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - malicious host sending broadcast messages DoS unsafe 843.2 49 6032 633415 25
Link-Local [RFC 3927]; Conflict Detection [RFC 5227] M3 - malicious host sending unicast messages DoS unsafe 1716.8 49 8180 1355491 26
Address Conflict Detection [RFC 5227] M4 - no malicious host MitM safe 0.306 2 5 991 8
Address Conflict Detection [RFC 5227] M4 - malicious host sending broadcast messages MitM unsafe 0.401 3 7 1108 8
Address Conflict Detection [RFC 5227] M4 - malicious host sending unicast messages MitM unsafe 0.415 2 6 1091 9

  Bibliography

[1] Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi, Elena Pagani.
Formal verification of the Address Resolution Protocols through SMT-based model checking - A case study -
Accepted for publication in the Proceedings of the 13th International Conference on integrated Formal Methods (iFM), 2017.
[2] S. Cheshire.
IPv4 Address Conflict Detection.
RFC 5227, Jul.2008.
[3] S. Cheshire, B. Aboba and E. Guttman.
Dynamic Configuration of IPv4 Link-Local Addresses.
RFC 3927, May 2005.
[4] Silvio Ghilardi, Silvio Ranise.
MCMT: a Model Checker Modulo Theories.
Proc. of IJCAR'10, Springer LNCS, vol. 6173, pp. 22-29, 2010.
[5] D.C. Plummer.
An Ethernet Address Resolution Protocol – or – Converting Network Protocol Addresses to 48.bit Ethernet Address for Transmission on Ethernet Hardware.
RFC 826, Nov.1982.

  Authors