Miyaji Laboratory

Abstract

The development of technologies such as SDN and NFV has increased the demand for software packet processing. With the widespread use of 10-100GbE, an environment that allows high-speed data communication between terminals is being developed, but software processing is slower than hardware processing, becoming a communication bottleneck. Kernel bypass technology is an example of a solution to this problem. Typical examples include Data Plane Development Kit (DPDK) and AF XDP of the eXpress Data Path (XDP) family. In addition, software bugs account for a high percentage of significant and customerimpacting incidents in network services, and research has been conducted to verify network functions using various methods. In this paper, we have designed a network function that achieves fast packet processing in user space using DPDK, memory safety using Rust language, and specification verification using Prusti. Furthermore, we developed a NAT based on the above design, and realized a NAT that satisfies high-speed packet processing, memory safety, and works without errors in the specification.