[quicwg/base-drafts] Overflow in appendix A packet number decoding sample (#3187)

Antoine Delignat-Lavaud <notifications@github.com> Mon, 04 November 2019 16:46 UTC

Return-Path: <noreply@github.com>
X-Original-To: quic-issues@ietfa.amsl.com
Delivered-To: quic-issues@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 00CEC120B19 for <quic-issues@ietfa.amsl.com>; Mon, 4 Nov 2019 08:46:35 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -8
X-Spam-Level:
X-Spam-Status: No, score=-8 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIMWL_WL_HIGH=-0.001, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, HTML_MESSAGE=0.001, MAILING_LIST_MULTI=-1, RCVD_IN_DNSWL_HI=-5, SPF_HELO_NONE=0.001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (1024-bit key) header.d=github.com
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 MVKUgsuI6GB7 for <quic-issues@ietfa.amsl.com>; Mon, 4 Nov 2019 08:46:31 -0800 (PST)
Received: from out-3.smtp.github.com (out-3.smtp.github.com [192.30.252.194]) (using TLSv1.2 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 90B21120806 for <quic-issues@ietf.org>; Mon, 4 Nov 2019 08:46:31 -0800 (PST)
Received: from github-lowworker-5fb2734.va3-iad.github.net (github-lowworker-5fb2734.va3-iad.github.net [10.48.19.27]) by smtp.github.com (Postfix) with ESMTP id BF4242C346D for <quic-issues@ietf.org>; Mon, 4 Nov 2019 08:46:30 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=github.com; s=pf2014; t=1572885990; bh=ZbTgAvzvTQ/5bvAJDx0d1YRkbXV/2IHWnPKAirGDuIw=; h=Date:From:Reply-To:To:Cc:Subject:List-ID:List-Archive:List-Post: List-Unsubscribe:From; b=zCFiBJoVQjOY0nPpwL6yXSs6ARTycXUixIoamEl296YXgT64/umBwEHzN9BpErxou glI8wQfc4yrYGaVdQqVuEBW0oKyenytm4jGiXS16LQAdjoADSHrXNd/ijBMjq7+hel E48kuHOhsDGKjhwJGhQBT35mivZLb2kTdCZa743k=
Date: Mon, 04 Nov 2019 08:46:30 -0800
From: Antoine Delignat-Lavaud <notifications@github.com>
Reply-To: quicwg/base-drafts <reply+AFTOJK6KQPUZVWKBDEGA65F3ZWEGNEVBNHHB5VH2I4@reply.github.com>
To: quicwg/base-drafts <base-drafts@noreply.github.com>
Cc: Subscribed <subscribed@noreply.github.com>
Message-ID: <quicwg/base-drafts/issues/3187@github.com>
Subject: [quicwg/base-drafts] Overflow in appendix A packet number decoding sample (#3187)
Mime-Version: 1.0
Content-Type: multipart/alternative; boundary="--==_mimepart_5dc055e6b0805_2fb93f8e500cd9607441c"; charset=UTF-8
Content-Transfer-Encoding: 7bit
Precedence: list
X-GitHub-Sender: ad-l
X-GitHub-Recipient: quic-issues
X-GitHub-Reason: subscribed
X-Auto-Response-Suppress: All
X-GitHub-Recipient-Address: quic-issues@ietf.org
Archived-At: <https://mailarchive.ietf.org/arch/msg/quic-issues/4uHdSRaiQ8BfOgIZoVkeiM_HWhs>
X-BeenThere: quic-issues@ietf.org
X-Mailman-Version: 2.1.29
List-Id: Notification list for GitHub issues related to the QUIC WG <quic-issues.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/quic-issues>, <mailto:quic-issues-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/quic-issues/>
List-Post: <mailto:quic-issues@ietf.org>
List-Help: <mailto:quic-issues-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/quic-issues>, <mailto:quic-issues-request@ietf.org?subject=subscribe>
X-List-Received-Date: Mon, 04 Nov 2019 16:46:38 -0000

While working on the proof of correctness of packet decoding, my intern discovered an error in the reference code of Appendix A. More precisely, we tried to prove the following lemma:

```fstar
let bound_npn (pn_len:nat2) = pow2 (8 * (pn_len+1))

let in_window (pn_len:nat2) (last pn:nat) =
  let h = bound_npn pn_len in
  (last+1 < h/2 /\ pn < h) \/
  (last+1 >= pow2 62 - h/2 /\ pn >= pow2 62 - h) \/
  (last+1 - h/2 < pn /\ pn <= last+1 + h/2)

val reduce_pn:
  pn_len:nat2 ->
  pn:nat62 ->
  npn:nat{npn < bound_npn pn_len}

val expand_pn :
  pn_len:nat2 ->
  last:nat{last+1 < pow2 62} ->
  npn:nat{npn < bound_npn pn_len} ->
  pn:nat62{in_window pn_len last pn /\ pn % bound_npn pn_len = npn}

val lemma_pn_correct : pn_len:nat2 -> last:nat{last+1 < pow2 62} -> pn:nat62 -> Lemma
  (requires in_window pn_len last pn)
  (ensures expand_pn pn_len last (reduce_pn pn_len pn) = pn)
```

However, the proof fails because in the first case `candidate_pn <= expected_pn - pn_hwin`, the returned value `candidate_pn + pn_win` can overflow:

```
      candidate_pn = (expected_pn & ~pn_mask) | truncated_pn
      if candidate_pn <= expected_pn - pn_hwin:
         return candidate_pn + pn_win
      // Note the extra check for underflow when candidate_pn
      // is near zero.
      if candidate_pn > expected_pn + pn_hwin and
         candidate_pn > pn_win:
         return candidate_pn - pn_win
      return candidate_pn
```
Instead, the first condition should be `if candidate_pn <= expected_pn - pn_hwin and candidate_pn + pn_win < 2^62`. Using this condition we are able to prove the lemma above (the proof is at https://github.com/project-everest/everquic-crypto/blob/master/src/QUIC.Spec.fst#L2685). It may also be a good idea to better document the `in_window` condition, as it can help with the choice of the pn_len parameter. 

-- 
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub:
https://github.com/quicwg/base-drafts/issues/3187