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.
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…
(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,…
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.
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…
(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,…