GNU social JP
  • FAQ
  • Login
GNU social JPは日本のGNU socialサーバーです。
Usage/ToS/admin/test/Pleroma FE
  • Public

    • Public
    • Network
    • Groups
    • Featured
    • Popular
    • People

Conversation

Notices

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

    In conversation Friday, 22-Dec-2023 03:06:25 JST from cybervillains.com permalink
    • clacke repeated this.
    • Embed this notice
      Kensan (kensan@mastodon.social)'s status on Friday, 22-Dec-2023 03:06:20 JST Kensan 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.

      In conversation Friday, 22-Dec-2023 03:06:20 JST permalink
      clacke likes this.
    • Embed this notice
      hannes (hannesm@mastodon.social)'s status on Friday, 22-Dec-2023 03:06:24 JST hannes 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

      In conversation Friday, 22-Dec-2023 03:06:24 JST permalink

      Attachments

      1. Domain not in remote thumbnail source whitelist: www.ietf.org
        RFC 9413: Maintaining Robust Protocols
        from David Schinazi
        The main goal of the networking standards process is to enable the long-term interoperability of protocols. This document describes active protocol maintenance, a means to accomplish that goal. By evolving specifications and implementations, it is possible to reduce ambiguity over time and create a healthy ecosystem. The robustness principle, often phrased as "be conservative in what you send, and liberal in what you accept", has long guided the design and implementation of Internet protocols. However, it has been interpreted in a variety of ways. While some interpretations help ensure the health of the Internet, others can negatively affect interoperability over time. When a protocol is actively maintained, protocol designers and implementers can avoid these pitfalls.

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

      In conversation Friday, 22-Dec-2023 03:06:45 JST permalink

      Attachments



      1. Domain not in remote thumbnail source whitelist: opengraph.githubassets.com
        GitHub - AdaCore/RecordFlux: Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
        Formal specification and generation of verifiable binary parsers, message generators and protocol state machines - GitHub - AdaCore/RecordFlux: Formal specification and generation of verifiable bin...
      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 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.

      In conversation Friday, 22-Dec-2023 18:08:03 JST permalink
      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 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.

      In conversation Friday, 22-Dec-2023 18:08:04 JST permalink

Feeds

  • Activity Streams
  • RSS 2.0
  • Atom
  • Help
  • About
  • FAQ
  • TOS
  • Privacy
  • Source
  • Version
  • Contact

GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.

Creative Commons Attribution 3.0 All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.