VigNAT: A Formally Verified Performant NAT | Hacker News Reader

VigNAT: A Formally Verified Performant NAT

vignat.github.io

128 pointssigna1140 comments

> Our proof applies directly to the C code of a network function, and it demonstrates the absence of implementation bugs.

Isn’t this just like a type system? You specify what you want in types, and the type checker complains if there are implementation bugs (the inferred type doesn’t match the specified type).

Of course, this just means that the hard part is now correctly expressing all the invariants (and combinations hereof) of your program as a type/proposition.

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

IMO this kind of work is very important, and is necessary to be able to categorize computer science as engineering. How do you see the future of this kind of programming? Will it become much easier/semi automated? Even mainstream? Could we see operating systems made with these methods?

For embedded and security applications this is extremely important and there's already tons of work done in this field - for example sel4 (https://sel4.systems/), ivory/tower (https://ivorylang.org/), yosys (http://www.clifford.at/papers/2016/yosys-synth-formal/slides...) for FPGAs.

Do you mean 'programming'? Because 'Computer Science' doesn't really need to be categorized as engineering, being a science and all.

Yeah. It's the other way around. Science is about learning. Engineering is build things based on knowledge gained from using the scientific method.

Building things without using scientific knowledge is not engineering. It's hacking.

Yes. Mainstream programming is more art than engineering, like how we built buildings before statics.

Buildings before statics were not built by 'art'. That entire 'programming is not like engineering' analogy is just terrible in almost every conceivable dimension, despite its enduring popularity.

> Our proof ... demonstrates the absence of implementation bugs.

It's definitely a strong statement, and thanks for the qualification.

When I saw the words on the page I began to wonder about all the other things that could go wrong. e.g. There could be bug in software that does the code analysis, or the compiler, or underlying libraries or operating system, or (sigh) in the CPU.

Also, there could be unexpected behavior when the machine its running on is under load. It would also be interesting to see it subjected to some of the fuzz-testing software out there.

Overall, I think it's a great approach and worth pursuing. Thank you for releasing the source.

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

Does the formalization have anything that would catch timing side channels, or is that out of scope?

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

in theory a provable lack of timing side channels might be possible to formalize, but it would be a tremendous amount of work (from which we will benefit enormously once we do)

This is very cool work. Our group had talked about trying something similar to the "lazy proofs" idea several years ago, but we never got around to actually trying it out. So it's very exciting to see someone do it!

Hopefully your project leads to more work like this -- practical, fast, and verified for everyone to use.

The RFC can also contain bugs, like the Bluetooth ECDH 'validating y-property is optional' variant, or suggested and reused polys for RSA.

Testing with garbage is still effective testing for exploits or figuring bottlenecks that could cause denial of service or exploits due to race conditions.

Either way, don't trust anything or anyone. Test it before someone else does.

Thanks for the response!

> 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.

I guess my main point is that not only is it not easy to do, but writing the spec is also an error-prone process (just like writing the implementation), and errors in the spec cannot be caught by any machinery.

Not to say that this makes the process meaningless — not at all — but simply to say that “formally verified” doesn’t mean “bug-free”, it means going from the challenge being writing a correct implementation to writing a correct specification.

Isn’t this just like a type system?

I suspect that other languages seem even better as subjects for this kind of formal verification. Haskell and Rust come to mind. For the same reasons, Go and Smalltalk strike me as less suitable. (For those people who think I'm just a Go and Smalltalk partisan.)

Why choose this problem to solve in 2018? NAT is a hacky solution to an old problem which is fixed by IPv6.

Someone benefits from the fact that IPv6 is not being rolled out. The ability to participate as a full-blown citizen on the internet is something which several groups of people wish to minimize, prevent, regulate, or profit from.

This problem is chosen because it matters to some people. I agree, it's not a good thing.

It was not a design feature, but IPv4 NAT provides some anonymity that IPv6 will take away in the future (if it hasn't already).

ISPs in my area assign a prefix per customer; If you know the ISP, you know the length of the prefix, and can thus pinpoint the exact ISP customer with every connection.

On ISPv4+CGNAT, the common deployment, they can't do that.

The IPv4 equivalent of that is giving each customer their own IP which happens all the time now. Individual devices within a customer network can be uniquely identified with IPv6 though which is new.

The IPv4 equiv cannot and does not happen because of address pool size.

Most ISPs charge extra for a fixed IPv4; and many default to CGNAT which makes it impossible to correlate even within a 10 minute period.

code is also available here: https://github.com/vignat/vignat

yay !

Don't leave out NAT PCP (RFC6887)!

It's a must for p2p communication

https://tools.ietf.org/html/rfc6887

I wish they tested a few adversarial conditions as well, like for instance having MANY open nat connections. At some point the memory runs out, right ?

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)

Interesting. Does it keep actively used connections open so as to maintain as much functionality as possible if it's under attack ?

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

This is truly amazing work, I'm glad you chose Nat as your NF example. One minor question I haven't seen answered anywhere: For vignat, in the git repository and the paper, I see no mention of software license.

May I assume that it is in the public domain, or if not, BSD licensed?

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

How does symbolic execution w KLEE work to formally verify programs, are there tradeoffs in coverage? For complete coverage you'd have to get it to cover the whole possible spaces of states and execution paths of the analyzed system.

The way they work around state space explosion is pretty cool. They push all the state off into another module, whose correctness they verify using other methods. Then they tell the symbolic execution engine that the state-holding module does not misbehave. So it's a hybrid -- use each verification technique where it's strong, to shore up the weaknesses/shortcomings in the other one.

Anyone know if there is anyone working on an equivalent of ascl or verifast for golang?

How does this work with IPV6 ?

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

This leads to my second question. Why NAT if ipv6 and routing ? Surely the performance is better routing ?

It's easy to prove correctness for IPv6 NAT: if you're doing it, it's wrong.

Let's imagine a small business with two IPv6-capable ISPs & a router. They want to make effective use of their two links for load balancing & failover.

There's not a chance that BGP is going to get set up or that their own IP allocation is going to happen.

How do you propose they implement multi-homing for their entire network? How do you propose they balance their link utilization?

>There's not a chance that BGP is going to get set up or that their own IP allocation is going to happen.

Why not? There's no restrictions on V6, unlike V4 where a small biz might not be able to afford even a /24.

Here are the three most significant problems from my perspective:

(1) Cost - IP allocation isn't close to free, either in $ or in time/administrative overhead.

(2) Technical Complexity - Using routing protocols like BGP is not currently a process with enough automated tooling to make it realistic

Those problems could likely be overcome with concerted effort.

But the biggest problem of all may be what this would do to the size of global routing tables. We've already got a problem with routing table size exploding with more and more people advertising smaller and smaller prefixes. All of that high-performance ram is expensive. That routing table is globally replicated.

If it were affordable for everyone to announce their own prefixes, routing tables would be prohibitively large. I don't think we yet have any good answers to this problem, and I am genuinely interested if you are aware of any.

Reply on news.ycombinator.com