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:

s2n-tls/tests/saw/spec/handshake/handshake_io_lowlevel.saw

Lines 163 to 165 in 2c27512

	// The following line could be made more precise, we only care that the use_tickets
	// bit is zero
	crucible_equal (crucible_term config_bitfield_value) (crucible_term {{zero : [16]}});

In addition, the proofs currently assume that conn->client_session_resumed will be disabled as well. This assumption is made explicit in #3079—see #3079 (comment).

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: Repair TLS 1.3 proofs after c096a55 #3079 (comment)
• 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:

s2n-tls/tests/saw/spec/handshake/handshake_io_lowlevel.saw

Lines 111 to 113 in 2c27512

	// we assume that corking/uncorking is managed by s2n
	let corked_io = {{1 : [8]}};
	crucible_points_to (conn_corked_io pconn) (crucible_term corked_io);

[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 #3080 (comment) shuffled around in #3155. In particular, the code which assumes that conn->client_session_resumed is disabled now lives here:

s2n-tls/tests/saw/spec/handshake/handshake_io_lowlevel.saw

Lines 181 to 183 in 5edafa7

	// ...we assume that the client_session_resumed bit in s2n_connection must
	// be zero...
	llvm_points_to_bitfield pconn "client_session_resumed" (llvm_term {{ 0 : [1] }});

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

s2n-tls/tests/saw/spec/handshake/handshake_io_lowlevel.saw

Lines 185 to 187 in 5edafa7

	// ...we currently require that the use_tickets bit in s2n_config must be
	// zero...
	llvm_points_to_bitfield config "use_tickets" (llvm_term {{ 0 : [1] }});

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.