3 ms·

What would be more interesting, and useful, compared to all these network stacks, would be a machine readable specification of TCP/IP from which a correct imple

What would be more interesting, and useful, compared to all these network stacks, would be a machine readable specification of TCP/IP from which a correct implementation could be engineered. However, the realist in me concedes, the specification itself, given the present state of the art, would probably fix, unsatisfactorily, many implementation details (in order for the implementation to pass the spec). I believe we need a network protocol with a solid, simple semantics. IP, that is not.

hannesm 10y ago
You have seen the network semantics research project https://www.cl.cam.ac.uk/~pes20/Netsem/index.html https://www.cl.cam.ac.uk/~pes20/Netsem/index.html? It is a formal model of TCP/IP validated with Linnux 2.4.20/FreeBSD-4.6/Windows XP (yes, that was ~10 years ago). It is nowadays BSD licensed on GitHub https://github.com/PeterSewell/netsem https://github.com/PeterSewell/netsem (and I'm currently reviving it https://www.cl.cam.ac.uk/~pes20/HuginnTCP/ https://www.cl.cam.ac.uk/~pes20/HuginnTCP/)...
- throwaway000002 10y ago
  No, I wasn't aware. Thank you for pointing this work out. This is exactly the kind of thing I was hoping for. Wonderful! I can't wait to see what you have planned. I was thinking after I posted my comment, that it'd be cool if someone could produce a fuzz tester that used both the specification, and the fact that you can turn the Linux and NetBSD network stacks into libraries (libOS and rumpkernel respectively) and co-engineer/evolve the spec whilst also finding and fixing bugs in both the network stacks. Excited by what you'll be up to!
  - hannesm 10y ago
    hmm, my other OS is MirageOS (https://mirage.io https://mirage.io) -- also see https://nqsb.io https://nqsb.io contains my previous two years of work ;) I'd rather call it extensive exploration than fuzz testing what is in my mind...

hannesm 10y ago

You have seen the network semantics research project https://www.cl.cam.ac.uk/~pes20/Netsem/index.html https://www.cl.cam.ac.uk/~pes20/Netsem/index.html? It is a formal model of TCP/IP validated with Linnux 2.4.20/FreeBSD-4.6/Windows XP (yes, that was ~10 years ago). It is nowadays BSD licensed on GitHub https://github.com/PeterSewell/netsem https://github.com/PeterSewell/netsem (and I'm currently reviving it https://www.cl.cam.ac.uk/~pes20/HuginnTCP/ https://www.cl.cam.ac.uk/~pes20/HuginnTCP/)...

throwaway000002 10y ago
No, I wasn't aware. Thank you for pointing this work out. This is exactly the kind of thing I was hoping for. Wonderful! I can't wait to see what you have planned. I was thinking after I posted my comment, that it'd be cool if someone could produce a fuzz tester that used both the specification, and the fact that you can turn the Linux and NetBSD network stacks into libraries (libOS and rumpkernel respectively) and co-engineer/evolve the spec whilst also finding and fixing bugs in both the network stacks. Excited by what you'll be up to!
- hannesm 10y ago
  hmm, my other OS is MirageOS (https://mirage.io https://mirage.io) -- also see https://nqsb.io https://nqsb.io contains my previous two years of work ;) I'd rather call it extensive exploration than fuzz testing what is in my mind...