TY - CPAPER
DO - 10.1145/3098822.3098833
AB - 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/
T1 - A Formally Verified NAT
DA - 2017
AU - Zaostrovnykh, Arseniy
AU - Pirelli, Solal
AU - Pedrosa, Luis David
AU - Argyraki, Katerina
AU - Candea, George
JF - Proceedings of the ACM SIGCOMM Conference
PB - Assoc Computing Machinery
PP - New York
ID - 231983
KW - Network function verification
KW - lazy proofs
KW - symbolic execution
UR - http://infoscience.epfl.ch/record/231983/files/vignat-sigcomm17.pdf
ER -