Towards Runtime Verification of Programmable Networks

Abstract

Today, we rely heavily upon Internet-connected devices, applications, and services. Such reliance makes it crucial for the underlying networks to be reliable and secure. However, network outages, bugs in network devices such as switches and routers, and security compromises of the critical network infrastructure happen and sometimes, incur losses in revenue. This makes network management and control important. Networking devices such as IP-based routers and ethernet-based switches are fxed-function devices. The control plane (that decides how to handle network traffc) and data plane (that forwards traffc according to the decisions made by the control plane) are bundled together within these devices. These devices can only be confgured by network operators and lack useful abstractions for network management and orchestration. This fundamental obstacle led to the need for new network management and control paradigms.

Software-defned Networking (SDN) emerged as a paradigm that introduced programmability to the control plane. SDN decouples the distributed control plane from the data plane and outsources the control plane to a logically centralized software SDN controller running on commodity hardware. SDN controller manages and controls several data plane devices (e.g., SDN switches) through a well-known interface called as OpenFlow. In particular, SDN offers a multitude of opportunities regarding management and control through programmability of the control plane that runs packet processing logic such as routing, ACL, switching, load balancing. However, SDN switches are mere fxed-function devices that can only be confgured via OpenFlow but cannot be programmed. To enhance SDNs, the Programming Protocol-independent Packet Processors (P4) language was introduced. P4 is a domain-specifc language that allows data plane programmability by writing custom programs known as P4 programs that are executed on data plane switches (e.g., P4 switches). These programs determine how the packets are processed by the P4 switches even when these switches are already deployed in a network. At the network level, a P4 network, comprises of an SDN controller that manages and controls underlying P4 switches. Together, SDN and P4 are complementary. The term programmable networks includes both Software-defned Networks (SDNs) as well as P4 networks.

However, as switches (e.g., P4 switches) and networks (e.g., SDNs and P4 networks) are programmed, complex bugs and faults surface especially, during runtime, i.e., under diverse workloads and pose unprecedented threats. To give an example of a single P4 switch, a programmer writes a P4 program defning packet processing and then deploys it on a P4 switch to decide the packet processing logic. However, programming errors or P4 switch-specifc errors may result in an abnormal switch behavior under active traffc. This necessitates the detection and elimination of bugs in a P4 program or a P4 switch. Moving away from a P4 switch to the network-level (e.g., SDNs and P4 networks), data plane faults such as software or hardware bugs, switch failures, misconfgurations of switches, and attacks occur. Moreover, the network control plane or SDN controller remains unaware of the existence of such data plane faults can result in control-data plane inconsistency. This necessitates sound mechanisms that verify the actual network data plane behavior against the expected network control plane behavior during runtime.

Alternate abstract:

Heutzutage verlassen wir uns vermehrt auf Geräte, Anwendungen und Services, die mit dem Internet verbunden sind. Diese Abhängigkeit erfordert es, dass das zugrundeliegende Netzwerk zuverlässig und sicher ist. Netzwerkausfälle, Fehler in Netzwerkgeräten wie Switches und Router, sowie Beeinträchtigungen der Sicherheit von kritischen Netzwerkinfrastrukturen passieren und bringen Umsatzverluste mit sich. Aus diesem Grund sind Netzwerkmanagement und -kontrolle unerlässlich. Netzwerkgeräte wie IP-basierte Router und Ethernet-basierte Switches sind traditionell als vertikal integrierte Geräte mit fest verbauter Funktionalität, d.h. gebündelter Kontroll- und Datenebene, bekannt. Solche Geräte können durch Netzbetreiber lediglich konfguriert werden, weshalb sie deutliche Nachteile im Bereich der Abstraktion von Netzwerkmanagement und -orchestrierung haben. Hieraus entstand die Notwendigkeit neuer Paradigmen für Netzwerkkontrolle und -management.

Software-Defned Networking (SDN) entstand als Paradigma, das Programmierbarkeit von Netzwerken ermöglicht. SDN trennt die zuvor verteilte Kontrollebene von der Datenebene, die nun in einem logisch-zentralisierten SDN Controller konsolidiert wird und als Software auf Standardhardware ausgeführt werden kann. Der SDN Controller managt und kontrolliert mehrere Geräte auf Datenebene (z.B. SDN Switches), über eine als OpenFlow bekannte Schnittstelle und bietet gleichzeitig, durch die Programmierbarkeit der Kontrollebene, eine Reihe von Möglichkeiten. Nichtsdestotrotz verbleiben SDN Switches als Geräte mit fest verbauter Funktionalität, die lediglich konfguriert, nicht aber programmiert werden können. Um die Programmierbarkeit zu ermöglichen, wurde die Programmiersprache Protocol-independent Packet Processors (P4) entwickelt. P4 ist eine domänenspezifsche Sprache, welche die Programmierbarkeit der Datenebene, durch das Entwickeln von benutzerdefnierten Programmen (sogenannten P4 Programmen), die auf Switches der Datenebene (z.B. P4 Switches) ausgeführt werden, ermöglicht. Diese Programme geben vor wie Pakete verarbeitet werden sollen, selbst wenn die P4 Switches bereits im Einsatz sind. Auf Netzwerkebene besteht ein P4 Netzwerk aus einem SDN Controller, der die untergeordneten P4 Switches managt und kontrolliert. Insgesamt sind SDN und P4 komplementär und können in Verbindung miteinander eingesetzt werden. Als Resultat entwickelte sich der Begriff programmierbare Netzwerke als Sammelbegriff, sowohl für Software-defned Networks (SDNs), als auch P4 Netzwerke.

Mit der erhöhten Programmierbarkeit von Switches (z.B. P4 Switch), sowie Netzwerken (z.B. SDNs und P4 Netzwerke), treten insbesondere zur Ausführung unterschiedlicher Arbeitslasten komplexe Bugs und Fehler zu Tage, die bis dato nie dagewesene Bedrohungen darstellen. Um ein Beispiel für einen einzelnen P4 Switch zu nennen: Ein Programmierer schreibt ein P4 Programm, das die Paketverarbeitung defniert und stellt dieses dann auf einem P4 Switch bereit. Programmierfehler oder P4 Switch-spezifsche Fehler manifestieren sich jedoch als Bugs, die in einem ungewöhnlichen Switch-Verhalten unter unterschiedlichem Datenverkehr resultieren. Sowohl die Erkennung als auch die Beseitigung von Bugs erlangen daher gröûte Bedeutung. Wenn der Fokus von einem P4 Switch auf die Netzwerkebene (z.B. SDNs und P4 Netzwerke) verlagert wird, zeigt sich, dass Fehler auf der Datenebene wie Software- oder Hardwarebugs, Hardwarefehler, Fehlkonfgurationen und Angriffe allgegenwärtig sind. Schlimmer noch: die Netzwerk-Kontrollebene oder der SDN Controller sind im Unklaren über die Exis5 tenz solcher Fehler auf Datenebene, was zu Inkonsistenzen zwischen Kontroll- und Datenebene führt während der Datenverkehr über das Netzwerk fieût. Dies erfordert solide Mechanismen, die das tatsächliche Verhalten der Datenebene mit dem erwarteten Verhalten der Kontrollebene während der Laufzeit vergleichen, um erforderliche Korrekturmaûnahmen einleiten zu können.