From 7f02f8e82c5b24c77abe1aa7f16f057eada915ac Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Wed, 31 Jan 2024 14:21:14 -0800 Subject: [PATCH] Fix saw --- .../spec/handshake/handshake_io_lowlevel.saw | 48 ++++++++++--------- tls/s2n_config.c | 2 +- tls/s2n_connection.c | 2 +- tls/s2n_connection.h | 20 ++++---- 4 files changed, 39 insertions(+), 33 deletions(-) diff --git a/tests/saw/spec/handshake/handshake_io_lowlevel.saw b/tests/saw/spec/handshake/handshake_io_lowlevel.saw index 90b6ad2aecd..aba6a7734b1 100644 --- a/tests/saw/spec/handshake/handshake_io_lowlevel.saw +++ b/tests/saw/spec/handshake/handshake_io_lowlevel.saw @@ -68,6 +68,9 @@ 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->config->client_cert_auth_type_overridden +let config_cca_type_ov config = (crucible_field config "client_cert_auth_type_overridden"); + //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"; @@ -154,12 +157,6 @@ 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); - secure <- crucible_alloc (llvm_struct "struct.s2n_crypto_parameters"); crucible_points_to (secure_crypto_params pconn) secure; @@ -175,9 +172,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; @@ -226,7 +220,7 @@ 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 }}; + let client_cert_auth_type = s2n_connection_get_client_auth_type pconn config; npn_negotiated <- llvm_fresh_var "npn_negotiated" (llvm_int 1); llvm_points_to_bitfield pconn "npn_negotiated" (llvm_term npn_negotiated); @@ -293,29 +287,39 @@ let s2n_allowed_to_cache_connection_spec = do { }; -let s2n_connection_get_client_auth_type_spec = do{ +let s2n_connection_get_client_auth_type pconn config = do { + conn_cca_ov <- llvm_fresh_var "conn_cca_ov" (llvm_int 1); + llvm_points_to_bitfield pconn "client_cert_auth_type_overridden" (llvm_term conn_cca_ov); - pconn <- crucible_alloc_readonly (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); + conn_cca <- crucible_fresh_var "conn_cca" (llvm_int 32); + crucible_points_to (cca_type pconn) (crucible_term conn_cca); - config <- crucible_alloc_readonly (llvm_struct "struct.s2n_config"); - crucible_points_to (conn_config pconn) config; + config_cca_ov <- llvm_fresh_var "config_cca_ov" (llvm_int 1); + llvm_points_to_bitfield pconn "client_cert_auth_type_overridden" (llvm_term config_cca_ov); config_cca <- crucible_fresh_var "config_cca" (llvm_int 32); crucible_points_to (config_cca_type config) (crucible_term config_cca); + + let default_cca = {{ if mode == S2N_CLIENT then S2N_CERT_AUTH_OPTIONAL else S2N_CERT_AUTH_NONE }}; + let expected_cca = {{ if cca_ov != 0 then cca + else if config_cca_ov != 0 then config_cca + else default_cca }}; + return expected_cca; +}; + +let s2n_connection_get_client_auth_type_spec = do { + pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection"); + auth_type <- crucible_alloc (llvm_int 32); - cca <- crucible_fresh_var "cca" (llvm_int 32); - crucible_points_to (cca_type pconn) (crucible_term cca); + config <- crucible_alloc_readonly (llvm_struct "struct.s2n_config"); + crucible_points_to (conn_config pconn) config; crucible_execute_func [pconn, auth_type]; - crucible_points_to (auth_type) (crucible_term {{if cca_ov != zero then cca else config_cca}}); + let expected_cca = s2n_connection_get_client_auth_type pconn config; + crucible_points_to (auth_type) (crucible_term expected_cca); crucible_return (crucible_term {{ 0 : [32] }}); - }; // Specification for s2n_conn_set_handshake_type that sets up simulation of it diff --git a/tls/s2n_config.c b/tls/s2n_config.c index 1a181e840d9..3fdfebedf4a 100644 --- a/tls/s2n_config.c +++ b/tls/s2n_config.c @@ -403,8 +403,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 c2238cfe06a..9d1f0e2e7f5 100644 --- a/tls/s2n_connection.c +++ b/tls/s2n_connection.c @@ -777,7 +777,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..bc1a5b3278e 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