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

RyanGlScott commented 2 years ago

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:

Remove the crucible_precond statement involving conn_client_session_resumed_index.
Add a new field to the Cryptol connection record which tracks if the client_session_resumed bit in s2n_connection is enabled or not.
In setup_connection_common, initialize this new Cryptol field with the appropriate value.

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.

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 commented 2 years ago

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 commented 2 years ago

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.

aws / s2n-tls