000231983 001__ 231983
000231983 005__ 20190317000848.0
000231983 0247_ $$2doi$$a10.1145/3098822.3098833
000231983 02470 $$2ISI$$a000414280000011
000231983 037__ $$aCONF
000231983 245__ $$aA Formally Verified NAT
000231983 269__ $$a2017
000231983 260__ $$bAssoc Computing Machinery$$c2017$$aNew York
000231983 300__ $$a14
000231983 336__ $$aConference Papers
000231983 520__ $$aWe 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/
000231983 6531_ $$aNetwork function verification
000231983 6531_ $$alazy proofs
000231983 6531_ $$asymbolic execution
000231983 700__ $$0248854$$g244739$$aZaostrovnykh, Arseniy
000231983 700__ $$0(EPFLAUTH)223572$$g223572$$aPirelli, Solal
000231983 700__ $$0250454$$g276547$$aPedrosa, Luis David
000231983 700__ $$aArgyraki, Katerina$$0243542$$g176638
000231983 700__ $$0241982$$g172241$$aCandea, George
000231983 7112_ $$dAugust 21-25, 2017$$cLos Angeles, CA, USA$$aACM SIGCOMM Conference
000231983 773__ $$tProceedings of the ACM SIGCOMM Conference
000231983 8564_ $$uhttps://infoscience.epfl.ch/record/231983/files/vignat-sigcomm17.pdf$$zPublisher's version$$s896808$$yPublisher's version
000231983 909C0 $$xU12550$$0252412$$pNAL
000231983 909CO $$ooai:infoscience.tind.io:231983$$qGLOBAL_SET$$pconf$$pIC
000231983 917Z8 $$x176638
000231983 917Z8 $$x176638
000231983 937__ $$aEPFL-CONF-231983
000231983 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000231983 980__ $$aCONF