Re:Why do we use the Linux kernel's TCP stack?
by hannesm on Sunday July 03, 2016 @03:03AM
(#12025083)
You have seen the network semantics research project 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 (and I'm currently reviving it https://www.cl.cam.ac.uk/~pes20/HuginnTCP/)...
Re:Why do we use the Linux kernel's TCP stack?
by throwaway000002 on Sunday July 03, 2016 @09:17AM
(#12025920)
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!
Re:Why do we use the Linux kernel's TCP stack?
by hannesm on Sunday July 03, 2016 @10:03AM
(#12026082)
hmm, my other OS is MirageOS (https://mirage.io) -- also see 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...
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.