Subject: [quicwg/base-drafts] Formal analysis of the protocol (#1874)

From: Demi Marie Obenour <[email-masked]>
Date: Wed, 17 Oct 2018 15:06:16 -0700

It would be nice to have a formal proof that QUIC meets its security goals, and is free from deadlocks, denial of service vulnerabilities, and other bad behavior.

-- 
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/1874

---

From: Mike Bishop <[email-masked]>
Date: Wed, 17 Oct 2018 16:47:19 -0700

It would be.  TLS has had such formal proofs, but there are potentially parts of the QUIC protocol that could be modeled as well.

That said, there are known deadlock situations, so I suspect such a proof would not be possible.  I'll leave to others to suggest where/whether such verification might be useful.

-- 
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/1874#issuecomment-430827627

---

From: ianswett <[email-masked]>
Date: Wed, 17 Oct 2018 18:53:40 -0700

My understanding is that we have text that prevents all known deadlocks.  Are there deadlocks you're aware of that are not preventable, particularly at the transport layer?  At the application layer, certainly one can create an application that causes a deadlock.

-- 
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/1874#issuecomment-430847929

---

From: Mike Bishop <[email-masked]>
Date: Thu, 18 Oct 2018 16:17:14 +0000 (UTC)

No, the known deadlocks are flow control footguns, which require application misuse.

-- 
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/1874#issuecomment-431071529