45 ms·

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

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

drsopp 8y ago
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?
- flowless 8y ago
  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/ https://sel4.systems/), ivory/tower (https://ivorylang.org/ https://ivorylang.org/), yosys (http://www.clifford.at/papers/2016/yosys-synth-formal/slides.pdf http://www.clifford.at/papers/2016/yosys-synth-formal/slides...) for FPGAs.
- pvg 8y ago
  Do you mean 'programming'? Because 'Computer Science' doesn't really need to be categorized as engineering, being a science and all.
  - diroussel 8y ago
    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.
    - drsopp 8y ago
      Yes. Mainstream programming is more art than engineering, like how we built buildings before statics.
      - pvg 8y ago
        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.
billrobertson42 8y ago
> 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.
- 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 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 http://dslab.epfl.ch/pubs/formally-verified-nat-stack.pdf
0xcde4c3db 8y ago
Does the formalization have anything that would catch timing side channels, or is that out of scope?
- SolalPirelli 8y ago
  Out of scope, this work is purely about semantic correctness.
- DoctorOetker 8y ago
  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)
cvwright 8y ago
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.
diamondo25 8y ago
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.
runeks 8y ago
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.

drsopp 8y ago

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?

flowless 8y ago
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/ https://sel4.systems/), ivory/tower (https://ivorylang.org/ https://ivorylang.org/), yosys (http://www.clifford.at/papers/2016/yosys-synth-formal/slides.pdf http://www.clifford.at/papers/2016/yosys-synth-formal/slides...) for FPGAs.
pvg 8y ago
Do you mean 'programming'? Because 'Computer Science' doesn't really need to be categorized as engineering, being a science and all.
- diroussel 8y ago
  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.
  - drsopp 8y ago
    Yes. Mainstream programming is more art than engineering, like how we built buildings before statics.
    - pvg 8y ago
      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.

billrobertson42 8y ago

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

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 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 http://dslab.epfl.ch/pubs/formally-verified-nat-stack.pdf

0xcde4c3db 8y ago

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

SolalPirelli 8y ago
Out of scope, this work is purely about semantic correctness.
DoctorOetker 8y ago
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)

cvwright 8y ago

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.

diamondo25 8y ago

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.

runeks 8y ago

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.