doi:10.1145/3098822.3098833
ISI:000414280000011
Zaostrovnykh, Arseniy
Pirelli, Solal
Pedrosa, Luis David
Argyraki, Katerina
Candea, George
A Formally Verified NAT
New York, Assoc Computing Machinery
http://infoscience.epfl.ch/record/231983/files/vignat-sigcomm17.pdf
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. The NAT code, proof toolchain, and proofs are available at https://vignat.github.io/
2017-10-30T09:37:23Z
http://infoscience.epfl.ch/record/231983
http://infoscience.epfl.ch/record/231983
Text