Forwarding Tables Verification through Representative Headers

Forwarding table verification consists in checking the correctness of the forwarding tables of the routers of a given network. For example, one may want to verify the absence of loops or black-holes. In this paper, we propose a two-step approach to address tables verification: computing a representative set of packet headers; testing the desired properties only for these headers. The tricky part is to guaranty that this set of headers represents all possible headers in the sense that any header will behave exactly as one of the headers in the set. In a general model of forwarding rules inspired from Software Defined Networking (SDN), we show that a natural condition on the table rules inspired from the work of Boutier and Chroboczek about source-sensitive routing allows to compute a representative set whose size is linear in the number of rules in the tables. This has to be compared to the overall number of possible headers which is exponential in the number of bits in the headers.