3 ms·

I struggle because I want to upvote these comments, because that's the world I want to live in. But the opposite side of that coin is who is going to author the

I struggle because I want to upvote these comments, because that's the world I want to live in. But the opposite side of that coin is who is going to author the incredibly arcane specification of TCP against which any such implementation is formally verified? Maybe TCP stacks are one of the few cases where that make sense, but I'd suspect if it was "worth the cost" it would have already been done

layer8 4y ago
There are certain guarantees you want such a formal specification to give, like for example not getting permanently stuck in some state as with the present bug. You can formalize the proofs for those guarantees and have their correctness machine-checked. Something like TLA+/PlusCal is likely suitable for that. A formal specification is less ambiguous than a prose specification. Formalizing the TCP specification will, if anything, expose aspects where the specification is unclear, or corner cases where the specification actually leads to unwanted behavior and doesn’t provide the desired guarantees. So, while you can’t prove that the formal specification matches the prose specification a 100%, you can prove that it provides all the guarantees the original prose specification was aiming for (once you’ve formalized those desired guarantees), which is something you can’t do for the prose specification.
specialist 4y ago
It seems to me that we should design for (formal) verification. Much like we should design for testability. But am noob, so what do I know? That said, my quick search shows some academic efforts to formally verify QUIC, both in whole and in parts. I would hope that bespoke (boutique?) TCP replacements, like Homa (specifically for datacenters), are verified as part of the design process. From a quick scan, I gleaned that Homa, and other aspirants, are simulated, compared, and benchmarked against each other. Maybe that's sufficient. https://homa-transport.atlassian.net/wiki/spaces/HOMA/overview?homepageId=229463 https://homa-transport.atlassian.net/wiki/spaces/HOMA/overvi...

layer8 4y ago

There are certain guarantees you want such a formal specification to give, like for example not getting permanently stuck in some state as with the present bug. You can formalize the proofs for those guarantees and have their correctness machine-checked. Something like TLA+/PlusCal is likely suitable for that. A formal specification is less ambiguous than a prose specification. Formalizing the TCP specification will, if anything, expose aspects where the specification is unclear, or corner cases where the specification actually leads to unwanted behavior and doesn’t provide the desired guarantees. So, while you can’t prove that the formal specification matches the prose specification a 100%, you can prove that it provides all the guarantees the original prose specification was aiming for (once you’ve formalized those desired guarantees), which is something you can’t do for the prose specification.

specialist 4y ago

It seems to me that we should design for (formal) verification. Much like we should design for testability. But am noob, so what do I know? That said, my quick search shows some academic efforts to formally verify QUIC, both in whole and in parts. I would hope that bespoke (boutique?) TCP replacements, like Homa (specifically for datacenters), are verified as part of the design process. From a quick scan, I gleaned that Homa, and other aspirants, are simulated, compared, and benchmarked against each other. Maybe that's sufficient. https://homa-transport.atlassian.net/wiki/spaces/HOMA/overview?homepageId=229463 https://homa-transport.atlassian.net/wiki/spaces/HOMA/overvi...