On Mon, Apr 19, 2021 at 10:59 PM Brian E Carpenter <brian.e.carpenter@xxxxxxxxx> wrote:
On 20-Apr-21 10:22, Keith Moore wrote:
> Could we make greater use of protocol specification
> languages to reduce the difference between specification and running code?
In theory we could, but it's far from easy. Take CBOR-based protocols for
a start. Yes, you can use CDDL for a formal specification of the message
formats, and you can in theory verify that the messages conform; you could
presumably write a CDDL-driven message parser. But none of that models
the protocol's state machine. That would be a whole new level of formalism.
People are trying, however: https://doi.org/10.1145/3341302.3342087
I use formal-ized tools for much of my work. But I haven't written a proof since I finished my doctorate. The problem I found is the aspects of the system that can be reasoned about tend to not be the parts that are important for reliability of the system. I prefer to spend the time simplifying the system and removing what is unnecessary than limiting myself to what can be proved.
There turns out to be a particular hazard with proofs of crypto protocols as protocols with a proof of correctness tend to be brittle as the constraints of proof hacking prevent the defense in depth type approaches needed today.
I almost always write a tool to parse and serialize even apparently simple messages because experience tells me that is necessary. I don't find the same is true for protocol state machines even though I have dozens of domain specific languages for state machines as well.
This morning, I modelled the state machine of RUD using CSP. But it doesn't really help very much because the important issues are packets being lost, packets arriving out of order and timing. Sure, there are timed versions of CSP but how do I get from CSP to the Tasks model of C# or anything in Java-land?
