Verification of programmable networks
Coordinators: Said Jawad Saidi, Seifeddine Fathalli
The underlying networks serving the online services and applications of a business must be reliable, secure, and highly available. Outages caused by defective network devices, misconﬁgurations, or security breaches can lead to expensive losses. Consequently, network veriﬁcation is a crucial task in the network management and control process. In the traditional networking paradigm, there is a ﬁxed set of functionalities that devices such as IP-based routers and Ethernet-based switches support. Speciﬁcally, in these devices, it is not easy to modify the control plane (the decision-making component) without the manufacturer’s intervention. The control plane and the data plane (the component responsible for forwarding the traﬃc based on the decisions made by the control plane) are highly coupled together.
Thus, network operators can only conﬁgure these devices which makes the orchestration and management of these devices a daunting task in highly customized environments. Software-deﬁned Networking (SDN) was ﬁrst proposed as a new paradigm that introduces programmability to the control plane. It separates the control plane from the data plane in the devices and places the control plane in a logically centralized software SDN controller. This decoupling lets the SDN controller, often running in commodity hardware, manage multiple data plane devices (i.e., SDN switches). However, in traditional SDNs the functionalities of devices were ﬁxed, and not programmable. Later, the P4 language was introduced to bring programmability to the data plane as well. P4 is a domain speciﬁc language with multiple abstractions for packet processing. It enables the ﬂexibility of data plane programming without sacriﬁcing the line-rate performance. And as a result, allow network administrators to implement custom network policies independent of the target devices. This opens up opportunities for novel uses of the network: e.g., in-band network telemetry, in-network caching, and in-network congestion control.
The increased capabilities of the programmability, however, are the portent of new challenges to the network correctness. In order to check the overall consistency of a network, we need to ﬁrst verify that the control plane is making decisions as expected by the network operator, i.e. the control plane is consistent with the management plane. Second, we need to check that the data plane is forwarding the traﬃc as expected by the control plane. The conventional wisdom is that in SDN, the logically centralized control plane has an accurate representation of the actual data plane state, e.g. network devices consistently match and forward the traﬃc as speciﬁed by the rules generated by the control plane. However, just like any other program, SDN switches and P4 programs are prone to software bugs or dataplane faults. The faults can manifest in many ways e.g., resulting in abnormal network behavior diﬀerent from the expected behavior or in other words, the control plane may be completely unaware of the abnormal data plane behavior caused by the faults on the dataplane.
Previous work in this area, however, lacks a holistic methodology to tackle this problem and thus, addresses only certain parts of the problem. Yet, the consistency of the overall system is only as good as its least consistent part. To that end, we need systems that perform consistency checking between diﬀerent planes and do not assume that the control plane has an accurate representation of the data plane state. In classic SDNs, motivated by an analogy of network consistency checking with program testing, we propose to add active probe-based network state fuzzing to our consistency check repertoire. Hereby, our system, PAZZ, combines production traﬃc with active probes to
periodically test if the actual forwarding path and decision elements (on the data plane) correspond to the expected ones (on the control plane).
Our insight is that active traﬃc covers the inconsistency cases beyond the ones identiﬁed by passive traﬃc. PAZZ prototype was built and evaluated on topologies of varying scale and complexity. Our results show that PAZZ requires minimal network resources to detect persistent data plane faults through fuzzing and localize them quickly while outperforming baseline approaches. For P4-enabled SDNs, we present P4CONSIST, a system that takes advantage of P4 to verify the control-data plane inconsistency. The workﬂow of P4Consist reposes on four main modules: a control plane module, a data plane module, an input traﬃc generator, and an analyzer. P4CONSIST continuously generates active probe-based traﬃc as an input to the network. For a given packet (5-tuple ﬂow) and a source-destination pair, the control plane module proactively gathers the topology and conﬁguration information in the form of an expected report. On the other side, the data plane module traces the forwarding behavior of each switch on the path using INT (In-band Network Telemetry) to continuously elicit telemetry data in the form of an actual report.
Finally, the analyzer compares the two results to detect control-data plane inconsistencies using depth-ﬁrst search (DFS) and symbolic execution. Experiments with our prototype show that P4CONSIST can verify the control-data plane consistency in the complex datacenter 4ary fat-tree (20 Switches) and multipath grid (4, 9, and 16 Switches)
topologies with 60k rules per switch within a minimum time of 4 minutes.
A. Shukla, S. J. Saidi, S. Schmid, M. Canini, T. Zinner, and A. Feldmann. Towards consistent SDNs: A case for network state fuzzing. IEEE Transactions on Network and Service Management, (Early Access), 2019.
A. Shukla, S. Fathalli, T. Zinner, A. Hecker, and S. Schmid. P4Consist: Toward consistent P4 SDNs. IEEE Journal on Selected Areas in Communications, 38(7):1293–1307, 2020.