SolalPirelli

Good point. Will talk about it with the other authors. Thanks.

Yes, existing connections are kept as long as there is traffic often enough (in either direction) - the timeout is configurable.

Out of scope, this work is purely about semantic correctness.

It only supports IPv4, but supporting IPv6 is likely trivial since none of the verification depends on the type used for representing IPs.

The size of the flow table is configurable, and the NAT drops connections once the table is full. (Of course, the NAT also expires old connections)

For a look at the underlying libraries, read the follow-up "A Formally Verified NAT Stack", which includes DPDK (the kernel-bypass framework used by the NAT) and its network card driver in the verification. In fact, my plane is about to take off for Budapest, where I'll be presenting that work, as I type this. :-)

Paper link: http://dslab.epfl.ch/pubs/formally-verified-nat-stack.pdf

(2nd author of the paper here)

By "implementation bugs" we mean _any_ bug that could cause the NAT to not satisfy its spec, which is a formalized version of RFC 3022.

This includes bugs that a type system would catch, such as improper use of void pointers, as well as lack of crashes (e.g. Out-of-bounds indexing, division by zero...); but most importantly, it includes _semantic_ bugs, such as forwarding a packet to the wrong port, incorrectly modifying a packet, not updating the internal state properly (so that future packets are handled correctly), etc.

The main contribution here is that only the data structures (which are reusable) need to be proven by hand; for a new NF, you only need a specification - which is, as you point out, not always easy to do.