The "robustness principle" is the most destructive concept in protocol design and implementation of all time. We should be embracing its inverse: strict, explicit state-machines with model-checked proofs
@djm agreed & there's https://datatracker.ietf.org/doc/html/rfc9413 :)
looking back, unfortunately formal methods work does not always pick up to ietf - e.g. our work on tcp/ip and the sockets api didn't get much resonance in the engineering community http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf
@hannesm @djm We did something like this for IKEv2 with TKM, which is part of strongSwan. (Library) Code generator which includes FSM and SPARK proof aspects for state transitions.
@senier et al (now at AdaCore) has done a project called RecordFlux, which does much more: you can specify the protocol in a DSL and the tools will generate SPARK code with some formal guarantees. NVIDIA has actually used it in production.
Also, the code is opensource and up on GitHub.
RecordFlux paper:
https://arxiv.org/abs/1910.02146
NVIDIA paper:
https://www.adacore.com/uploads/techPapers/232867-adacore-record-flux-tech-paper-v10.pdf
Source Code:
https://github.com/AdaCore/RecordFlux
@thodg which network protocols did you do in OCaml? open source? :)
@hannesm no, very simple protocols, nothing fancy but it worked without a flaw everytime for a long time