Conversation

Notices

1. Embed this notice
   Damien Miller (djm@cybervillains.com)'s status on Friday, 22-Dec-2023 03:06:25 JST Damien Miller

   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

   • clacke repeated this.
   • Embed this notice
     Kensan (kensan@mastodon.social)'s status on Friday, 22-Dec-2023 03:06:20 JST Kensan

     in reply to

     • hannes
     • Alexander Senier

     @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.

     https://codelabs.ch/tkm/

     @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.

     clacke likes this.
   • Embed this notice
     hannes (hannesm@mastodon.social)'s status on Friday, 22-Dec-2023 03:06:24 JST hannes

     in reply to

     @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

     clacke likes this.
   • Embed this notice
     Kensan (kensan@mastodon.social)'s status on Friday, 22-Dec-2023 03:06:45 JST Kensan

     in reply to

     • hannes
     • Alexander Senier

     @hannesm @djm @senier

     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

     clacke likes this.
   • Embed this notice
     Howard Chu @ Symas (hyc@mastodon.social)'s status on Friday, 22-Dec-2023 18:08:03 JST Howard Chu @ Symas

     in reply to

     • Lars Wirzenius

     @liw @djm and we're trending back toward closed gardens now. As usual, the present generation doesn't learn why things were done the way they were.

     clacke likes this.
   • Embed this notice
     Lars Wirzenius (liw@toot.liw.fi)'s status on Friday, 22-Dec-2023 18:08:04 JST Lars Wirzenius

     in reply to

     @djm While I agree that the Postel / RFC robustness principle, especially as widely understood today, is largely the wrong thing to do in protocols in 2023, things were different in the early Internet and early web. Then the problem was not "how do I do this networking thing really well", but "how do I and others do this at all so that it gets wide use?". The principle mattered more back then. Without it, we might not have the Internet at all today. We might only have closed gardens.