From b73f783781c4594257fb6c321546c1f3dbb21631 Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Wed, 31 Jan 2024 14:21:14 -0800 Subject: [PATCH] Fix saw --- api/s2n.h | 2 +- .../spec/handshake/handshake_io_lowlevel.saw | 66 +++++++++---------- tests/saw/spec/handshake/s2n_handshake_io.cry | 1 + tls/s2n_config.c | 2 +- tls/s2n_connection.c | 12 ++-- tls/s2n_connection.h | 22 ++++--- 6 files changed, 54 insertions(+), 51 deletions(-) diff --git a/api/s2n.h b/api/s2n.h index 6bce51c0342..109febdbf50 100644 --- a/api/s2n.h +++ b/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. diff --git a/tests/saw/spec/handshake/handshake_io_lowlevel.saw b/tests/saw/spec/handshake/handshake_io_lowlevel.saw index 90b6ad2aecd..d7a7d910eb1 100644 --- a/tests/saw/spec/handshake/handshake_io_lowlevel.saw +++ b/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 diff --git a/tests/saw/spec/handshake/s2n_handshake_io.cry b/tests/saw/spec/handshake/s2n_handshake_io.cry index 46fe869ddd3..91faf76f05a 100644 --- a/tests/saw/spec/handshake/s2n_handshake_io.cry +++ b/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 diff --git a/tls/s2n_config.c b/tls/s2n_config.c index 9a64ed8db1d..24b5b132d06 100644 --- a/tls/s2n_config.c +++ b/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; } diff --git a/tls/s2n_connection.c b/tls/s2n_connection.c index 0c11e34716e..6bcb88640d3 100644 --- a/tls/s2n_connection.c +++ b/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; } diff --git a/tls/s2n_connection.h b/tls/s2n_connection.h index 1f8c735f127..0cb46050219 100644 --- a/tls/s2n_connection.h +++ b/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);