Formal verification of the ARPON protocols through SMT-based model checking


Valid XHTML 1.0 Strict
Valid CSS!

  Abstract

In this work, we apply formal methods to verify the safety of the ARPON protocols, namely SARPI and DARPI, showing on one hand the feasibility of formal verification of networks protocols, and on the other hand their safeties and vulnerabilities, 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, A formal verification of ARPON - a tool for avoiding man in the middle attacks in Ethernet networks, submitted for publication to IEEE/ACM Transactions on Networking.

  Index

In this work, we analyze the safety of the different protocols composing the ARPON infrastructure as it is described in [1]. ARPON aims at solving some well-known vulnerabilities suffered by the standard ARP protocol [3, 4, 6] and analyzed in [2]. Safety is defined in terms of the capability of the protocols in coping with 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. The relevance of ARPON lies in the fact that it does not require any form of cryptography, thus guaranteeing compatibility and interoperability with legacy implementations of ARP.
The protocols under verification are:

which have been modeled and verified using the MCMT tool [5]

In the next sections (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 SARPI and DARPI protocols are supplied. In order to replicate our experiments, the MCMT model checker for infinite state systems must be used (see Tools section).

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
SARPI MITM - no malicious host [Download]
SARPI MITM - malicious hosts sending broadcast Requests [Download]
SARPI MITM - malicious hosts sending unicast Requests [Download]
DARPI MITM - no malicious host [Download]
DARPI MITM - one malicious host sending broadcast messages [Download]
DARPI un-poisoning - generation of a base request from a victim [Download]
DARPI un-poisoning - generation of a base request to the victimn [Download]
DARPI un-poisoning - generation of an unsolicited reply [Download]
DARPI un-poisoning - comprehensive [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 particular, 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. 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.
The comprehensive DARPI model is run with option -S4.

Algorithm Condition Property Outcome Time (s.) Max depth Nodes SMT calls # literals
SARPI no malicious host MITM attack safe 0.128 s. 1 1 1166 2
SARPI any number of malicious hosts sending broadcast Requests MITM attack safe 0.144 s. 1 1 1346 2
SARPI any number of malicious hosts sending unicast Requests MITM attack safe 0.167 s. 1 1 1624 2
DARPI no malicious host MITM attack safe 0.381 s. 2 1 1745 11
DARPI malicious host sending broadcast messages MITM attack unsafe 67011 12 4352 2597327 12
DARPI generation of Request from victim - malicious host un-poisoning safe 25.35 19 291 35736 11
DARPI generation of Request to victim - malicious host un-poisoning safe 17.33 11 127 14157 11
DARPI generation of unsolicited Reply from malicious host un-poisoning safe 32.69 19 299 40276 11
DARPI comprehensive un-poisoning safe 304.3 20 1258 308682 18

  Bibliography

[1] Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi, Elena Pagani.
A formal verification of ARPON - a tool for avoiding man in the middle attacks in Ethernet networks
Accepted for publication in IEEE Transactions on Dependable and Secure Computing.
[2] 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 -
In Proc. 13th International Conference on integrated Formal Methods (iFM), 2017.
[3] S. Cheshire.
IPv4 Address Conflict Detection.
RFC 5227, Jul.2008.
[4] S. Cheshire, B. Aboba and E. Guttman.
Dynamic Configuration of IPv4 Link-Local Addresses.
RFC 3927, May 2005.
[5] Silvio Ghilardi, Silvio Ranise.
MCMT: a Model Checker Modulo Theories.
Proc. of IJCAR'10, Springer LNCS, vol. 6173, pp. 22-29, 2010.
[6] 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