From d5a044b8ce4eee8273397ee99d224faf8b562a39 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 29 Sep 2021 13:33:00 -0400 Subject: [PATCH] Re-enable TLS 1.3 SAW tests (#3031) --- tests/saw/spec/handshake/cork_uncork.cry | 48 ++- tests/saw/spec/handshake/handshake.saw | 32 +- .../spec/handshake/handshake_io_lowlevel.saw | 134 +++++-- .../spec/handshake/rfc_handshake_tls13.cry | 37 +- tests/saw/spec/handshake/s2n_handshake_io.cry | 352 ++++++++++++++++-- tls/Makefile | 4 +- 6 files changed, 513 insertions(+), 94 deletions(-) diff --git a/tests/saw/spec/handshake/cork_uncork.cry b/tests/saw/spec/handshake/cork_uncork.cry index 3bd8c014e98..432b53e3de7 100644 --- a/tests/saw/spec/handshake/cork_uncork.cry +++ b/tests/saw/spec/handshake/cork_uncork.cry @@ -24,24 +24,46 @@ type State = ([2], [2]) // For any two related 'connection' and corking 'State' they produce related // corking traces. +// We only check handshakes up until the first APPLICATION_DATA. highLevelSimulatesLowLevel : {len} (fin len, len >= 2) => connection -> State -> Bit highLevelSimulatesLowLevel conn state = - initial_connection conn /\ conn.mode == S2N_SERVER /\ conn2state conn == state ==> - (map conn2state conn_trace) == (trace_corking `{n = len} state writers) + initial_connection conn /\ conn.mode == S2N_SERVER /\ conn.corked == uncorked /\ conn2state conn == state ==> + go 0 where (conn_trace : [len]connection) = trace_advance_message `{n = len} conn writers = drop `{1} (map getWriter conn_trace) + conn_trace_states : [len]State + conn_trace_states = map conn2state conn_trace + + trace_corking_states : [len]State + trace_corking_states = trace_corking `{n = len} state writers + + go : [width len] -> Bit + go i = if i >= `len + then True + | (ACTIVE_STATE (conn_trace@i)).record_type == TLS_APPLICATION_DATA + then (trace_corking_states@i).1 == uncorked + else (conn_trace_states@i == trace_corking_states@i) /\ go (i+1) + // Property of the high-level state machine: there is no uncorking or corking // twice in a row // This is not true for arbitrary sequences of writers, as for example a server // could transition S->A->S and cork twice. However, we do not have such // a sequence possible given the handshake sequences +// We only check handshakes up until the first APPLICATION_DATA. noDoubleCorkUncork : {len} (fin len, len >= 2) => connection -> Bit noDoubleCorkUncork conn = - initial_connection conn ==> and (map corkingInBounds (run writers)) + initial_connection conn ==> go 0 where (conn_trace : [len]connection) = trace_advance_message `{n = len} conn writers = map getWriter conn_trace + run_writers_corking_in_bounds : [len+1]Bit + run_writers_corking_in_bounds = map corkingInBounds (run writers) + + go : [width len] -> Bit + go i = if i >= `len then True + | (ACTIVE_STATE (conn_trace@i)).record_type == TLS_APPLICATION_DATA then True + else run_writers_corking_in_bounds@i /\ go (i+1) writer2sender : [8] -> [2] writer2sender w = if w == 'C' then clientSender else @@ -53,7 +75,7 @@ corkedFromConn conn = if mode_writer conn.mode == (ACTIVE_STATE conn).writer the else 0 trace_advance_message : {n} (fin n) => connection -> [n]connection -trace_advance_message conn = take (iterate advance_message conn) +trace_advance_message conn = take (iterate s2nTrans conn) trace_corking : {n} (fin n, n >= 2) => State -> [n-1][8] -> [n]State trace_corking s writers = scanl cork_transition s writers @@ -68,13 +90,27 @@ conn2state conn = (writer2sender (getWriter conn), conn.corked) // mode" precondition. // We wrap this with negation to show that we can't do this proof without // the server-mode assumption +// We only check handshakes up until the first APPLICATION_DATA. highLevelDoesNotSimulateLowLevel : {len} (fin len, len >= 2) => connection -> State -> Bit highLevelDoesNotSimulateLowLevel conn state = - initial_connection conn /\ conn2state conn == state ==> - (map conn2state conn_trace) == (trace_corking `{n = len} state writers) + initial_connection conn /\ conn2state conn == state /\ conn.corked == uncorked ==> + go 0 where (conn_trace : [len]connection) = trace_advance_message `{n = len} conn writers = drop `{1} (map getWriter conn_trace) + conn_trace_states : [len]State + conn_trace_states = map conn2state conn_trace + + trace_corking_states : [len]State + trace_corking_states = trace_corking `{n = len} state writers + + go : [width len] -> Bit + go i = if i >= `len + then True + | (ACTIVE_STATE (conn_trace@i)).record_type == TLS_APPLICATION_DATA + then (trace_corking_states@i).1 == uncorked + else (conn_trace_states@i == trace_corking_states@i) /\ go (i+1) + // The abstract transition function for the cork/uncork state machine cork_transition : State -> [8] -> State cork_transition (s, corking) c = diff --git a/tests/saw/spec/handshake/handshake.saw b/tests/saw/spec/handshake/handshake.saw index 63eb53fa27f..2ebe7d3fdb9 100644 --- a/tests/saw/spec/handshake/handshake.saw +++ b/tests/saw/spec/handshake/handshake.saw @@ -26,9 +26,7 @@ include "handshake_io_lowlevel.saw"; import "rfc_handshake_tls12.cry"; - -// TLS1.3 is temporarily removed from SAW testing. -// import "rfc_handshake_tls13.cry"; +import "rfc_handshake_tls13.cry"; import "cork_uncork.cry"; @@ -38,7 +36,7 @@ let yices_debug = do { yices; print_goal; }; // Workaround for If then else on nat let equalNat_ite = core_axiom - "\\(x y z : Nat) (b : Bool) -> eq Bool (equalNat x (ite Nat b y z)) (ite Bool b (equalNat x y) (equalNat x z))"; + "(x y z : Nat) -> (b : Bool) -> Eq Bool (equalNat x (ite Nat b y z)) (ite Bool b (equalNat x y) (equalNat x z))"; // Low-level handshake_io correspondence proof let prove_handshake_io_lowlevel = do { @@ -68,8 +66,19 @@ let prove_handshake_io_lowlevel = do { auth_type_proof <- crucible_llvm_verify llvm "s2n_connection_get_client_auth_type" dependencies false s2n_connection_get_client_auth_type_spec (do {simplify (addsimp equalNat_ite basic_ss); yices;}); print "Proving correctness of s2n_advance_message"; 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; + // To prove s2n_conn_set_handshake_type's correctness, we invoke its + // specification (s2n_conn_set_handshake_type_spec) twice: once where + // chosen_psk is assumed to be NULL, and once again where chosen_psk is + // assumed to be non-NULL. This is needed to ensure all code paths are + // tested if TLS 1.3 is used, as whether FULL_HANDSHAKE is enabled or not + // depends on whether chosen_psk is NULL. + // + // Issue #3052 is about removing the need to invoke the specification twice. + let s2n_conn_set_handshake_type_ovs = [s2n_allowed_to_cache_connection, auth_type_proof, s2n_generate_new_client_session_id, s2n_decrypt_session_ticket]; + print "Proving correctness of s2n_conn_set_handshake_type (NULL chosen_psk)"; + s2n_conn_set_handshake_type_chosen_psk_null_proof <- crucible_llvm_verify llvm "s2n_conn_set_handshake_type" s2n_conn_set_handshake_type_ovs false (s2n_conn_set_handshake_type_spec true) yices; + print "Proving correctness of s2n_conn_set_handshake_type (non-NULL chosen_psk)"; + s2n_conn_set_handshake_type_chosen_psk_non_null_proof <- crucible_llvm_verify llvm "s2n_conn_set_handshake_type" s2n_conn_set_handshake_type_ovs false (s2n_conn_set_handshake_type_spec false) yices; print "Done: Verified that the low-level specification corresponds to the C code"; @@ -80,22 +89,21 @@ let prove_state_machine = do { print "Checking proof that the TLS1.2 RFC simulates our Cryptol s2n spec"; prove_print abc {{ tls12rfcSimulatesS2N `{16} }}; - // 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} }}; + 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 z3 {{ highLevelSimulatesLowLevel `{16} }}; print "Verifying that double uncorking or corking cannot occur in server mode"; - prove_print abc {{ noDoubleCorkUncork `{16} }}; + prove_print z3 {{ noDoubleCorkUncork `{16} }}; print "Expecting failure when proving low-high simulation without the server mode assumption"; - sat abc {{ ~highLevelDoesNotSimulateLowLevel `{16} }}; + sat z3 {{ ~highLevelDoesNotSimulateLowLevel `{16} }}; return (); }; diff --git a/tests/saw/spec/handshake/handshake_io_lowlevel.saw b/tests/saw/spec/handshake/handshake_io_lowlevel.saw index c033e401520..c337a0615df 100644 --- a/tests/saw/spec/handshake/handshake_io_lowlevel.saw +++ b/tests/saw/spec/handshake/handshake_io_lowlevel.saw @@ -64,17 +64,19 @@ let config_cca_type config = (crucible_field config "client_cert_auth_type"); let ocsp_status_size cert_and_key = crucible_field (crucible_field (cert_and_key) "ocsp_status") "size"; -//conn->config->use_tickets is the field we care about, but it is -// in a bitfield. For now, we only care about that, so we point -// at the entire bitfield and say it must all be initialized to -// a value of 0 for the proof to go through. This is a stronger -// statement than we stricly need to make, and will limit -// compositional proofs in the future, but we can make more -// precise statements at that time +// conn->config->use_tickets and conn->config->quic_enabled are the fields we +// care about, but they are in a bitfield. We currently handle this by +// initializing the entire bitfield with a symbolic value and imposing a +// precondition that bit 3 (i.e., use_tickets) must be equal to 0. +// Bit 9 (i.e., quic_enabled), on the other hand, is allowed to be either +// 0 or 1. // It's also noteworthy that we use the crucible_elem here, which will // cause problems if the fields are reordered. This is reasonably unlikely -// because it makes sense to have the bitfield at the start +// because it makes sense to have the bitfield at the start, but it is a bit +// fragile nonetheless. If https://github.com/GaloisInc/saw-script/issues/1461 +// were implemented, we could reference the names of bitfields instead of their +// offsets, which would avoid this issue. let config_bitfield config = (crucible_elem config 0); //conn->session_ticket_status @@ -98,22 +100,37 @@ let conn_handshake_message_number pconn = let conn_chain_and_key pconn = crucible_field (crucible_field pconn "handshake_params") "our_chain_and_key"; +//conn->psk_params.chosen_psk +let conn_chosen_psk pconn = + crucible_field (crucible_field pconn "psk_params") "chosen_psk"; + +//conn->early_data_state +let conn_early_data_state pconn = crucible_field pconn "early_data_state"; + // Ghost state that represents the number of times the connection write socket // has been corked/uncorked. corked <- crucible_declare_ghost_state "corked"; crucible_ghost_value corked {{ 0 : [2] }}; -// setup_handshake de-serializes parts of the s2n_handshake and s2n_connection -// structs into a Cryptol record. It also deserializes the ghost state. -let setup_connection = do { +// setup_handshake_common de-serializes parts of the s2n_handshake and +// s2n_connection structs into a Cryptol record. It also deserializes the ghost +// state. We use the suffix "_common" since it captures the properties shared +// in common between setup_connection and setup_psk_connection. +// +// The chosen_psk_null argument is true if conn->psk_params.chosen_psk should +// be set to NULL, which enables the use of FULL_HANDSHAKE if TLS 1.3 is used. +// If false, then chosen_psk is set to a non-NULL value, disabling +// FULL_HANDSHAKE if TLS 1.3 is used. The value of conn->psk_params.chosen_psk +// has no effect if TLS 1.2 is used. +let setup_connection_common chosen_psk_null = do { pconn <- crucible_alloc (llvm_struct "struct.s2n_connection"); // 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); - // TLS1.3 is temporarily removed from SAW testing, force the TLS1.2 version - let version = {{33 : [8]}}; + version <- crucible_fresh_var "version" (llvm_int 8); + crucible_precond {{ version != S2N_UNKNOWN_PROTOCOL_VERSION /\ version <= S2N_TLS13 }}; crucible_points_to (crucible_field pconn "actual_protocol_version") (crucible_term version); mode <- crucible_fresh_var "mode" (llvm_int 32); @@ -160,9 +177,14 @@ let setup_connection = do { config_bitfield_value <- crucible_fresh_var "config_bitfield" (llvm_int 16); crucible_points_to (config_bitfield config) (crucible_term config_bitfield_value); - // 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]}}); + // We currently require that the use_tickets bit is zero. Because + // use_tickets is the third field in a bitfield, we force it to be zero by + // requiring that bit 3 in the bitfield (corresponding to a bitmask of + // 2^(3 - 1) = 4) be set to zero. + crucible_equal (crucible_term {{ config_bitfield_value && 4 }}) (crucible_term {{ zero : [16] }}); + // quic_enabled is bit 9 in the bitfield, corresponding to a bitmask of + // 2^(9 - 1) = 256. + let quic_enabled_bit = {{ (config_bitfield_value && 256) != zero }}; session_ticket_status <- crucible_fresh_var "session_ticket_status" (llvm_int 32); crucible_points_to (conn_session_ticket_status pconn) (crucible_term session_ticket_status); @@ -170,6 +192,16 @@ let setup_connection = do { ocsp_flag <- crucible_fresh_var "ocsp_flag" (llvm_int 32); crucible_points_to (conn_status_type pconn) (crucible_term ocsp_flag); + if chosen_psk_null + then crucible_points_to (conn_chosen_psk pconn) crucible_null + else do { chosen_psk <- crucible_alloc (llvm_struct "struct.s2n_psk"); + crucible_points_to (conn_chosen_psk pconn) chosen_psk; + }; + let chosen_psk_null_bit = if chosen_psk_null then {{ True }} else {{ False }}; + + early_data_state <- crucible_fresh_var "early_data_state" (llvm_int 32); + crucible_points_to (conn_early_data_state pconn) (crucible_term early_data_state); + no_client_cert <- crucible_fresh_var "no_client_cert" (llvm_int 8); let client_cert_auth_type = {{ if cca_ov != 0 then cca else config_cca }}; @@ -187,14 +219,26 @@ let setup_connection = do { ((ocsp_flag == 1) && (status_size > 0)) || ((mode == 1) && (ocsp_flag == 1)) ,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 + ,client_auth_flag = if mode == S2N_CLIENT then client_cert_auth_type == S2N_CERT_AUTH_REQUIRED else + if mode == S2N_SERVER then client_cert_auth_type != S2N_CERT_AUTH_NONE else False ,no_client_cert = no_client_cert != zero ,actual_protocol_version = version + ,early_data_state = early_data_state + ,chosen_psk_null = chosen_psk_null_bit + ,quic_enabled = quic_enabled_bit } }}); }; +// Set conn->psk_params.chosen_psk to NULL, which enables the use of FULL_HANDSHAKE +// if TLS 1.3 is used. Note that if TLS 1.2 is used, there is no difference between +// this function and setup_psk_connection. +let setup_connection = setup_connection_common true; + +// Set conn->psk_params.chosen_psk to a non-NULL value, which disables the use of FULL_HANDSHAKE +// if TLS 1.3 is used. Note that if TLS 1.2 is used, there is no difference between +// this function and setup_connection. +let setup_psk_connection = setup_connection_common false; // This function checks that the values of the state_machine array are what we @@ -248,8 +292,8 @@ let s2n_connection_get_client_auth_type_spec = do{ // Specification for s2n_conn_set_handshake_type that sets up simulation of it // by conn_set_handshake_type (low-level model function) -let s2n_conn_set_handshake_type_spec = do { - (pconn, conn) <- setup_connection; +let s2n_conn_set_handshake_type_spec chosen_psk_null = do { + (pconn, conn) <- setup_connection_common chosen_psk_null; // 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") @@ -279,6 +323,9 @@ let s2n_conn_set_handshake_type_spec = do { // specification for s2n_advance_message that sets up simulation of it // by advance_message (low-level model function) let s2n_advance_message_spec = do { + // Note that s2n_advance_message() doesn't actually care about the value of + // chosen_psk, so we arbitrarily set it to NULL here by using + // setup_connection. Using setup_psk_connection would work just as well. (pconn, conn) <- setup_connection; // 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 @@ -305,19 +352,46 @@ let s2n_advance_message_spec = do { // 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. - // crucible_points_to (crucible_global "tls13_handshakes") (crucible_term {{ tls13_handshakes }}); + // + // Note that we use crucible_points_to_untyped here rather than + // crucible_points_to because LLVM 7 and later represent static arrays that + // are partially initialized with zeroes as packed structs. For more + // information, see + // https://llvm.discourse.group/t/array-layout-changed-by-clang-llvm-starting-from-version-7/2271 + // + // Changing the Cryptol definitions of the state machines to match these + // new types would be annoying, and moreover, it isn't guaranteed that + // future versions of LLVM won't change the types further. Fortunately, the + // in-memory representation of the arrays hasn't changed, just the types. + // As a result, we can use crucible_points_to_untyped to check if the two + // state machines are bitwise equivalent without checking the types. + crucible_points_to_untyped (crucible_global "handshakes") (crucible_term {{ handshakes }}); + crucible_points_to_untyped (crucible_global "tls13_handshakes") (crucible_term {{ tls13_handshakes }}); - let messages = [ {{CLIENT_HELLO : [5]}}, {{SERVER_HELLO : [5]}}, {{SERVER_CERT : [5]}}, {{SERVER_NEW_SESSION_TICKET : [5]}}, {{SERVER_CERT_STATUS : [5]}}, - {{SERVER_KEY : [5]}}, {{SERVER_CERT : [5]}}, {{SERVER_CERT_REQ : [5]}}, {{SERVER_HELLO_DONE : [5]}}, {{CLIENT_CERT : [5]}}, {{CLIENT_KEY : [5]}}, {{CLIENT_CERT_VERIFY : [5]}}, - {{CLIENT_CHANGE_CIPHER_SPEC : [5]}}, {{SERVER_FINISHED : [5]}}, {{ENCRYPTED_EXTENSIONS : [5]}}, {{SERVER_CERT_VERIFY : [5]}}, {{APPLICATION_DATA : [5]}} ]; + let messages = [ {{CLIENT_HELLO : [5]}} + , {{SERVER_HELLO : [5]}} + , {{SERVER_CERT : [5]}} + , {{SERVER_NEW_SESSION_TICKET : [5]}} + , {{SERVER_CERT_STATUS : [5]}} + , {{SERVER_KEY : [5]}} + , {{SERVER_CERT_REQ : [5]}} + , {{SERVER_HELLO_DONE : [5]}} + , {{CLIENT_CERT : [5]}} + , {{CLIENT_KEY : [5]}} + , {{CLIENT_CERT_VERIFY : [5]}} + , {{CLIENT_CHANGE_CIPHER_SPEC : [5]}} + , {{CLIENT_FINISHED : [5]}} + , {{SERVER_CHANGE_CIPHER_SPEC : [5]}} + , {{SERVER_FINISHED : [5]}} + , {{ENCRYPTED_EXTENSIONS : [5]}} + , {{SERVER_CERT_VERIFY : [5]}} + , {{HELLO_RETRY_MSG : [5]}} + , {{END_OF_EARLY_DATA : [5]}} + , {{APPLICATION_DATA : [5]}} + ]; for messages (verify_state_machine_elem (crucible_global "state_machine") {{ state_machine }} ); - - // TLS1.3 is temporarily removed from SAW testing. - // for messages (verify_state_machine_elem (crucible_global "tls13_state_machine") {{ tls13_state_machine }} ); + for messages (verify_state_machine_elem (crucible_global "tls13_state_machine") {{ tls13_state_machine }} ); // assert that s2n_advance_message returns 0 (true if the 4 // functions it calls don't fail) diff --git a/tests/saw/spec/handshake/rfc_handshake_tls13.cry b/tests/saw/spec/handshake/rfc_handshake_tls13.cry index 81434693757..cec57de474e 100644 --- a/tests/saw/spec/handshake/rfc_handshake_tls13.cry +++ b/tests/saw/spec/handshake/rfc_handshake_tls13.cry @@ -70,7 +70,8 @@ type Parameters = { retry : Bit, client_auth : Bit, no_client_cert : Bit, - zero_rtt : Bit + zero_rtt : Bit, + early_ccs : Bit } /** @@ -84,13 +85,20 @@ connectionParameters conn params = params.psk_mode == conn_psk_mode /\ params.client_auth == (conn_client_auth /\ ~params.psk_mode) /\ params.no_client_cert == (conn_no_client_cert /\ params.client_auth) /\ params.zero_rtt == (conn_zero_rtt /\ params.psk_mode) - /\ params.compat_mode == [ conn.mode != S2N_CLIENT, conn.mode == S2N_CLIENT ] + /\ params.compat_mode == + [ when_middlebox_compat (conn.mode != S2N_CLIENT) + , when_middlebox_compat (conn.mode == S2N_CLIENT) ] + /\ params.early_ccs == conn_early_ccs /\ conn.actual_protocol_version == S2N_TLS13 - where conn_psk_mode = False /* Not supported yet */ - conn_retry = False /* Not supported yet */ + where conn_psk_mode = ~conn.chosen_psk_null + conn_retry = (conn.handshake.handshake_type && HELLO_RETRY_REQUEST) != zero conn_client_auth = conn.client_auth_flag conn_no_client_cert = conn.no_client_cert - conn_zero_rtt = False /* Not supported yet */ + conn_early_ccs = (conn.handshake.handshake_type && EARLY_CLIENT_CCS) != zero + conn_zero_rtt = (conn.early_data_state == S2N_EARLY_DATA_ACCEPTED) + + conn_middlebox_compat = ~conn.quic_enabled \/ ((conn.handshake.handshake_type && MIDDLEBOX_COMPAT) != zero) + when_middlebox_compat b = conn_middlebox_compat /\ b type Action = { message : Message, @@ -237,19 +245,19 @@ stateMachine params = iterate (\s -> stateFor s.next) CLIENT_START_STATE CLIENT_START_STATE = state 1 [ action clientHello client True, - action changeCipherSpec client (params.zero_rtt /\ compatMode client) + action changeCipherSpec client (params.early_ccs /\ compatMode client) ] (if params.retry then HELLO_RETRY_STATE else SERVER_HELLO_STATE) HELLO_RETRY_STATE = state 2 [ action helloRetryRequest server True, action changeCipherSpec server (compatMode server), - action changeCipherSpec client (~params.zero_rtt /\ compatMode client), + action changeCipherSpec client (~params.early_ccs /\ compatMode client), action clientHello client True ] SERVER_HELLO_STATE SERVER_HELLO_STATE = state 3 [ action serverHello server True, - action changeCipherSpec server (~params.retry /\ ~params.zero_rtt /\ compatMode server), + action changeCipherSpec server (~params.retry /\ compatMode server), action encryptedExtensions server True ] (if params.psk_mode then SERVER_FINISH_STATE else SERVER_AUTH_STATE) @@ -261,7 +269,7 @@ stateMachine params = iterate (\s -> stateFor s.next) CLIENT_START_STATE SERVER_FINISH_STATE = state 5 [ action finished server True, - action changeCipherSpec client (~params.retry /\ ~params.zero_rtt /\ compatMode client), + action changeCipherSpec client (~params.retry /\ ~params.early_ccs /\ compatMode client), action endOfEarlyData client params.zero_rtt ] (if params.client_auth then CLIENT_AUTH_STATE else CLIENT_FINISH_STATE) @@ -292,7 +300,7 @@ rfc2S2N msg = mkAct recordType messageType writer messageType = if recordType != TLS_HANDSHAKE then noMessageType | msg.messageType == clientHello then TLS_CLIENT_HELLO | msg.messageType == serverHello then TLS_SERVER_HELLO - | msg.messageType == helloRetryRequest then TLS_HELLO_RETRY_REQUEST + | msg.messageType == helloRetryRequest then TLS_SERVER_HELLO | msg.messageType == encryptedExtensions then TLS_ENCRYPTED_EXTENSIONS | msg.messageType == certificateRequest then TLS_CERTIFICATE_REQ | msg.messageType == certificate then TLS_CERTIFICATE @@ -324,7 +332,8 @@ testParameters = { retry = False, client_auth = False, no_client_cert = False, - zero_rtt = False + zero_rtt = False, + early_ccs = False } testConnection : connection @@ -340,7 +349,10 @@ testConnection = { key_exchange_eph = False, client_auth_flag = False, actual_protocol_version = 0x22, - no_client_cert = True + no_client_cert = True, + early_data_state = zero, + chosen_psk_null = True, + quic_enabled = False } type Character = [8] @@ -361,7 +373,6 @@ s2nToWords action = name # [ '(', action.writer, ')'] | action.record_type == TLS_APPLICATION_DATA then padded "Data" | action.message_type == TLS_CLIENT_HELLO then padded "ClientHello" | action.message_type == TLS_SERVER_HELLO then padded "ServerHello" - | action.message_type == TLS_HELLO_RETRY_REQUEST then padded "HelloRetryRequest" | action.message_type == TLS_ENCRYPTED_EXTENSIONS then padded "EncryptedExtensions" | action.message_type == TLS_CERTIFICATE_REQ then padded "CertRequest" | action.message_type == TLS_CERTIFICATE then padded "Cert" diff --git a/tests/saw/spec/handshake/s2n_handshake_io.cry b/tests/saw/spec/handshake/s2n_handshake_io.cry index 81335bf4b6b..d2219af6e36 100644 --- a/tests/saw/spec/handshake/s2n_handshake_io.cry +++ b/tests/saw/spec/handshake/s2n_handshake_io.cry @@ -7,7 +7,17 @@ module s2n_handshake_io where // This function models the update of the s2n_connection struct by the // s2n_conn_set_handshake_type function in s2n. conn_set_handshake_type : connection -> connection -conn_set_handshake_type conn = conn' +conn_set_handshake_type conn = + if IS_TLS13_HANDSHAKE conn + then conn_set_tls13_handshake_type conn + else conn_set_pre_tls13_handshake_type conn + +// This function models the update of the s2n_connection struct by the +// s2n_conn_set_handshake_type function in s2n. This only models the +// pre-TLS 1.3 code path; see conn_set_tls13_handshake_type for a model of the +// TLS 1.3 code path. +conn_set_pre_tls13_handshake_type : connection -> connection +conn_set_pre_tls13_handshake_type conn = conn' where conn' = {handshake = handshake' ,mode = conn.mode ,corked_io = conn.corked_io @@ -19,6 +29,9 @@ conn_set_handshake_type conn = conn' ,client_auth_flag = conn.client_auth_flag ,actual_protocol_version = conn.actual_protocol_version ,no_client_cert = conn.no_client_cert + ,early_data_state = conn.early_data_state + ,chosen_psk_null = conn.chosen_psk_null + ,quic_enabled = conn.quic_enabled } (handshake' : handshake) = {handshake_type = handshake_type' ,message_number = conn.handshake.message_number @@ -27,19 +40,56 @@ conn_set_handshake_type conn = conn' (if (full_handshake != 0) then perfect_forward_secrecy || ocsp_status || client_auth else zero) - full_handshake = if (conn.is_caching_enabled /\ ~conn.resume_from_cache /\ ~IS_TLS13_HANDSHAKE conn) + full_handshake = if (conn.is_caching_enabled /\ ~conn.resume_from_cache) then zero else FULL_HANDSHAKE - perfect_forward_secrecy = if (conn.key_exchange_eph /\ ~IS_TLS13_HANDSHAKE conn) + perfect_forward_secrecy = if conn.key_exchange_eph then PERFECT_FORWARD_SECRECY else zero - ocsp_status = if (conn.server_can_send_ocsp /\ ~IS_TLS13_HANDSHAKE conn) + ocsp_status = if conn.server_can_send_ocsp then OCSP_STATUS else zero client_auth = if conn.client_auth_flag then CLIENT_AUTH else zero +// This function models the update of the s2n_connection struct by the +// s2n_conn_set_tls13_handshake_type function in s2n. +conn_set_tls13_handshake_type : connection -> connection +conn_set_tls13_handshake_type conn = conn' + where conn' = {handshake = handshake' + ,mode = conn.mode + ,corked_io = conn.corked_io + ,corked = conn.corked + ,is_caching_enabled = conn.is_caching_enabled + ,resume_from_cache = conn.resume_from_cache + ,server_can_send_ocsp = conn.server_can_send_ocsp + ,key_exchange_eph = conn.key_exchange_eph + ,client_auth_flag = conn.client_auth_flag + ,actual_protocol_version = conn.actual_protocol_version + ,no_client_cert = conn.no_client_cert + ,early_data_state = conn.early_data_state + ,chosen_psk_null = conn.chosen_psk_null + ,quic_enabled = conn.quic_enabled + } + (handshake' : handshake) = {handshake_type = handshake_type' + ,message_number = conn.handshake.message_number + } + handshake_type' = (conn.handshake.handshake_type && (HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)) + || NEGOTIATED || full_handshake || with_early_data || client_auth || middlebox_compat + full_handshake = if conn.chosen_psk_null + then FULL_HANDSHAKE + else zero + with_early_data = if conn.early_data_state == S2N_EARLY_DATA_ACCEPTED + then WITH_EARLY_DATA + else zero + client_auth = if conn.client_auth_flag /\ (full_handshake != 0) + then CLIENT_AUTH + else zero + middlebox_compat = if conn.quic_enabled + then zero + else MIDDLEBOX_COMPAT + // This function models the update of the s2n_connection struct by the // s2n_advance_message function in s2n. advance_message : connection -> connection @@ -55,6 +105,9 @@ advance_message conn = conn2 ,client_auth_flag = conn.client_auth_flag ,actual_protocol_version = conn.actual_protocol_version ,no_client_cert = conn.no_client_cert + ,early_data_state = conn.early_data_state + ,chosen_psk_null = conn.chosen_psk_null + ,quic_enabled = conn.quic_enabled } (handshake2 : handshake) = { handshake_type = conn.handshake.handshake_type, message_number = message_number2 } @@ -81,6 +134,9 @@ conn_set_handshake_no_client_cert conn = conn2 ,client_auth_flag = conn.client_auth_flag ,actual_protocol_version = conn.actual_protocol_version ,no_client_cert = conn.no_client_cert + ,early_data_state = conn.early_data_state + ,chosen_psk_null = conn.chosen_psk_null + ,quic_enabled = conn.quic_enabled } (handshake' : handshake) = {handshake_type = handshake_type' ,message_number = conn.handshake.message_number @@ -156,12 +212,18 @@ type connection = {handshake : handshake ,client_auth_flag : Bit //whether the server will request client cert ,actual_protocol_version : [8] ,no_client_cert : Bit + ,early_data_state : [32] + ,chosen_psk_null : Bit + ,quic_enabled : Bit } type handshake = {handshake_type : [32] ,message_number : [32] } +type S2N_HANDSHAKES_COUNT = 256 +type S2N_MAX_HANDSHAKE_LENGTH = 32 + // functions model the corresponding macros in C IS_TLS13_HANDSHAKE : connection -> Bit @@ -170,7 +232,7 @@ IS_TLS13_HANDSHAKE conn = conn.actual_protocol_version == S2N_TLS13 ACTIVE_STATE_MACHINE : connection -> [20]handshake_action ACTIVE_STATE_MACHINE conn = if IS_TLS13_HANDSHAKE conn then tls13_state_machine else state_machine # zero -ACTIVE_HANDSHAKES : connection -> [256][32][32] +ACTIVE_HANDSHAKES : connection -> [S2N_HANDSHAKES_COUNT][S2N_MAX_HANDSHAKE_LENGTH][32] ACTIVE_HANDSHAKES conn = if IS_TLS13_HANDSHAKE conn then tls13_handshakes else handshakes ACTIVE_MESSAGE : connection -> [32] @@ -218,14 +280,16 @@ tls13_state_machine_fn : [5] -> handshake_action tls13_state_machine_fn m = if m == CLIENT_HELLO then mkAct TLS_HANDSHAKE TLS_CLIENT_HELLO 'C' else if m == SERVER_HELLO then mkAct TLS_HANDSHAKE TLS_SERVER_HELLO 'S' + else if m == HELLO_RETRY_MSG then mkAct TLS_HANDSHAKE TLS_SERVER_HELLO 'S' else if m == ENCRYPTED_EXTENSIONS then mkAct TLS_HANDSHAKE TLS_ENCRYPTED_EXTENSIONS 'S' - else if m == SERVER_CERT then mkAct TLS_HANDSHAKE TLS_CERTIFICATE 'S' else if m == SERVER_CERT_REQ then mkAct TLS_HANDSHAKE TLS_CERTIFICATE_REQ 'S' + else if m == SERVER_CERT then mkAct TLS_HANDSHAKE TLS_CERTIFICATE 'S' else if m == SERVER_CERT_VERIFY then mkAct TLS_HANDSHAKE TLS_CERT_VERIFY 'S' else if m == SERVER_FINISHED then mkAct TLS_HANDSHAKE TLS_FINISHED 'S' else if m == CLIENT_CERT then mkAct TLS_HANDSHAKE TLS_CERTIFICATE 'C' else if m == CLIENT_CERT_VERIFY then mkAct TLS_HANDSHAKE TLS_CERT_VERIFY 'C' else if m == CLIENT_FINISHED then mkAct TLS_HANDSHAKE TLS_FINISHED 'C' + else if m == END_OF_EARLY_DATA then mkAct TLS_HANDSHAKE TLS_END_OF_EARLY_DATA 'C' else if m == CLIENT_CHANGE_CIPHER_SPEC then mkAct TLS_CHANGE_CIPHER_SPEC 0 'C' else if m == SERVER_CHANGE_CIPHER_SPEC then mkAct TLS_CHANGE_CIPHER_SPEC 0 'S' else if m == APPLICATION_DATA then mkAct TLS_APPLICATION_DATA 0 'B' @@ -257,35 +321,218 @@ state_machine_fn m = else zero // A model of the tls1.3 handshake state machine (array handshakes in C) -tls13_handshakes : [256][32][32] +tls13_handshakes : [S2N_HANDSHAKES_COUNT][S2N_MAX_HANDSHAKE_LENGTH][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] tls13_handshakes_fn handshk = - if handshk == INITIAL then [CLIENT_HELLO, SERVER_HELLO] # zero - else if handshk == (NEGOTIATED || FULL_HANDSHAKE) then - [ CLIENT_HELLO, - SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, - CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED, - APPLICATION_DATA - ] # zero - else if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH) then - [ CLIENT_HELLO, - SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, - CLIENT_CHANGE_CIPHER_SPEC, CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED, - APPLICATION_DATA - ] # zero - else if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || NO_CLIENT_CERT) then - [ CLIENT_HELLO, - SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT,SERVER_CERT_VERIFY, SERVER_FINISHED, - CLIENT_CHANGE_CIPHER_SPEC, CLIENT_CERT, CLIENT_FINISHED, - APPLICATION_DATA - ] # zero - else zero + if handshk == INITIAL + then [ CLIENT_HELLO, + SERVER_HELLO + ] # zero else + if handshk == (INITIAL || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + SERVER_HELLO + ] # zero else + if handshk == (INITIAL || HELLO_RETRY_REQUEST) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG + ] # zero else + if handshk == (INITIAL || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + HELLO_RETRY_MSG + ] # zero else + if handshk == NEGOTIATED + then [ CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || WITH_EARLY_DATA) + then [ CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + END_OF_EARLY_DATA, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || MIDDLEBOX_COMPAT) + then [ CLIENT_HELLO, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || MIDDLEBOX_COMPAT || WITH_EARLY_DATA) + then [ CLIENT_HELLO, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + CLIENT_CHANGE_CIPHER_SPEC, END_OF_EARLY_DATA, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS || WITH_EARLY_DATA) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + END_OF_EARLY_DATA, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || HELLO_RETRY_REQUEST) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG, + CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC, + CLIENT_CHANGE_CIPHER_SPEC, CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC, + CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE) + then [ CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || MIDDLEBOX_COMPAT) + then [ CLIENT_HELLO, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG, + CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC, + CLIENT_CHANGE_CIPHER_SPEC, CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC, + CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG, + CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || MIDDLEBOX_COMPAT) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC, + CLIENT_CHANGE_CIPHER_SPEC, CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC, + CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || NO_CLIENT_CERT) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG, + CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || NO_CLIENT_CERT || MIDDLEBOX_COMPAT) + then [ CLIENT_HELLO, + HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC, + CLIENT_CHANGE_CIPHER_SPEC, CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || NO_CLIENT_CERT || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC, + CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH) + then [ CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || MIDDLEBOX_COMPAT) + then [ CLIENT_HELLO, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CHANGE_CIPHER_SPEC, CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || NO_CLIENT_CERT) + then [ CLIENT_HELLO, + SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || NO_CLIENT_CERT || MIDDLEBOX_COMPAT) + then [ CLIENT_HELLO, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CHANGE_CIPHER_SPEC, CLIENT_CERT, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || NO_CLIENT_CERT || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS) + then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC, + SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED, + CLIENT_CERT, CLIENT_FINISHED, + APPLICATION_DATA + ] # zero else + zero // A model of the handshake state machine (array handshakes in C) -handshakes : [256][32][32] +handshakes : [S2N_HANDSHAKES_COUNT][S2N_MAX_HANDSHAKE_LENGTH][32] handshakes = [handshakes_fn h | h <- [0..255]] // A function that gives the handshake sequence for each valid handshake_type. @@ -465,9 +712,31 @@ valid_connection conn = valid_handshake (conn.handshake) // Tells if the connection struct is in a valid initial state initial_connection : connection -> Bit -initial_connection conn = conn.handshake.handshake_type == INITIAL /\ conn.handshake.message_number == 0 +initial_connection conn = + conn.handshake.handshake_type < `(S2N_HANDSHAKES_COUNT) + /\ conn.handshake.message_number == 0 /\ (conn.corked == 0 \/ conn.corked == 1) - + + // The assumptions below specifically pertain to TLS 1.3 handshakes. + // Some of the logic that decides which TLS 1.3 handshake types are + // reachable has moved out of the functions that we're verifying, so + // we use the preconditions below instead. Issue + // https://github.com/aws/s2n-tls/issues/3047 is about consolidating + // this logic into the `s2n_conn_set_tls13_handshake_type` function + // instead. + + // If using early data, a full handshake (i.e., chosen_psk being null) + // cannot happen + /\ ((conn.early_data_state == S2N_EARLY_DATA_ACCEPTED) ==> ~conn.chosen_psk_null) + + // HelloRetryRequest and EarlyData cannot both happen simultaneously + /\ ~(((conn.handshake.handshake_type && HELLO_RETRY_REQUEST) != zero) + /\ (conn.early_data_state == S2N_EARLY_DATA_ACCEPTED)) + + // EarlyClientCCS implies MiddleboxCompat + /\ (((conn.handshake.handshake_type && EARLY_CLIENT_CCS) != zero) ==> + ((conn.handshake.handshake_type && MIDDLEBOX_COMPAT) != zero)) + // Logical implication implies : Bit -> Bit -> Bit implies l r = if r then True else ~l @@ -493,6 +762,19 @@ OCSP_STATUS = zero # 0x20 WITH_SESSION_TICKET : [32] WITH_SESSION_TICKET = zero # 0x40 +HELLO_RETRY_REQUEST : [32] +HELLO_RETRY_REQUEST = zero # 0x10 +MIDDLEBOX_COMPAT : [32] +MIDDLEBOX_COMPAT = zero # 0x20 +WITH_EARLY_DATA : [32] +WITH_EARLY_DATA = zero # 0x40 +EARLY_CLIENT_CCS : [32] +EARLY_CLIENT_CCS = zero # 0x80 + +S2N_UNKNOWN_PROTOCOL_VERSION : [8] +S2N_UNKNOWN_PROTOCOL_VERSION = 0 +S2N_TLS12 : [8] +S2N_TLS12 = 33 S2N_TLS13 : [8] S2N_TLS13 = 34 @@ -513,6 +795,8 @@ SERVER_CHANGE_CIPHER_SPEC = 13 SERVER_FINISHED = 14 ENCRYPTED_EXTENSIONS = 15 SERVER_CERT_VERIFY = 16 +HELLO_RETRY_MSG = 17 +END_OF_EARLY_DATA = 18 APPLICATION_DATA = 19 //TLS record type @@ -527,7 +811,6 @@ TLS_CLIENT_HELLO = 1 TLS_SERVER_HELLO = 2 TLS_END_OF_EARLY_DATA = 5 TLS_SERVER_NEW_SESSION_TICKET = 4 -TLS_HELLO_RETRY_REQUEST = 6 TLS_ENCRYPTED_EXTENSIONS = 8 TLS_CERTIFICATE = 11 TLS_SERVER_KEY = 12 @@ -540,3 +823,10 @@ TLS_CERTIFICATE_STATUS = 22 S2N_SERVER = 0 S2N_CLIENT = 1 + +//S2N cert auth types +S2N_CERT_AUTH_NONE = 0 +S2N_CERT_AUTH_REQUIRED = 1 + +//S2N early data states +S2N_EARLY_DATA_ACCEPTED = 3 diff --git a/tls/Makefile b/tls/Makefile index 7b39e33e231..4b8ab38588c 100644 --- a/tls/Makefile +++ b/tls/Makefile @@ -19,7 +19,7 @@ SUB_BUILDS = $(patsubst %/Makefile, %, $(wildcard */Makefile)) BITCODE_DIR?=../tests/saw/bitcode/ -BCS_1=s2n_handshake_io.bc s2n_handshake_type.bc s2n_connection.bc s2n_kex.bc +BCS_1=s2n_handshake_io.bc s2n_handshake_type.bc s2n_connection.bc s2n_kex.bc s2n_tls13.bc s2n_quic_support.bc BCS=$(addprefix $(BITCODE_DIR), $(BCS_1)) .PHONY : all @@ -46,4 +46,4 @@ indent: indentsource clean: decruft $(foreach subfolder, $(SUB_BUILDS), ${MAKE} -C $(subfolder) decruft) -include ../s2n.mk \ No newline at end of file +include ../s2n.mk