Proofs of correctness of the TLS Handshake and corking state machine

[achudnov]

This pull request contains:

• Proofs of correctness for the s2n handshake state machine with respect to the TLS 1.2 handshake model and IETF RFCs 5246, 5077 and 6066.
• Proof of correctness for TCP socket corking. Proof that the socket will not be corked or uncorked twice in server mode.
• Makefile and Travis CI integration for these new proofs
• Cryptographic proof (as seen in this paper) of s2n HMAC

A few key files:

• handshake.saw and cork-uncork.saw: Entry points for saw proofs. Run with saw handshake.saw or saw cork-uncork.saw
• s2n_handshake_io.saw : Proof script relating the LLVM code of s2n_handshake_io.c to our low-level Cryptol specifications in s2n_handshake_io.cry
• spec/rfc-handshake.cry: High level specification of the TLS 1.2 handshake, developed from relevant RFCs. This file also contains a Cryptol property relating the high-level handshake model to the low level one
• spec/cork-uncork.cry: A high-level model of s2n socket corking, and the property that corks and uncorks don't happen twice.
• Makefile and Travis integration: Integration runs all SAW proofs that are directly about the C code, as well as "negative test cases" that that introduce meaningful errors into the code ensure the proofs fail on them.
• Coq proofs of equivalence to FCF HMAC: Proofs of equivalence between the Cryptol specification of HMAC (previously proved equivalent to the C code) and the HMAC used for FCF proofs of correctness for HMAC. Together with the existing SAW proofs this establishes computational security of s2n's HMAC implementation.

CC: @colmmacc, @smagill, @atomb, @jldodds .

[achudnov]

So, the change I proposed works. Here's the diff. I'll add it to the pull request if you agree.

diff --git a/tests/saw/spec/rfc-handshake.cry b/tests/saw/spec/rfc-handshake.cry
index f53bb68..a9dbfce 100644
--- a/tests/saw/spec/rfc-handshake.cry
+++ b/tests/saw/spec/rfc-handshake.cry
@@ -118,24 +118,18 @@ type Parameters = {keyExchange : KeyExchange
 connectionParameters : connection -> Parameters -> Bit
 connectionParameters conn params =
     conn.server_can_send_ocsp == params.sendCertificateStatus
- /\ ((conn.key_exchange_eph /\ keyExchangeEphemeral params) \/
+ /\ ((conn.key_exchange_eph /\ ~keyExchangeNonEphemeral params /\ params.keyExchange != DH_anon) \/
      (~conn.key_exchange_eph /\ keyExchangeNonEphemeral params))
  /\ (conn.is_caching_enabled /\ ~conn.resume_from_cache) == params.sessionTicket
  /\ (~params.includeSessionTicket) // s2n server does not issue tickets at this time
  /\ (~params.renewSessionTicket) // s2n server does not issue tickets at this time
  /\ conn.client_auth_flag == params.requestClientCert
 
-// A predicate that tells whether key-exchange is non-ephemeral (doesn't use
-// Diffie-Hellman key exchange). In this case the key exchange algorithm does not
-// require KeyExchange messages.
+// A predicate that tells whether key-exchange is non-ephemeral and uses server certificate
+// data for exchanging a premaster secret (RFC 5246 7.4.3). In this case the key exchange
+// algorithm does not require KeyExchange messages.
 keyExchangeNonEphemeral : Parameters -> Bit
-keyExchangeNonEphemeral params = params.keyExchange == RSA \/ params.keyExchange == DH_DSS \/ params.keyExchange == DH_RSA // 
-
-// A predicate that tells whether key-exchange is ephemeral (uses Diffie-Hellman
-// key exchange). In this case the key exchange algorithm does not require
-// KeyExchange messages.
-keyExchangeEphemeral : Parameters -> Bit
-keyExchangeEphemeral params =  params.keyExchange == DHE_DSS \/ params.keyExchange == DHE_RSA
+keyExchangeNonEphemeral params = params.keyExchange == RSA \/ params.keyExchange == DH_DSS \/ params.keyExchange == DH_RSA
 
 // Handshake state transition relation per the RFCs. Given handshake parameters
 // and a handshake state, return the next state. If there is no valid next state,

[achudnov]

So, the change I proposed works. Here's the diff. I'll add it to the pull request if you agree.

diff --git a/tests/saw/spec/rfc-handshake.cry b/tests/saw/spec/rfc-handshake.cry
index f53bb68..a9dbfce 100644
--- a/tests/saw/spec/rfc-handshake.cry
+++ b/tests/saw/spec/rfc-handshake.cry
@@ -118,24 +118,18 @@ type Parameters = {keyExchange : KeyExchange
 connectionParameters : connection -> Parameters -> Bit
 connectionParameters conn params =
     conn.server_can_send_ocsp == params.sendCertificateStatus
- /\ ((conn.key_exchange_eph /\ keyExchangeEphemeral params) \/
+ /\ ((conn.key_exchange_eph /\ ~keyExchangeNonEphemeral params /\ params.keyExchange != DH_anon) \/
      (~conn.key_exchange_eph /\ keyExchangeNonEphemeral params))
  /\ (conn.is_caching_enabled /\ ~conn.resume_from_cache) == params.sessionTicket
  /\ (~params.includeSessionTicket) // s2n server does not issue tickets at this time
  /\ (~params.renewSessionTicket) // s2n server does not issue tickets at this time
  /\ conn.client_auth_flag == params.requestClientCert
 
-// A predicate that tells whether key-exchange is non-ephemeral (doesn't use
-// Diffie-Hellman key exchange). In this case the key exchange algorithm does not
-// require KeyExchange messages.
+// A predicate that tells whether key-exchange is non-ephemeral and uses server certificate
+// data for exchanging a premaster secret (RFC 5246 7.4.3). In this case the key exchange
+// algorithm does not require KeyExchange messages.
 keyExchangeNonEphemeral : Parameters -> Bit
-keyExchangeNonEphemeral params = params.keyExchange == RSA \/ params.keyExchange == DH_DSS \/ params.keyExchange == DH_RSA // 
-
-// A predicate that tells whether key-exchange is ephemeral (uses Diffie-Hellman
-// key exchange). In this case the key exchange algorithm does not require
-// KeyExchange messages.
-keyExchangeEphemeral : Parameters -> Bit
-keyExchangeEphemeral params =  params.keyExchange == DHE_DSS \/ params.keyExchange == DHE_RSA
+keyExchangeNonEphemeral params = params.keyExchange == RSA \/ params.keyExchange == DH_DSS \/ params.keyExchange == DH_RSA
 
 // Handshake state transition relation per the RFCs. Given handshake parameters
 // and a handshake state, return the next state. If there is no valid next state,

[achudnov]

@alexw91, have you had a chance to look at the changes I proposed and whether they address your concerns? Have you had any more thoughts about the pull request?

[achudnov]

@alexw91, have you had a chance to look at the changes I proposed and whether they address your concerns? Have you had any more thoughts about the pull request?

[alexw91]

Yes, it looks good to me. Thanks! :)

[alexw91]

Yes, it looks good to me. Thanks! :)

[achudnov]

The changes in 7b9c88d broke the proofs about handshake. We're investigating what could be done about it.

[achudnov]

The changes in 7b9c88d broke the proofs about handshake. We're investigating what could be done about it.

[jldodds]

We have fully updated the proofs for the TLS modifications. I also did a somewhat involved travis.yml merge, which probably needs examination before this PR is accepted

[jldodds]

We have fully updated the proofs for the TLS modifications. I also did a somewhat involved travis.yml merge, which probably needs examination before this PR is accepted

[achudnov]

Thanks, @jldodds! @alexw91, the tests now pass against the proposed merge into current master. Would you, please, review the PR once more and merge, if you are satisfied? We had to amend the code-related specifications, but it looks like the proof and the high-level specs are still the same.

[achudnov]

Thanks, @jldodds! @alexw91, the tests now pass against the proposed merge into current master. Would you, please, review the PR once more and merge, if you are satisfied? We had to amend the code-related specifications, but it looks like the proof and the high-level specs are still the same.

[alexw91]

We may need to get approval to ensure we're following https://github.com/PrincetonUniversity/VST/blob/master/LICENSE

[jldodds]

I've added the license file to this directory. The Princeton authors are also aware of this inclusion and approve of it, happy to get written approval if necessary.

[alexw91]

Please confirm this contribution is under the terms of the BSD 2 clause license. Thanks. :)

[jldodds]

Confirmed. I've also updated the licence to contain the appropriate author notice.

[jldodds]

From what I can tell, the Travis errors are some external dependency timing out. It is likely these will cause problems the next time any build is run, so it might be worth looking into now.

[jldodds]

From what I can tell, the Travis errors are some external dependency timing out. It is likely these will cause problems the next time any build is run, so it might be worth looking into now.

[alexw91]

Yeah, it looks like the ct-verif build is failing here: https://github.com/awslabs/s2n/blob/master/.travis/install_ctverif_dependencies.sh#L29-L30 since http://llvm-apt.ecranbleu.org/apt/trusty/ seems to be down.

[alexw91]

Yeah, it looks like the ct-verif build is failing here: https://github.com/awslabs/s2n/blob/master/.travis/install_ctverif_dependencies.sh#L29-L30 since http://llvm-apt.ecranbleu.org/apt/trusty/ seems to be down.

[alexw91]

Build Passes. Merging. :)

[alexw91]

Build Passes. Merging. :)