Accelerating the development of a library of verified NF data structures
Team
| Argyraki Katerina |
| Candea George |
| Pirelli Solal |
Networks comprise an essential component of computational infrastructure. However, it is crucial to apply verification to ensure the integrity of networks and ascertain their conformity to current and future configurations. In this process, the security of most networks hinges on a network address translation (NAT), which connects the internal network to the public internet. Although there is a body of literature on network verification, very few studies have looked at the verification of software network functions (NF). That is the rationale underlying a study being conducted by a team of EPFL researchers.
Unlike previous studies, the current research presents a NAT function written in C to implement the semantics specified in RFC 3022. By using C, the researchers leverage the DPDK packet-processing library to ensure crash-free, bug-free, and memory-safe implementation. While existing literature points to the lack of scalability in verifying an NF written in C, the researchers meet this challenge by proposing a new combination of symbolic execution and proof checking using separation logic, thus ensuring no compromise on performance. In fact, the verified NAT (VigNAT) offers latency similar to that in unverified NAT.
In verifying NAT, the researchers adopt the Vigor approach. Vigor is a verification toolchain that contains a library of verified data structures called libVig. Software development with Vigor centers around three clear developer roles: libVig developers, standards developers, and NF developers.
The researchers evaluated the performance of VigNAT by comparing it with three other NFs. The results revealed that VigNAT had 2% higher latency than Unverified NAT, and 8% higher than No-op forwarding. Conversely, Linux NAT exhibited a much higher latency. The plots for throughput showed that VigNAT had a throughput of 1.8 Mpps, 10% lower than that of the Unverified NAT, while the Linux NAT had a throughput of only 0.6 Mpps. The evaluation demonstrated that a verified NAT can be used for competitive performance.
This research could provide important pointers for many other software NFs and help accelerate the development of a library of verified NF data structures.
The project is being conducted by Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina Argyraki, and George Candea. They are affiliated to EPFL’s School of Computer and Communication Sciences.
Suggested readings:
Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina Argyraki, and George Candea. 2017. A Formally Verified NAT. Proceedings of SIGCOMM ’17, Los Angeles, CA, USA, August 21-25, 2017.
Sourced at https://vignat.github.io/vignat-paper.pdf