SolalPirelli

4 ms·

1. 1.▲
   by SolalPirelli 8y ago

   Good point. Will talk about it with the other authors. Thanks.
2. 2.▲
   by SolalPirelli 8y ago

   Yes, existing connections are kept as long as there is traffic often enough (in either direction) - the timeout is configurable.
3. 3.▲
   by SolalPirelli 8y ago

   Out of scope, this work is purely about semantic correctness.
4. 4.▲
   by SolalPirelli 8y ago

   It only supports IPv4, but supporting IPv6 is likely trivial since none of the verification depends on the type used for representing IPs.
5. 5.▲
   by SolalPirelli 8y ago

   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)
6. 6.▲
   by SolalPirelli 8y ago

   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 ab
7. 7.▲
   by SolalPirelli 8y ago

   (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 impr