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

[Antoine Delignat-Lavaud <[e-mail]>]

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