Safe and Secure Software-Defined Networks in P4

This thesis is about software-defined networking (SDN), an alternative to traditional network design which provides a greater degree of configurability and control. In particular, it focuses on the P4 framework, which is considered the de-facto standard for SDN programming.

While the programmability of SDNs can be leveraged to provide increased security guarantees and to enforce correct communication over the network, the increase in programmability also opens up for higher risks of bugs being introduced into the network configuration.

This thesis addresses two research questions:
1. Can we provide safety guarantees for P4 control plane programs?
2. Can we provide safety guarantees for networks by leveraging P4?

This thesis answers both positively, presenting the following results:
1. A formal model for P4 control plane programs, servers and networks, including a semantics and type system, as well as a detailed proof proving the type safety of the model.
2. A Scala 3 API that implements the type checks and guarantees of our formal model, and is capable of updating real-life P4 devices.
3. A design of network-layer runtime monitors capable of observing and enforcing application-level protocols specified as session types.
4. An implementation of our monitor design in P4, with accompanying tooling and an evaluation showing that this approach can be be used to monitor real-world examples that use real-world protocols.

With these results, this thesis shows that it is possible to both improve the safety of SDNs and use SDNs to improve safety.