Seit Mitte der 1990er Jahre gibt es Bestrebungen, eine flexiblere Verarbeitung von Netzwerkpaketen zu ermöglichen, indem Paketverarbeitung programmierbar wird. Mit dem Aufkommen von Software-Defined-Networking (SDN) ist diese Idee nun Realität geworden. Frühe Ansätze haben sich zunächst auf die Programmierung der Control-Plane konzentriert, mit dem Ziel, auf hohem Abstraktionsniveau zentrale Netzwerkrichtlinien zu realisieren, ohne systemnahe, gerätespezifische Konfigurationsmechanismen nutzen zu müssen. Hierfür entstanden diverse Programmiersprachen, die Korrektheitsgarantien gewähren und die formale Verifikation der Netzwerkrichtlinien ermöglichen. In jüngster Zeit ist es zudem auch möglich die Netzwerk-Data-Plane zu programmieren. Durch die Möglichkeit die Struktur von Netzwerkpaketheadern frei zu definieren, eröffnen sich eine Vielzahl neuer Anwendungsmöglichkeiten, von der Implementierung neuartiger Netzwerkprotokolle bis hin zur Auslagerung von Anwendungsfunktionalität direkt in das Netzwerk. Bis heute hat sich die Sprache P4 als Standard für die Programmierung von Data-Planes durchgesetzt. Zwar bietet P4 deklarative Abstraktionen für die Programmierung von Data-Planes, allerdings fehlen P4 grundlegende Sicherheitsgarantien, die dabei helfen Fehler zu vermeiden und korrekte Anwendungen für die Data-Plane zu implementieren. Modernen Programmiersprachen nutzen statische Typsysteme, um Sprachen mit grundlegenden Sicherheitsgarantien auszustatten, die das Auftreten ganzer Fehlerkategorien vollständig ausschließen. Überraschenderweise wurde der Einsatz von Typsysteme im Bereich der Netzwerkprogrammierung jedoch bislang kaum untersucht. Diese Dissertation untersucht wie geeignete Typsysteme aussehen müssen, um Data-Plane-Programmiersprachen – insbesondere P4 – mit statischen Korrektheitsgarantien auszustatten. Im ersten Schritt präsentieren wir SafeP4, eine domänenspezifische Sprache für programmierbare Data-Planes, die mit einem statischen Typsystem ausgestattet ist, das garantiert, dass alle Header, die gelesen oder geschrieben werden gültig sind, was eine häufige Ursache für Fehler ist. Im zweiten Schritt präsentieren wir Π4, dessen Typsystem auf Dependent-Types basiert und damit in der Lage ist, die Lücke hinsichtlich der Ausdrucksstärke zwischen SafeP4 und vollwertigen Verifikationswerkzeugen zu schließen. Gleichzeitig ermöglicht Π4 die modulare Verifikation von Programmen. Unsere Auswertung anhand von Open-Source-Programmen bestätigt, dass der Zugriff auf ungültige Paketheader in der Praxis eine häufige Fehlerquelle ist und das SafeP4s Typsystem in der Lage ist, fehlerhafte Programme zu identifizieren. Anhand von Fallstudien zeigen wir zudem, dass Π4s Typsystem imstande ist eine Vielzahl praktisch relevanter Korrektheitseigenschaften auszudrücken und zu verifizieren.