> 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.
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?
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. :-)
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.
> 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.
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.)
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 ?
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?
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.
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?
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.
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.
40 comments
[ 4.0 ms ] story [ 78.4 ms ] threadyay !
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.
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.
Building things without using scientific knowledge is not engineering. It's hacking.
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.
Paper link: http://dslab.epfl.ch/pubs/formally-verified-nat-stack.pdf
Hopefully your project leads to more work like this -- practical, fast, and verified for everyone to use.
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.
> 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.
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.)
May I assume that it is in the public domain, or if not, BSD licensed?
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?
Why not? There's no restrictions on V6, unlike V4 where a small biz might not be able to afford even a /24.
(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.
It's a must for p2p communication
https://tools.ietf.org/html/rfc6887
This problem is chosen because it matters to some people. I agree, it's not a good thing.
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.
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.