[arch-d] Making Networks Safe and Agile with Formal Methods and Programming Abstractions: Future Directions

Hesham ElBakoury <helbakoury@gmail.com> Tue, 28 November 2023 19:26 UTC

Return-Path: <helbakoury@gmail.com>
X-Original-To: architecture-discuss@ietfa.amsl.com
Delivered-To: architecture-discuss@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 9BB1AC1519AE for <architecture-discuss@ietfa.amsl.com>; Tue, 28 Nov 2023 11:26:05 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -2.104
X-Spam-Level:
X-Spam-Status: No, score=-2.104 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, FREEMAIL_FROM=0.001, HTML_MESSAGE=0.001, PDS_OTHER_BAD_TLD=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_ZEN_BLOCKED_OPENDNS=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01, 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=gmail.com
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 OY2vUDhmiktd for <architecture-discuss@ietfa.amsl.com>; Tue, 28 Nov 2023 11:26:01 -0800 (PST)
Received: from mail-pj1-x1035.google.com (mail-pj1-x1035.google.com [IPv6:2607:f8b0:4864:20::1035]) (using TLSv1.3 with cipher TLS_AES_128_GCM_SHA256 (128/128 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id B3BE8C1519AA for <architecture-discuss@ietf.org>; Tue, 28 Nov 2023 11:26:01 -0800 (PST)
Received: by mail-pj1-x1035.google.com with SMTP id 98e67ed59e1d1-285b926e5deso2905144a91.0 for <architecture-discuss@ietf.org>; Tue, 28 Nov 2023 11:26:01 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1701199561; x=1701804361; darn=ietf.org; h=to:subject:message-id:date:from:mime-version:from:to:cc:subject :date:message-id:reply-to; bh=whVE5JSjwSRkKtEI1Zu58lcDWoniBVSJv+jntP/6gbQ=; b=A6pHsddIn46X5T5iHfsW+dh3zETBePTk0N8+g4RQPQsglPj873P0ZpqJ37BBNETx8r eKYRn42QI5+UW0CoyNhoMpP7y8+MTKakAGcfLQOQB2z10oLmqOpVYBZZZGSBqp9vT+F+ rB3TyXvYav6pvILYxIwHIUxpcaVerTB9xiky96mhePgovgVhws0+uc6A4X5/coiswVRr Uh1+votU9AmFXx5bMPudPxYc0vPO1ttVKDvpW+OhelR4w1uKErm4+9jNzqbbdD2/MQtD ZVJ3b7NZi6pWsuE7O/UukU6Z0zeEzYz8OljZ+mxNynaKxsVEN6Exq1hpeO51Z/g3nCIQ 11sg==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1701199561; x=1701804361; h=to:subject:message-id:date:from:mime-version:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=whVE5JSjwSRkKtEI1Zu58lcDWoniBVSJv+jntP/6gbQ=; b=vuRuiE1ilLqgFzWDZsfDvhEtsU70CufP13tbQW/PgW2W6kkkRMI64w2PZPqxxipNHs bgkP38/bkU5q0V9eSEYzAwD6bjuUif5+k0yj4+AXVskAPpmbIhxq83aMt+yTtYPhFpYn Bqw5ZxdMqFG+LIzGLZL9jclzHPYUxXSTqFPph6d9juiksQ0+oFQAeS5M7IzGu413BzUM lgBEy0+YudWrGcc4UhW1IKF6n8kGGpecpGRkSxeOf82Ce7SWOFDeCFaLcgYnJSPhM0Xq +xA84yS/O+xL53Jq3OBjfuOuHfF5qx5kWw+KRpGXs/Dvzj+lTmsNvGzz4O+QEy4YVGe0 R1yg==
X-Gm-Message-State: AOJu0YwYtRF9ulyr1oc4x8NFJIegSv38Yu8sdnDzPf79ciZJcI5SyKO9 AwwOMDrREtBfGN4VgCjG0+Z/XZ+1vY9B8uecmwswegmy
X-Google-Smtp-Source: AGHT+IGGtAntuDD+QSw7TKjiBWe7bGd9M8KaOoI/3mdLhikZAd7/TdDuOLXifKjCPrZLoMIw43tXqFTaZEZVYhIGiEQ=
X-Received: by 2002:a17:90b:17c8:b0:285:bc16:6135 with SMTP id me8-20020a17090b17c800b00285bc166135mr9955904pjb.30.1701199560632; Tue, 28 Nov 2023 11:26:00 -0800 (PST)
MIME-Version: 1.0
From: Hesham ElBakoury <helbakoury@gmail.com>
Date: Tue, 28 Nov 2023 11:25:48 -0800
Message-ID: <CAFvDQ9pADq19OB=0F=n8aJ-0NHRU_xDuxNeHkBJiJW63CdLs6A@mail.gmail.com>
To: architecture-discuss@ietf.org
Content-Type: multipart/alternative; boundary="00000000000080eea3060b3b6356"
Archived-At: <https://mailarchive.ietf.org/arch/msg/architecture-discuss/d053n1HPwb29ZPHZCmOYsIM_xy4>
Subject: [arch-d] Making Networks Safe and Agile with Formal Methods and Programming Abstractions: Future Directions
X-BeenThere: architecture-discuss@ietf.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: open discussion forum for long/wide-range architectural issues <architecture-discuss.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/architecture-discuss>, <mailto:architecture-discuss-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/architecture-discuss/>
List-Post: <mailto:architecture-discuss@ietf.org>
List-Help: <mailto:architecture-discuss-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/architecture-discuss>, <mailto:architecture-discuss-request@ietf.org?subject=subscribe>
X-List-Received-Date: Tue, 28 Nov 2023 19:26:05 -0000

The article below captures the  results of brainstorming discussions
on future directions in applying formal methods and programming languages
to networking. The discussion included Nate Foster, Arvind Krishnamurthy,
Todd Millstein, Dave Walker, Anduo Wang, Pamela Zave, and Ratul Mahajan.

https://netverify.fun/making-networks-safe-and-agile-with-formal-methods-and-programming-abstractions/

This article is a byproduct of discussions amongst the authors in the
context of NSF Community Workshop on Long-term Research Directions in Wired
Networking <https://wired23.github.io/>

The article highlights the compositional network architecture which is
promoted by Pamela Zave and Jennifer Rexford.

Hesham