Re-enable TLS 1.3 SAW tests

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 =

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,11 @@ 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;
+    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 +81,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 ();
 };

tests/saw/spec/handshake/handshake_io_lowlevel.saw

@@ -64,13 +64,12 @@ 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
@@ -98,22 +97,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,16 +174,31 @@ 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);
 
    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 +216,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 +289,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 +320,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 +349,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)