Network Programming via Computable Products

TL;DR

This paper introduces a novel software paradigm for 5G network user plane functions, leveraging computable products inspired by model checking to enable efficient, provably correct, and adaptable network service implementation.

Contribution

It presents a new approach for UPF programming based on product computation and state invariants, improving upon existing network dataplane languages.

Findings

Computed products for UPF example demonstrate feasibility.

Inferred state invariants eliminate separate formal verification.

Generated code adapts dynamically to traffic distribution.

Abstract

The User Plane Function (UPF) aims to provide network services in the 3GPP 5G core network. These services need to be implemented on demand inexpensively with provable properties. Existing network dataplane programming languages are not up to the task. A new software paradigm is presented for the UPF. It is inspired by model checking a concurrent reactive system where conceptually each component of the system is modeled as an extended finite-state machine and their product is verified. We show how such a product can be computed for one example of a UPF and how its state invariants can be inferred, thereby eliminating the need to formally verify the product separately. Code can be generated from the product and regenerated on the fly to remain optimal for the probability distribution of network traffic the UPF must process.