Fix saw

api/s2n.h

@@ -2202,7 +2202,7 @@ S2N_API extern int s2n_config_set_client_auth_type(struct s2n_config *config, s2
  * @param client_auth_type A pointer to a client auth policy. This will be updated to the s2n_connection value.
  * @returns S2N_SUCCESS on success. S2N_FAILURE on failure
  */
-S2N_API extern int s2n_connection_get_client_auth_type(struct s2n_connection *conn, s2n_cert_auth_type *client_auth_type);
+S2N_API extern int s2n_connection_get_client_auth_type(const struct s2n_connection *conn, s2n_cert_auth_type *client_auth_type);
 
 /**
  * Sets whether or not a Client Certificate should be required to complete the TLS Connection. 

tests/saw/spec/handshake/handshake_io_lowlevel.saw

@@ -65,9 +65,6 @@ let conn_status_type pconn = crucible_field pconn "status_type";
 //conn->config
 let conn_config pconn = crucible_field pconn "config";
 
-//conn->config -> client_cert_auth_type
-let config_cca_type config = (crucible_field config "client_cert_auth_type");
-
 //conn->handshake_params.our_chain_and_key->ocsp_status.size
 let ocsp_status_size cert_and_key =
     crucible_field (crucible_field (cert_and_key) "ocsp_status") "size";
@@ -88,9 +85,6 @@ let conn_session_ticket_status pconn = (crucible_field pconn "session_ticket_sta
 //conn->client_cert_auth_type
 let cca_type pconn = crucible_field pconn "client_cert_auth_type";
 
-//conn->client_cert_auth_type_overridden
-let cca_type_ov pconn = crucible_field pconn "client_cert_auth_type_overridden";
-
 //conn->handshake.handshake_type
 let conn_handshake_handshake_type pconn =
     crucible_field (crucible_field pconn "handshake") "handshake_type";
@@ -154,11 +148,8 @@ let setup_connection_common chosen_psk_null = do {
    cork_val <- crucible_fresh_var "corked" (llvm_int 2);
    crucible_ghost_value corked cork_val;
 
-   cca_ov <- crucible_fresh_var "cca_ov" (llvm_int 8);
-   crucible_points_to (cca_type_ov pconn) (crucible_term cca_ov);
-
-   cca <- crucible_fresh_var "cca" (llvm_int 32);
-   crucible_points_to (cca_type pconn) (crucible_term cca);
+   client_auth <- crucible_fresh_var "client_auth" (llvm_int 32);
+   crucible_points_to (cca_type pconn) (crucible_term client_auth);
 
    secure <- crucible_alloc (llvm_struct "struct.s2n_crypto_parameters");
    crucible_points_to (secure_crypto_params pconn) secure;
@@ -175,9 +166,6 @@ let setup_connection_common chosen_psk_null = do {
    config <- crucible_alloc (llvm_struct "struct.s2n_config");
    crucible_points_to (conn_config pconn) config;
 
-   config_cca <- crucible_fresh_var "config_cca" (llvm_int 32);
-   crucible_points_to (config_cca_type config) (crucible_term config_cca);
-
    cak <- crucible_alloc (llvm_struct "struct.s2n_cert_chain_and_key");
    crucible_points_to (conn_chain_and_key pconn) cak;
 
@@ -207,6 +195,12 @@ let setup_connection_common chosen_psk_null = do {
    config_quic_enabled <- llvm_fresh_var "config_quic_enabled" (llvm_int 1);
    llvm_points_to_bitfield config "quic_enabled" (llvm_term config_quic_enabled);
    let quic_enabled_bit = {{ bv1_to_bit conn_quic_enabled \/ bv1_to_bit config_quic_enabled }};
+
+   // We assume that the client_cert_auth_type_overridden bit in s2n_connection is set.
+   // If that flag is not set, auth_type / "cca_type" could be determined by the config
+   // or just set to a default value. Since we're primarily interested in the handshake
+   // here and the end result is the same, just consider the connection auth_type.
+   llvm_points_to_bitfield pconn "client_cert_auth_type_overridden" (llvm_term {{ 1 : [1] }});
 
    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);
@@ -226,8 +220,6 @@ let setup_connection_common chosen_psk_null = do {
 
    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 }};
-
    npn_negotiated <- llvm_fresh_var "npn_negotiated" (llvm_int 1);
    llvm_points_to_bitfield pconn "npn_negotiated" (llvm_term npn_negotiated);
    let npn_negotiated_bit = {{ bv1_to_bit npn_negotiated }};
@@ -246,8 +238,8 @@ let setup_connection_common chosen_psk_null = 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 == S2N_CERT_AUTH_REQUIRED else
-                                         if mode == S2N_SERVER then client_cert_auth_type != S2N_CERT_AUTH_NONE     else False
+                     ,client_auth_flag = if mode == S2N_CLIENT then client_auth == S2N_CERT_AUTH_REQUIRED else
+                                         if mode == S2N_SERVER then client_auth != S2N_CERT_AUTH_NONE     else False
                      ,no_client_cert = no_client_cert != zero
                      ,actual_protocol_version = version
                      ,early_data_state = early_data_state
@@ -292,30 +284,38 @@ let s2n_allowed_to_cache_connection_spec = do {
     crucible_return (crucible_term {{ 0 : [32] }});
 };
 
-
-let s2n_connection_get_client_auth_type_spec = do{
-
-    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");
+let s2n_connection_get_client_auth_type_spec = do {
+    pconn <- crucible_alloc (llvm_struct "struct.s2n_connection");
     auth_type <- crucible_alloc (llvm_int 32);
 
-    cca_ov <- crucible_fresh_var "cca_ov" (llvm_int 8);
-    crucible_points_to (cca_type_ov pconn) (crucible_term cca_ov);
-
-    config <- crucible_alloc_readonly (llvm_struct "struct.s2n_config");
+    config <- crucible_alloc (llvm_struct "struct.s2n_config");
     crucible_points_to (conn_config pconn) config;
+
+    conn_auth_type <- crucible_fresh_var "conn_auth_type" (llvm_int 32);
+    crucible_points_to (cca_type pconn) (crucible_term conn_auth_type);
 
-    config_cca <- crucible_fresh_var "config_cca" (llvm_int 32);
-    crucible_points_to (config_cca_type config) (crucible_term config_cca);
-
-    cca <- crucible_fresh_var "cca" (llvm_int 32);
-    crucible_points_to (cca_type pconn) (crucible_term cca);
+    config_auth_type <- crucible_fresh_var "config_auth_type" (llvm_int 32);
+    crucible_points_to (crucible_field config "client_cert_auth_type") (crucible_term config_auth_type);
+
+    conn_override <- llvm_fresh_var "conn_override" (llvm_int 1);
+    llvm_points_to_bitfield pconn "client_cert_auth_type_overridden" (llvm_term conn_override);
+
+    config_override <- llvm_fresh_var "config_override" (llvm_int 1);
+    llvm_points_to_bitfield config "client_cert_auth_type_overridden" (llvm_term config_override);
+
+    mode <- crucible_fresh_var "mode" (llvm_int 32);
+    crucible_points_to (conn_mode pconn) (crucible_term mode);
 
     crucible_execute_func [pconn, auth_type];
 
-    crucible_points_to (auth_type) (crucible_term {{if cca_ov != zero then cca else config_cca}});
+    crucible_points_to (auth_type) (crucible_term {{
+        if bv1_to_bit conn_override then conn_auth_type else
+        if bv1_to_bit config_override then config_auth_type else
+        if mode == S2N_CLIENT then S2N_CERT_AUTH_OPTIONAL else
+        S2N_CERT_AUTH_NONE
+    }});
 
     crucible_return (crucible_term {{ 0 : [32] }});
-
 };
 
 // Specification for s2n_conn_set_handshake_type that sets up simulation of it

tests/saw/spec/handshake/s2n_handshake_io.cry

@@ -1112,6 +1112,7 @@ S2N_CLIENT = 1
 //S2N cert auth types
 S2N_CERT_AUTH_NONE = 0
 S2N_CERT_AUTH_REQUIRED = 1
+S2N_CERT_AUTH_OPTIONAL = 2
 
 //S2N early data states
 S2N_EARLY_DATA_ACCEPTED = 3

tls/s2n_config.c

@@ -410,8 +410,8 @@ int s2n_config_get_client_auth_type(struct s2n_config *config, s2n_cert_auth_typ
 int s2n_config_set_client_auth_type(struct s2n_config *config, s2n_cert_auth_type client_auth_type)
 {
     POSIX_ENSURE_REF(config);
-    config->client_cert_auth_type = client_auth_type;
     config->client_cert_auth_type_overridden = true;
+    config->client_cert_auth_type = client_auth_type;
     return 0;
 }
 

tls/s2n_connection.c

@@ -59,8 +59,8 @@
 #define S2N_SET_KEY_SHARE_LIST_EMPTY(keyshares) (keyshares |= 1)
 #define S2N_SET_KEY_SHARE_REQUEST(keyshares, i) (keyshares |= (1 << (i + 1)))
 
-static S2N_RESULT s2n_connection_and_config_get_client_auth_type(struct s2n_connection *conn,
-        struct s2n_config *config, s2n_cert_auth_type *client_cert_auth_type);
+static S2N_RESULT s2n_connection_and_config_get_client_auth_type(const struct s2n_connection *conn,
+        const struct s2n_config *config, s2n_cert_auth_type *client_cert_auth_type);
 
 /* Allocates and initializes memory for a new connection.
  *
@@ -748,8 +748,8 @@ int s2n_connection_get_protocol_preferences(struct s2n_connection *conn, struct
     return 0;
 }
 
-static S2N_RESULT s2n_connection_and_config_get_client_auth_type(struct s2n_connection *conn,
-        struct s2n_config *config, s2n_cert_auth_type *client_cert_auth_type)
+static S2N_RESULT s2n_connection_and_config_get_client_auth_type(const struct s2n_connection *conn,
+        const struct s2n_config *config, s2n_cert_auth_type *client_cert_auth_type)
 {
     RESULT_ENSURE_REF(conn);
     RESULT_ENSURE_REF(config);
@@ -772,7 +772,7 @@ static S2N_RESULT s2n_connection_and_config_get_client_auth_type(struct s2n_conn
     return S2N_RESULT_OK;
 }
 
-int s2n_connection_get_client_auth_type(struct s2n_connection *conn,
+int s2n_connection_get_client_auth_type(const struct s2n_connection *conn,
         s2n_cert_auth_type *client_cert_auth_type)
 {
     POSIX_ENSURE_REF(conn);
@@ -783,7 +783,7 @@ int s2n_connection_get_client_auth_type(struct s2n_connection *conn,
 
 int s2n_connection_set_client_auth_type(struct s2n_connection *conn, s2n_cert_auth_type client_cert_auth_type)
 {
-    conn->client_cert_auth_type_overridden = 1;
+    conn->client_cert_auth_type_overridden = true;
     conn->client_cert_auth_type = client_cert_auth_type;
     return 0;
 }

tls/s2n_connection.h

@@ -133,6 +133,15 @@ struct s2n_connection {
     /* Indicates whether the connection should request OCSP stapling from the peer */
     unsigned request_ocsp_status : 1;
 
+    /* Whether to use client_cert_auth_type stored in s2n_config or in this s2n_connection.
+     *
+     * By default the s2n_connection will defer to s2n_config->client_cert_auth_type
+     * on whether or not to use Client Auth. But users can override Client Auth
+     * at the connection level using s2n_connection_set_client_auth_type() without
+     * mutating s2n_config since s2n_config can be shared between multiple s2n_connections.
+     */
+    unsigned client_cert_auth_type_overridden : 1;
+
     /* The configuration (cert, key .. etc ) */
     struct s2n_config *config;
 
@@ -224,15 +233,8 @@ struct s2n_connection {
     /* The PRF needs some storage elements to work with */
     struct s2n_prf_working_space *prf_space;
 
-    /* Whether to use client_cert_auth_type stored in s2n_config or in this s2n_connection.
-     *
-     * By default the s2n_connection will defer to s2n_config->client_cert_auth_type on whether or not to use Client Auth.
-     * But users can override Client Auth at the connection level using s2n_connection_set_client_auth_type() without mutating
-     * s2n_config since s2n_config can be shared between multiple s2n_connections. */
-    uint8_t client_cert_auth_type_overridden;
-
-    /* Whether or not the s2n_connection should require the Client to authenticate itself to the server. Only used if
-     * client_cert_auth_type_overridden is non-zero. */
+    /* Whether or not the s2n_connection should require the Client to authenticate itself to the server.
+     * Only used if client_cert_auth_type_overridden is true. */
     s2n_cert_auth_type client_cert_auth_type;
 
     /* Our workhorse stuffers, used for buffering the plaintext
@@ -420,7 +422,7 @@ int s2n_connection_get_signature_preferences(struct s2n_connection *conn, const
 int s2n_connection_get_ecc_preferences(struct s2n_connection *conn, const struct s2n_ecc_preferences **ecc_preferences);
 int s2n_connection_get_protocol_preferences(struct s2n_connection *conn, struct s2n_blob **protocol_preferences);
 int s2n_connection_set_client_auth_type(struct s2n_connection *conn, s2n_cert_auth_type cert_auth_type);
-int s2n_connection_get_client_auth_type(struct s2n_connection *conn, s2n_cert_auth_type *client_cert_auth_type);
+int s2n_connection_get_client_auth_type(const struct s2n_connection *conn, s2n_cert_auth_type *client_cert_auth_type);
 int s2n_connection_get_client_cert_chain(struct s2n_connection *conn, uint8_t **der_cert_chain_out, uint32_t *cert_chain_len);
 int s2n_connection_get_peer_cert_chain(const struct s2n_connection *conn, struct s2n_cert_chain_and_key *cert_chain_and_key);
 uint8_t s2n_connection_get_protocol_version(const struct s2n_connection *conn);