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.
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-01262130
Contributor : Fabien Mathieu <>
Submitted on : Tuesday, January 26, 2016 - 11:57:36 AM
Last modification on : Tuesday, May 14, 2019 - 10:12:38 AM
Long-term archiving on : Wednesday, April 27, 2016 - 1:21:42 PM

Files

report.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

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

Citation

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⟩

Share

Metrics

Record views

725

Files downloads

210