Server hrr support (#1742)

* Server support for Hello Retry Requests

 * Rewrite transcript after the HelloRetryRequest is sent.
   This prevents the need for cookies to store the ClientHello1 hash.
 * Refactor transcript rewrites into a new unit
 * Refactor get_hash_state.
 * Add an integration test for an unsupported curve that forces
   a retry.
 * OpenSSL and BoringSSL handshakes are successful

* Refactor the way HelloRetryRequests are handled.

 * Add new handshake type to handle to multiple CH and SH messages.

* SAW Tests

 * Update Cryptol models for the new handshake types.
 * Update RFC definitions to handle HelloRetryRequests.

* Updates to code and tests after removing client support for HRR.

* Modifications to handshake types supporting HelloRetryRequests.
Small modifications based on PR feedback.

* Update handshake_io_lowlevel.saw

.travis/s2n_setup_env.sh

@@ -84,6 +84,9 @@ export S2N_CORKED_IO
 export S2N_NO_PQ_ASM
 
 
+# Unset the FIPS flag incase the tester has changed modes after a FIPS test
+unset S2N_TEST_IN_FIPS_MODE
+
 # Select the libcrypto to build s2n against. If this is unset, default to the latest stable version(Openssl 1.1.1)
 if [[ -z $S2N_LIBCRYPTO ]]; then export LIBCRYPTO_ROOT=$OPENSSL_1_1_1_INSTALL_DIR ; fi
 if [[ "$S2N_LIBCRYPTO" == "openssl-1.1.1" ]]; then export LIBCRYPTO_ROOT=$OPENSSL_1_1_1_INSTALL_DIR ; fi

crypto/s2n_hash.c

@@ -199,7 +199,7 @@ static int s2n_low_level_hash_digest(struct s2n_hash_state *state, void *out, ui
         break;
     case S2N_HASH_MD5:
         eq_check(size, MD5_DIGEST_LENGTH);
-	GUARD_OSSL(MD5_Final(out, &state->digest.low_level.md5), S2N_ERR_HASH_DIGEST_FAILED);
+        GUARD_OSSL(MD5_Final(out, &state->digest.low_level.md5), S2N_ERR_HASH_DIGEST_FAILED);
         break;
     case S2N_HASH_SHA1:
         eq_check(size, SHA_DIGEST_LENGTH);
@@ -406,8 +406,8 @@ static int s2n_evp_hash_copy(struct s2n_hash_state *to, struct s2n_hash_state *f
         if (s2n_digest_is_md5_allowed_for_fips(&from->digest.high_level.evp)) {
             GUARD(s2n_hash_allow_md5_for_fips(to));
         }
-	GUARD_OSSL(EVP_MD_CTX_copy_ex(to->digest.high_level.evp.ctx, from->digest.high_level.evp.ctx), S2N_ERR_HASH_COPY_FAILED);
-	GUARD_OSSL(EVP_MD_CTX_copy_ex(to->digest.high_level.evp_md5_secondary.ctx, from->digest.high_level.evp_md5_secondary.ctx), S2N_ERR_HASH_COPY_FAILED);
+        GUARD_OSSL(EVP_MD_CTX_copy_ex(to->digest.high_level.evp.ctx, from->digest.high_level.evp.ctx), S2N_ERR_HASH_COPY_FAILED);
+        GUARD_OSSL(EVP_MD_CTX_copy_ex(to->digest.high_level.evp_md5_secondary.ctx, from->digest.high_level.evp_md5_secondary.ctx), S2N_ERR_HASH_COPY_FAILED);
         break;
     default:
         S2N_ERROR(S2N_ERR_HASH_INVALID_ALGORITHM);

tests/integration/common/s2n_test_scenario.py

@@ -25,6 +25,7 @@
 from enum import Enum as BaseEnum
 from multiprocessing.pool import ThreadPool
 
+
 class Enum(BaseEnum):
 
     def __str__(self):
@@ -281,4 +282,3 @@ def get_scenarios(host, start_port, s2n_modes=Mode.all(), versions=[None], ciphe
             port += 1
 
     return scenarios
-

tests/integration/s2n_tls13_handshake_tests.py

@@ -23,7 +23,29 @@
 import sys
 
 from common.s2n_test_openssl import run_openssl_connection_test
-from common.s2n_test_scenario import get_scenarios, Mode, Cipher, Version
+from common.s2n_test_scenario import get_scenarios, Mode, Cipher, Version, Curve
+from common.s2n_test_reporting import Result, Status
+import common.s2n_test_common as util
+
+
+def verify_hrr_random_data(server, client):
+    """
+    This callback verifies a HelloRetryRequest was sent from the S2N
+    server. If the rest of the integration test passes as well, then
+    the handshake completed after the HelloRetryRequest was sent.
+    """
+    result = Result()
+    result.status = Status.FAILED
+
+    # Start of HRR random data which will be printed in the
+    # client process output
+    marker = b"cf 21 ad 74 e5 9a 61 11 be 1d"
+    for line in client.stdout:
+        if marker in line:
+            result.status = Status.PASSED
+            break
+
+    return result
 
 
 def main():
@@ -39,6 +61,9 @@ def main():
 
     print("\n\tRunning TLS1.3 handshake tests with openssl: %s" % os.popen('openssl version').read())
     failed += run_openssl_connection_test(get_scenarios(host, port, versions=[Version.TLS13], s2n_modes=Mode.all(), ciphers=Cipher.all()))
+    print("\n\tRunning TLS1.3 HRR tests with openssl: %s" % os.popen('openssl version').read())
+    failed += run_openssl_connection_test(get_scenarios(host, port, versions=[Version.TLS13], s2n_modes=[Mode.server], ciphers=Cipher.all(),
+                                                        peer_flags=['-msg', '-curves', 'X448:P-256']), test_func=verify_hrr_random_data)
 
     return failed
 

tests/saw/spec/handshake/handshake.saw

@@ -57,7 +57,7 @@ let prove_handshake_io_lowlevel = do {
     print "s2n_connection_is_managed_corked";
     s2n_connection_is_managed_corked <- crucible_llvm_unsafe_assume_spec llvm "s2n_connection_is_managed_corked" s2n_connection_is_managed_corked_spec;
     print "s2n_generate_new_client_session_id";
-    s2n_generate_new_client_session_id <- crucible_llvm_unsafe_assume_spec llvm "s2n_generate_new_client_session_id" s2n_generate_new_client_session_id_spec;    
+    s2n_generate_new_client_session_id <- crucible_llvm_unsafe_assume_spec llvm "s2n_generate_new_client_session_id" s2n_generate_new_client_session_id_spec;
     print "s2n_allowed_to_cache_connection";
     s2n_allowed_to_cache_connection <- crucible_llvm_unsafe_assume_spec llvm "s2n_allowed_to_cache_connection" s2n_allowed_to_cache_connection_spec;
     print "s2n_decrypt_session_ticket";
@@ -70,9 +70,9 @@ let prove_handshake_io_lowlevel = do {
     s2n_advance_message_proof <- crucible_llvm_verify llvm "s2n_advance_message" dependencies false s2n_advance_message_spec yices;
     print "Proving correctness of s2n_conn_set_handshake_type";
     s2n_conn_set_handshake_type_proof <- crucible_llvm_verify llvm "s2n_conn_set_handshake_type" [s2n_allowed_to_cache_connection, auth_type_proof, s2n_generate_new_client_session_id, s2n_decrypt_session_ticket] false s2n_conn_set_handshake_type_spec yices;
-    
+
     print "Done: Verified that the low-level specification corresponds to the C code";
-    
+
     return ();
 };
 
@@ -83,19 +83,19 @@ let prove_state_machine = do {
     // TLS1.3 is temporarily removed from SAW testing.
     // print "Checking proof that the TLS1.3 RFC simulates our Cryptol s2n spec";
     // prove_print z3 {{ tls13rfcSimulatesS2N `{16} }};
-    
+
     return ();
 };
 
 let prove_cork_uncork = do {
     print "Verifying the low-level->high-level cork-uncork simulation";
-    prove_print abc {{ highLevelSimulatesLowLevel `{16} }}; 
-    
+    prove_print abc {{ highLevelSimulatesLowLevel `{16} }};
+
     print "Verifying that double uncorking or corking cannot occur in server mode";
     prove_print abc {{ noDoubleCorkUncork `{16} }};
-    
+
     print "Expecting failure when proving low-high simulation without the server mode assumption";
     sat abc {{ ~highLevelDoesNotSimulateLowLevel `{16} }};
-    
+
     return ();
 };

tests/saw/spec/handshake/handshake_io_lowlevel.saw

@@ -28,7 +28,12 @@ import "s2n_handshake_io.cry";
 llvm <- llvm_load_module "../../bitcode/all_llvm.bc";
 print "Loaded bitcode via Crucible";
 
+////////////////////////////////////////////////////////////////
 // References to various components of the connection state:
+// The Cryptol definitions are located in the s2n_handshake_io.cry file.
+// Those Cryptol definitions will be compared against the actual C
+// definitions by this SAW script.
+////////////////////////////////////////////////////////////////
 
 //conn->corked_io
 let conn_corked_io pconn = crucible_field pconn "corked_io";
@@ -169,6 +174,8 @@ let setup_connection = do {
 
    let client_cert_auth_type = {{ if cca_ov != 0 then cca else config_cca }};
 
+   // This returns a connection containing a handshake. If the connection or the handshake
+   // definitions are changed, they must also be changed here.
    return (pconn, {{ {corked_io = corked_io
                      ,mode      = mode
                      ,handshake = {message_number = message_number
@@ -182,8 +189,8 @@ let setup_connection = do {
                      ,resume_from_cache = False
                      ,client_auth_flag = if mode == S2N_CLIENT then client_cert_auth_type == 1 else 
                                          if mode == S2N_SERVER then client_cert_auth_type != 0 else False
-                     ,actual_protocol_version = version
                      ,no_client_cert = no_client_cert != zero
+                     ,actual_protocol_version = version
                      }
                   }}); 
 };
@@ -246,6 +253,8 @@ let s2n_conn_set_handshake_type_spec = do {
     // we assume that the handshake struct denotes a valid handshake state
     // (e.g. it will not index out of bounds in the state transition array
     // "handshakes")
+    // conn.handshake is defined in s2n_handshake_io.cry.
+    // valid_handshake is defined in s2n_handshake_io.cry as well.
     crucible_precond {{ valid_handshake conn.handshake }};
 
     // symbolically execute s2n_conn_set_handshake_type
@@ -295,6 +304,7 @@ let s2n_advance_message_spec = do {
     // make sure the low-level spec representation of the declarative
     // handshake/cork-uncork state machine is equivalent to the one in
     // s2n
+    // The Cryptol representations are defined here: tests/saw/spec/handshake/s2n_handshake_io.cry
     crucible_points_to (crucible_global "handshakes") (crucible_term {{ handshakes }});
 
     // TLS1.3 is temporarily removed from SAW testing.

tests/saw/spec/handshake/s2n_handshake_io.cry

@@ -170,7 +170,7 @@ IS_TLS13_HANDSHAKE conn = conn.actual_protocol_version == S2N_TLS13
 ACTIVE_STATE_MACHINE : connection -> [19]handshake_action
 ACTIVE_STATE_MACHINE conn = if IS_TLS13_HANDSHAKE conn then tls13_state_machine else state_machine # zero
 
-ACTIVE_HANDSHAKES : connection -> [128][32][32]
+ACTIVE_HANDSHAKES : connection -> [256][32][32]
 ACTIVE_HANDSHAKES conn = if IS_TLS13_HANDSHAKE conn then tls13_handshakes else handshakes
 
 ACTIVE_MESSAGE : connection -> [32]
@@ -257,8 +257,8 @@ state_machine_fn m =
   else zero
 
 // A model of the tls1.3 handshake state machine (array handshakes in C)
-tls13_handshakes : [128][32][32]
-tls13_handshakes = [tls13_handshakes_fn h | h <- [0..127]]
+tls13_handshakes : [256][32][32]
+tls13_handshakes = [tls13_handshakes_fn h | h <- [0..255]]
 
 // A function that gives the tls1.3 handshake sequence for each valid handshake_type.
 tls13_handshakes_fn: [32] -> [32][32]
@@ -285,8 +285,8 @@ tls13_handshakes_fn handshk =
   else zero
 
 // A model of the handshake state machine (array handshakes in C)
-handshakes : [128][32][32]
-handshakes = [handshakes_fn h | h <- [0..127]]
+handshakes : [256][32][32]
+handshakes = [handshakes_fn h | h <- [0..255]]
 
 // A function that gives the handshake sequence for each valid handshake_type.
 // This is a sparse encoding of the handshakes array (which is sparse too).
@@ -512,7 +512,7 @@ SERVER_CHANGE_CIPHER_SPEC = 13
 SERVER_FINISHED = 14
 ENCRYPTED_EXTENSIONS = 15
 SERVER_CERT_VERIFY = 16
-APPLICATION_DATA = 17
+APPLICATION_DATA = 18
 
 //TLS record type
 TLS_CHANGE_CIPHER_SPEC = 20

tests/testlib/s2n_connection_test_utils.c

@@ -201,3 +201,12 @@ void s2n_print_connection(struct s2n_connection *conn, const char *marker)
     }
     printf("\n");
 }
+
+int s2n_set_connection_hello_retry_flags(struct s2n_connection *conn)
+{
+    conn->actual_protocol_version = S2N_TLS13;
+    conn->handshake.message_number = 1;
+    conn->handshake.handshake_type = NEGOTIATED | HELLO_RETRY_REQUEST | FULL_HANDSHAKE;
+
+    return 0;
+}

tests/testlib/s2n_testlib.h

@@ -55,6 +55,8 @@ int s2n_connections_set_piped_io(struct s2n_connection *client, struct s2n_conne
 int s2n_fd_set_blocking(int fd);
 int s2n_fd_set_non_blocking(int fd);
 
+int s2n_set_connection_hello_retry_flags(struct s2n_connection *conn);
+
 #define S2N_MAX_TEST_PEM_SIZE 4096
 
 /* These paths assume that the unit tests are run from inside the unit/ directory.