Re: [Ufmrg] Follow-up: HTTP/2 Rapid Reset & Formal Analysis

Liu Si <si.liu@inf.ethz.ch> Wed, 08 November 2023 14:33 UTC

Return-Path: <si.liu@inf.ethz.ch>
X-Original-To: ufmrg@ietfa.amsl.com
Delivered-To: ufmrg@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id AC9A0C17DBE6 for <ufmrg@ietfa.amsl.com>; Wed, 8 Nov 2023 06:33:12 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -4.306
X-Spam-Level:
X-Spam-Status: No, score=-4.306 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_MED=-2.3, 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=inf.ethz.ch
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 jEVgMk0vmMTh for <ufmrg@ietfa.amsl.com>; Wed, 8 Nov 2023 06:33:08 -0800 (PST)
Received: from mailg210.ethz.ch (mailg210.ethz.ch [IPv6:2001:67c:10ec:5606::21]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id E98ADC17DBF4 for <ufmrg@irtf.org>; Wed, 8 Nov 2023 06:33:06 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=inf.ethz.ch; s=key1-q2-2022; t=1699453978; h=From:Subject:Date:Message-ID:To :MIME-Version:Content-Type:In-Reply-To:References; bh=R7XvWVQvHIeOO8l4Ymj 6ZdWgzIMCHFUw8H1vo9o4M9E=; b=IEu1QcKVR7+qOxO35V1/G14iMC8VOle9FENHLxVLeTLO RjXbZyij1ZVp8Vjfbow5zZSDcbm0woAAYGZOveESAQeGUBJW26W0tHV+vya9OJGFpZiioYMP0 ZvHnZGabruLe1Rk7UuN4jZOqkdcVx4e28qv4RXh8nVP9M1NBPG38TKyltET4H3H5FJ68ZeCu5 lNvNqS0ObUqVFL/cmR00cMxW5u5XFdi9NtZLmus91BxZLGn1twLcYPSFOO6j7tmtwSfPg/wTZ lWt9uNdCSquHo1p/iZ1vE9z6vyBlCFmyuhlC4AJ0qszQV4QCQPSj90EbaFK8WLV3vfzhCIe7E D4xd2Q==;
Received: from mailm211.d.ethz.ch (2001:67c:10ec:5603::25) by mailg210.ethz.ch (2001:67c:10ec:5606::21) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.2507.34; Wed, 8 Nov 2023 15:32:58 +0100
Received: from mailm213.d.ethz.ch (2001:67c:10ec:5603::27) by mailm211.d.ethz.ch (2001:67c:10ec:5603::25) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.2507.34; Wed, 8 Nov 2023 15:33:03 +0100
Received: from mailm213.d.ethz.ch ([fe80::48e5:b9c:79eb:9d16]) by mailm213.d.ethz.ch ([fe80::48e5:b9c:79eb:9d16%4]) with mapi id 15.01.2507.034; Wed, 8 Nov 2023 15:33:03 +0100
From: Liu Si <si.liu@inf.ethz.ch>
To: UFMRG IRTF <ufmrg@irtf.org>
Thread-Topic: [Ufmrg] Follow-up: HTTP/2 Rapid Reset & Formal Analysis
Thread-Index: AQHaEkmSjRUYMVjkGUqngHVc7l3P27Bwa5IA
Date: Wed, 08 Nov 2023 14:33:02 +0000
Message-ID: <AD373208-B507-4E18-A7BA-E9A0A3AC1A1E@inf.ethz.ch>
References: <AM9PR02MB70277E088A746E8424A0BC74ABA8A@AM9PR02MB7027.eurprd02.prod.outlook.com>
In-Reply-To: <AM9PR02MB70277E088A746E8424A0BC74ABA8A@AM9PR02MB7027.eurprd02.prod.outlook.com>
Accept-Language: en-US, de-CH
Content-Language: en-US
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
x-originating-ip: [31.164.78.160]
Content-Type: multipart/alternative; boundary="_000_AD373208B5074E18A7BAE9A0A3AC1A1Einfethzch_"
MIME-Version: 1.0
X-DKIM-Signer: DkimX (v3.20.320)
Archived-At: <https://mailarchive.ietf.org/arch/msg/ufmrg/OZOz7NHl57FNxo3MnaYJY8PPwsw>
Subject: Re: [Ufmrg] Follow-up: HTTP/2 Rapid Reset & Formal Analysis
X-BeenThere: ufmrg@irtf.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: Usable Formal Methods Research Group <ufmrg.irtf.org>
List-Unsubscribe: <https://mailman.irtf.org/mailman/options/ufmrg>, <mailto:ufmrg-request@irtf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/ufmrg/>
List-Post: <mailto:ufmrg@irtf.org>
List-Help: <mailto:ufmrg-request@irtf.org?subject=help>
List-Subscribe: <https://mailman.irtf.org/mailman/listinfo/ufmrg>, <mailto:ufmrg-request@irtf.org?subject=subscribe>
X-List-Received-Date: Wed, 08 Nov 2023 14:33:12 -0000

Hi all,

I would also like to share some of our experience on “whether formal methods can help with DDoS attack vectors”. The short answer is yes.

We have recently developed a formal framework for end-to-end DNS resolution (https://doi.org/10.1145/3603269.3604870) in the Maude formal language. Major results from this project include:

1. Formalizing the semantics of DNS resolution. Along the way, we’ve identified ambiguities and underspecificaiton in the RFCs.
2. Discovering new DoS vulnerabilities in DNS including multiple attacks that can achieve large amplification effects.

I would be happy to share more if someone finds it interesting. I hope this helps anyway.

Cheers,
Si Liu
Senior Scientist at ETH Zurich (a group mate of Felix’s ;)


On 8 Nov 2023, at 14:43, Felix Linker <linkerfelix@gmail.com> wrote:

Hi all,

I wanted to follow-up on Lucas Pardue’s question whether formal methods can help with DDoS attack vectors. I knew that I had attended a talk that seemed related earlier this year but wasn’t quick enough in digging up the reference to step up to the microphone.

But better late than never! This paper seems related to Lucas’s presentation: https://www.usenix.org/conference/nsdi23/presentation/tahmasbi

Notably, the authors model buffers/queues. The link above also provides a presentation recording (15min) and the talk’s slides.

@Lucas: I remember being intrigued by this work, so happy to discuss this topic more should you have follow-up questions.

I hope this helps,
Felix
--
Ufmrg mailing list
Ufmrg@irtf.org<mailto:Ufmrg@irtf.org>
https://mailman.irtf.org/mailman/listinfo/ufmrg