VigNAT: A Formally Verified NAT

Poster.png: 3310x4681, 1185k (July 20, 2018, at 04:06 PM)
Vigor Poster @ EDIC Open House 2018

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of network functions and proves properties specific to network configuration, such as reachability and absence of loops. Our proof applies directly to the C code of a network function, and it demonstrates the absence of implementation bugs. Prior work argued that this is not feasible (i.e., that verifying a real, stateful network function written in C does not scale) but we demonstrate otherwise: NAT is one of the most popular network functions and maintains per-flow state that needs to be properly updated and expired, which is a typical source of verification challenges. We tackle the scalability challenge with a new combination of symbolic execution and proof checking using separation logic; this combination matches well the typical structure of a network function. We then demonstrate that formally proven correctness in this case does not come at the cost of performance.

VigNAT Talk @ SIGCOMM'17

Further Reading

Main Website:

Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina Argyraki, and George Candea; A Formally Verified NAT. In Proceedings of the ACM Conference of the Special Interest Group on Data Communication (SIGCOMM'17). 2017
Open Website Download PDF Document Download MPEG-4 Video More Information
Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina Argyraki, and George Candea; Vigor: Practical Formal Verification of Network Functions. Presented at The Intel ISRA SDN/NFV Retreat, Hillsboro, OR, USA. 2017
Open Website Download PDF Document More Information

Getting the Source

The VigNAT source code is hosted on GitHub. To create a local copy of the repository run:

git clone