Re: adapting IETF in light of github and similar tools

Phillip Hallam-Baker <phill@hallambaker.com> Tue, 20 April 2021 05:26 UTC

Return-Path: <hallam@gmail.com>
X-Original-To: ietf@ietfa.amsl.com
Delivered-To: ietf@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 920FB3A0DD5 for <ietf@ietfa.amsl.com>; Mon, 19 Apr 2021 22:26:00 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -1.4
X-Spam-Level:
X-Spam-Status: No, score=-1.4 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, FREEMAIL_FORGED_FROMDOMAIN=0.249, FREEMAIL_FROM=0.001, HEADER_FROM_DIFFERENT_DOMAINS=0.249, HTML_MESSAGE=0.001, RCVD_IN_MSPIKE_H2=-0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, URIBL_BLOCKED=0.001] autolearn=no autolearn_force=no
Received: from mail.ietf.org ([4.31.198.44]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id uBcWBPGkXIzN for <ietf@ietfa.amsl.com>; Mon, 19 Apr 2021 22:25:56 -0700 (PDT)
Received: from mail-yb1-f179.google.com (mail-yb1-f179.google.com [209.85.219.179]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 17B963A0DD2 for <ietf@ietf.org>; Mon, 19 Apr 2021 22:25:55 -0700 (PDT)
Received: by mail-yb1-f179.google.com with SMTP id g38so41554476ybi.12 for <ietf@ietf.org>; Mon, 19 Apr 2021 22:25:55 -0700 (PDT)
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=472GI1BlcaWftmO6fjaA8KrVv1A+nCMbIru7+1uQVcU=; b=dNH5gkz21VsgVtqBDFk+ryIf1r1NUXWWtBmnDQpxYfRJWHnmOqJEA3RxYC0hO4lHvp GoS0kHxB1PJ4R/d/rL2oE105DX8ShY2EV8I5/fgowHTBEJQl17o+E0pt+6FUjCVXWxGU Roh8D45hfJ0rgm4aGRyBKDp6PpgTSH3QDXcx+G3Hvd7zKrfUDl47OuBhmQ4z1HPCD038 AwfHe1AcclHwmgasah1qky2VXMlRcWlXI3ym3nUx734FBvJQJM/tlvfjoKO5G0Y8YGzv IKFH+xNhyFtVA8dKK+mVRW7vA7nNMVxqya3GWeiAqLRaM2iRGMdXaG4U0YmEVhGSI9vr Dbow==
X-Gm-Message-State: AOAM533smkQCwhlFIEPCQQVFyJQZqi39xd3MB3W7uE8W53FMGGFTzWNL kUx0PIm9rhAL2GAa89z/VSpbsb3StKh1YTtBrf4=
X-Google-Smtp-Source: ABdhPJyBFdhGa01hfEary1QS0xsMIWnf1IcKNbJBGgnT2vIoaDm2E3e2Dylo9OfB09iE1QmsBietOrqlhWgBiDnz2FM=
X-Received: by 2002:a5b:585:: with SMTP id l5mr20959524ybp.213.1618896354462; Mon, 19 Apr 2021 22:25:54 -0700 (PDT)
MIME-Version: 1.0
References: <0b63d094-8c95-409f-282e-86231128f7b5@network-heretics.com> <1C5B7B67-27E5-41F5-89D4-765A407C1FC6@mnt.se> <EE6AD028-C5E9-4FA9-9756-0ACB32E298F9@shockey.us> <10029019-302a-dbf0-6a8e-eb0d26cd027a@network-heretics.com> <ddd6a7af-0f94-6250-c5d6-4348ddc8d059@gmail.com>
In-Reply-To: <ddd6a7af-0f94-6250-c5d6-4348ddc8d059@gmail.com>
From: Phillip Hallam-Baker <phill@hallambaker.com>
Date: Tue, 20 Apr 2021 01:25:42 -0400
Message-ID: <CAMm+LwgyMU0+fyP2_6UpQWurU3NhEDkcpUv48Vyv3b7OJnWtbA@mail.gmail.com>
Subject: Re: adapting IETF in light of github and similar tools
To: Brian E Carpenter <brian.e.carpenter@gmail.com>
Cc: Keith Moore <moore@network-heretics.com>, Richard Shockey <richard@shockey.us>, Leif Johansson <leifj@mnt.se>, IETF Discussion Mailing List <ietf@ietf.org>
Content-Type: multipart/alternative; boundary="00000000000022cdbb05c060aef9"
Archived-At: <https://mailarchive.ietf.org/arch/msg/ietf/LyJ6erS04JOSjuB-ausVb8mQOa4>
X-BeenThere: ietf@ietf.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: IETF-Discussion <ietf.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/ietf>, <mailto:ietf-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/ietf/>
List-Post: <mailto:ietf@ietf.org>
List-Help: <mailto:ietf-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/ietf>, <mailto:ietf-request@ietf.org?subject=subscribe>
X-List-Received-Date: Tue, 20 Apr 2021 05:26:01 -0000

On Mon, Apr 19, 2021 at 10:59 PM Brian E Carpenter <
brian.e.carpenter@gmail.com> 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?