Hacker News Reader

Comment by SolalPirelli | Hacker News Reader

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

View on HN

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

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.

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.

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.

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)

Reply on news.ycombinator.com