1. 3

Abstract: “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 here.”


  2. [Comment removed by author]

    1. 2

      I havent thoroughly read/vetted this one yet. My skimming of it showed they do verified data structures, use KLEE for symbolic analysis, and tie things together with contracts. KLEE and contracts have a bunch of bugs exposed in the field as empirical justification for their use. The things worth more exploration are how libVigor works (esp formalism) plus their specs for safety of things like pointers.

      Even if those unknowns were bogus, the NAt-level specs and/or empirical components they’re chaining may prove useful to a reader doing something similar. So I submitted it for that.

      1. 3

        They use KLEE (well worth investigating) to “..prove that VigNAT is free of the following undesired behaviors: buffer over/underflow, invalid pointer dereferences, misaligned pointers, out-of-bounds array indexing, accessing memory that is not owned by the accessor, use after free, double free, type conversions that would overflow the destination, division by zero, problematic bit shifts, and integer over/underflow. Proving these properties boils down to proving that a set of assertions introduced in the VigNAT code—either by default in the KLEE symbolic execution engine [9] or using the LLVM undefined behavior sanitizers [42, 43, 57]—always hold.”

        At least they define what level of proof they achieve.

        1. 3

          KLEE can be used to prove some other things, you can make assertions on the symbolic values and thus prove properties about them.

      2. 1

        Just reread the paper in more detail. They do more than I originally thought. They annotate the code to collect lots of state information during program execution. When the program terminates this state information is checked for consistency “… we wrote a NAT specification that formalizes our interpretation of the RFC, and which we believe to be consistent with typical NAT implementations.”

        I did not see an discussion of how they obtained all the input necessary to invoke all of the behavior specified by RFC 3022. Runtime checks are limited by the input that gets processed.

        1. 1

          FWIW, in my opinion it is better to put such an update as an edit note in the original, rather than delete it. Gives better context and would probably stop any down votes.