Forwarding Tables Verification through Representative Header Sets

Abstract : Forwarding table verification consists in checking the distributed data-structure resulting from the forwarding tables of a network. A classical concern is the detection of loops. We study this problem in the context of software-defined networking (SDN) where forwarding rules can be arbitrary bitmasks (generalizing prefix matching) and where tables are updated by a centralized controller. Basic verification problems such as loop detection are NP-hard and most previous work solves them with heuristics or SAT solvers. We follow a different approach based on computing a representation of the header classes, i.e. the sets of headers that match the same rules. This representation consists in a collection of representative header sets, at least one for each class, and can be computed centrally in time which is polynomial in the number of classes. Classical verification tasks can then be trivially solved by checking each representative header set. In general, the number of header classes can increase exponentially with header length, but it remains polynomial in the number of rules in the practical case where rules are constituted with predefined fields where exact, prefix matching or range matching is applied in each field (e.g., IP/MAC addresses, TCP/UDP ports). We propose general techniques that work in polynomial time as long as the number of classes of headers is polynomial and that do not make specific assumptions about the structure of the sets associated to rules. The efficiency of our method rely on the fact that the data-structure representing rules allows efficient computation of intersection, cardinal and inclusion. Finally, we propose an algorithm to maintain such representation in presence of updates (i.e., rule insert/update/removal). We also provide a local distributed algorithm for checking the absence of black-holes and a proof labeling scheme for locally checking the absence of loops.
Type de document :
[Research Report] Inria Paris Rocquencourt. 2016
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
Contributeur : Fabien Mathieu <>
Soumis le : mardi 26 janvier 2016 - 11:57:36
Dernière modification le : lundi 17 décembre 2018 - 01:26:46
Document(s) archivé(s) le : mercredi 27 avril 2016 - 13:21:42


Fichiers produits par l'(les) auteur(s)


Distributed under a Creative Commons Paternité 4.0 International License


  • HAL Id : hal-01262130, version 1
  • ARXIV : 1601.07002


Yacine Boufkhad, Ricardo De La Paz, Leonardo Linguaglossa, Fabien Mathieu, Diego Perino, et al.. Forwarding Tables Verification through Representative Header Sets. [Research Report] Inria Paris Rocquencourt. 2016. 〈hal-01262130〉



Consultations de la notice


Téléchargements de fichiers