[Lake] Fwd: [irtf-discuss] Usable formal methods side meeting at IETF 115

Colin Perkins <csp@csperkins.org> Fri, 04 November 2022 16:56 UTC

Return-Path: <csp@csperkins.org>
X-Original-To: lake@ietfa.amsl.com
Delivered-To: lake@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 8BD1DC1522A0; Fri, 4 Nov 2022 09:56:46 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -7.105
X-Spam-Level:
X-Spam-Status: No, score=-7.105 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_HI=-5, RCVD_IN_ZEN_BLOCKED_OPENDNS=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01, URIBL_BLOCKED=0.001, URIBL_DBL_BLOCKED_OPENDNS=0.001, URIBL_ZEN_BLOCKED_OPENDNS=0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=csperkins.org
Received: from mail.ietf.org ([50.223.129.194]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id WCzvOaBPXMHX; Fri, 4 Nov 2022 09:56:41 -0700 (PDT)
Received: from mx2.mythic-beasts.com (mx2.mythic-beasts.com [IPv6:2a00:1098:0:82:1000:0:2:1]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange ECDHE (P-256) server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 8874CC14CE32; Fri, 4 Nov 2022 09:56:41 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=csperkins.org; s=mythic-beasts-k1; h=Date:Subject:To:From; bh=jqs0S4jqMXhD87b1Cn14E4lVJfJHvEnYPr1k2phNbt8=; b=1MwcFT+E+hC5rPmgab/ICX3Nb/ +B1xZ3ng/tLl56baEW9z7qLgpsMXIiTxlIcIpagfqbkxUrHs2qCG4sch7oOq5Ntw41WA3X/u27/5W X2S/0Yr8FrGIokyenuBvj7W6x1c0HTCZtlpA6Q7GuBCtn9izWwSz487rbf956idCnQfBhHNTe5fvU sPBKtdP9l8bfHJKhQvNaKWgWnPj31EiOmqqWdqtbGKekxwstnv2sRrKActTt3v8TNVJpxL1f7CynB 9jbFNI2063kIEGhizTdCT4dh4X1WCQdiXJTWetXvxDXiCmlXNhoAceN/zxgyz0ynEAc7O+C5+c7eT /ZdifLFQ==;
Received: from [81.187.2.149] (port=45382 helo=[192.168.56.1]) by mailhub-hex-d.mythic-beasts.com with esmtpsa (TLS1.2) tls TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 (Exim 4.94.2) (envelope-from <csp@csperkins.org>) id 1oqzzj-0003uP-9u; Fri, 04 Nov 2022 16:56:39 +0000
From: Colin Perkins <csp@csperkins.org>
To: lake@ietf.org, tls@ietf.org
Date: Fri, 04 Nov 2022 16:56:35 +0000
Reply-To: irtf-discuss@irtf.org
X-Mailer: MailMate (1.14r5926)
Message-ID: <1E66C3F8-63BA-47AC-AC40-E2AE6ED28660@csperkins.org>
References: <C91D3863-37D3-4E09-B1F9-588C316240CD@csperkins.org>
MIME-Version: 1.0
Content-Type: multipart/alternative; boundary="=_MailMate_CA7A411F-9125-41BE-AD2B-74383367B2F2_="
X-BlackCat-Spam-Score: 0
Archived-At: <https://mailarchive.ietf.org/arch/msg/lake/SoopQxThggHqOJ6chbSPW00QnNY>
Subject: [Lake] Fwd: [irtf-discuss] Usable formal methods side meeting at IETF 115
X-BeenThere: lake@ietf.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: Lightweight Authenticated Key Exchange <lake.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/lake>, <mailto:lake-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/lake/>
List-Post: <mailto:lake@ietf.org>
List-Help: <mailto:lake-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/lake>, <mailto:lake-request@ietf.org?subject=subscribe>
X-List-Received-Date: Fri, 04 Nov 2022 16:56:46 -0000

There’s a side meeting on usable formal methods for protocol 
specification taking place during IETF next week that may be of interest 
to some in this group – please consider attending.

Colin



Forwarded message:

> From: Colin Perkins <csp@csperkins.org>
> To: irtf-discuss@irtf.org
> Cc: 115attendees@ietf.org
> Subject: [irtf-discuss] Usable formal methods side meeting at IETF 115
> Date: Fri, 04 Nov 2022 16:42:21 +0000
>
> Hi,
>
> How should we describe and specify protocols?
>
> How can we ensure that network protocol specifications are consistent 
> and correct, and verify that implementations match the specification?
>
> The IETF community has long used natural language, English, to 
> describe and specify its protocols, with occasional use of formal 
> languages and a some limited amounts of formal verification. One of 
> the sessions in the Applied Networking Research Workshop at IETF 114 
> [1] started to discuss whether this is the right approach, and to what 
> extent formal methods, structured specification languages, and natural 
> language processing techniques can help describe network protocols.
>
> Chris Wood and I are organising a side meeting at IETF 115 to continue 
> this discussion, and to assess interest in forming a new IRTF research 
> group to explore usable formal methods for protocol specification.
>
> This will takes place on Thursday lunchtime, 10 November, from 
> 11:30-13:00 UK time in room Richmond 5 of the IETF meeting hotel (the 
> IAB breakout room).
>
> The draft agenda is as follows:
>
>   - Welcome, Goals, Motivation, Introductions
>       - (15 mins)
>   - Short presentations (45 mins)
>       - “What are Formal Methods and Why Should We Care?”Jonathan 
> Hoyland
>       - “Formal Specification and Specification-Based Testing of 
> QUIC”, Ken McMillan
>   - Discussion of proposed charter (20 mins)
>       - See [Google 
> Doc](https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#)
>   - Next steps (10 mins)
>       - Does this seem appropriate for an RG?
>       - Are there volunteers to work on this topic?
>       - What, if anything, have we missed?
>
> if you’re interested in this topic, please review [the draft 
> charter](https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#) 
> and come along to the side meeting to give your feedback.
>
> Hope to see you in London!
>
> Colin
>
>
>
> [1] https://www.youtube.com/watch?v=tCsiB87s-f4
>
> -- 
> Colin Perkins
> https://csperkins.org/