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

From: Antoine Delignat-Lavaud <[email-masked]>
Date: Mon, 04 Nov 2019 08:46:30 -0800

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

---

From: Antoine Delignat-Lavaud <[email-masked]>
Date: Mon, 04 Nov 2019 08:54:58 -0800

Actually, there is another mistake in the underflow case, the condition `candidate_pn > expected_pn + pn_hwin and candidate_pn > pn_win` should be `candidate_pn > expected_pn + pn_hwin and candidate_pn >= pn_win`, as we may want to decode an underflow to 0. 

-- 
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#issuecomment-549446610

---

From: Martin Thomson <[email-masked]>
Date: Mon, 04 Nov 2019 15:53:55 -0800

Thanks for finding these.  I'm not concerned about overflow on the upper end (you get other problems at that point), but it's worth getting right.

-- 
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#issuecomment-549600368

---

From: Martin Thomson <[email-masked]>
Date: Tue, 05 Nov 2019 15:57:09 -0800

Fixed in #3188.

-- 
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#issuecomment-550077842

---

From: Martin Thomson <[email-masked]>
Date: Tue, 05 Nov 2019 15:57:10 -0800

Closed #3187.

-- 
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#event-2773443659