Remove hard-coded assumptions about `use_tickets` and `client_session_resumed` in SAW proofs

[RyanGlScott]

Problem:

Currently, the SAW proofs assume that config->use_tickets is always disabled:

https://github.com/aws/s2n-tls/blob/2c27512895e8a2945f97b5137bb0371126549007/tests/saw/spec/handshake/handshake_io_lowlevel.saw#L163-L165

In addition, the proofs currently assume that conn->client_session_resumed will be disabled as well. This assumption is made explicit in #3079—see https://github.com/aws/s2n-tls/pull/3079#discussion_r721291815.

While these assumptions make the proofs somewhat simpler, they have the drawback of making the proofs skip over certain parts of s2n-tls, such as session resumption logic.

Solution:

We should remove these preconditions and repair the SAW proofs accordingly. Here is a rough sketch of how this might go for the particular case of conn->client_session_resumed:

1. Remove the crucible_precond statement involving conn_client_session_resumed_index.

2. Add a new field to the Cryptol connection record which tracks if the client_session_resumed bit in s2n_connection is enabled or not.

3. In setup_connection_common, initialize this new Cryptol field with the appropriate value.

4. The code in the conn_set_pre_tls13_handshake_type Cryptol function will need to be updated accordingly. Something like this, perhaps:

   diff --git a/tests/saw/spec/handshake/s2n_handshake_io.cry b/tests/saw/spec/handshake/s2n_handshake_io.cry
   index b466aa20f8..452f09f7be 100644
   --- a/tests/saw/spec/handshake/s2n_handshake_io.cry
   +++ b/tests/saw/spec/handshake/s2n_handshake_io.cry
   @@ -27,6 +27,7 @@ conn_set_pre_tls13_handshake_type conn = conn'
                    ,server_can_send_ocsp = conn.server_can_send_ocsp
                    ,key_exchange_eph = conn.key_exchange_eph
                    ,client_auth_flag = conn.client_auth_flag
   +                ,client_session_resumed = conn.client_session_resumed
                    ,actual_protocol_version = conn.actual_protocol_version
                    ,no_client_cert = conn.no_client_cert
                    ,early_data_state = conn.early_data_state
   @@ -36,9 +37,9 @@ conn_set_pre_tls13_handshake_type conn = conn'
            (handshake' : handshake) = {handshake_type = handshake_type'
                                       ,message_number = conn.handshake.message_number
                                       }
   -        handshake_type' = NEGOTIATED || full_handshake ||
   -                            (if (full_handshake != 0) then
   -                              perfect_forward_secrecy || ocsp_status || client_auth
   +        handshake_type' = NEGOTIATED || client_auth ||
   +                            (if (~is_client_session_resumed) then
   +                              full_handshake || perfect_forward_secrecy || ocsp_status
                                  else zero)
            full_handshake  = if (conn.is_caching_enabled /\ ~conn.resume_from_cache)
                              then zero
   @@ -52,6 +53,7 @@ conn_set_pre_tls13_handshake_type conn = conn'
            client_auth = if conn.client_auth_flag
                          then CLIENT_AUTH
                          else zero
   +        is_client_session_resumed = conn.mode == S2N_CLIENT /\ conn.client_session_resumed
   
    // This function models the update of the s2n_connection struct by the
    // s2n_conn_set_tls13_handshake_type function in s2n.
   

5. The rfc_handshake_tls12 proofs will also need to be updated.

• Does this change what S2N sends over the wire? No.
• Does this change any public APIs? No.
• Which versions of TLS will this impact? This should only affect the TLS 1.2–specific code paths in the SAW proofs.

Requirements / Acceptance Criteria:

What must a solution address in order to solve the problem? How do we know the solution is complete?

• RFC links: Links to relevant RFC(s)
• Related Issues: The PR in which the assumptions about client_session_resumed were uncovered: https://github.com/aws/s2n-tls/pull/3079#discussion_r721291815
• Will the Usage Guide or other documentation need to be updated?
• Testing: This should be tested by running the make -C tests/saw tmp/verify_handshake.log and make -C tests/saw failure-tests tests.
  • Will this change trigger SAW changes? Yes.
  • Should this change be fuzz tested? No.

Out of scope:

This does not address other hard-coded assumptions made in the SAW proofs, such as what the value of corked_io should be:

https://github.com/aws/s2n-tls/blob/2c27512895e8a2945f97b5137bb0371126549007/tests/saw/spec/handshake/handshake_io_lowlevel.saw#L111-L113

[toidiu]

Has this issue been resolved and can be closed? If not could you update it specify what is left to do. Thank you.

@RyanGlScott

[RyanGlScott]

This issue has not been resolved, although some of the code described in https://github.com/aws/s2n-tls/issues/3080#issue-1015463448 shuffled around in #3155. In particular, the code which assumes that conn->client_session_resumed is disabled now lives here:

https://github.com/aws/s2n-tls/blob/5edafa73bbbd3d7dec6d44785ebff634cc914d2f/tests/saw/spec/handshake/handshake_io_lowlevel.saw#L181-L183

And the code which assumes that config->use_tickets is disabled now lives here:

https://github.com/aws/s2n-tls/blob/5edafa73bbbd3d7dec6d44785ebff634cc914d2f/tests/saw/spec/handshake/handshake_io_lowlevel.saw#L185-L187

Step (1) in my sketched solution would be to remove these lines instead of removing crucible_precond statements (which no longer appear after #3155). The rest of the sketched solution should still apply.