From 7f1017ee9b09ab6910f1d2bf56135663ca0b12c5 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 28 Jan 2022 20:06:22 -0500 Subject: [PATCH] Use `llvm_points_to_bitfield` in SAW proofs (#3155) This uses SAW's new `llvm_points_to_bitfield` command (introduced in GaloisInc/saw-script#1539) to simplify specifications that involve the bitfields in `s2n_config` and `s2n_connection`. In particular, there is no longer any need to manually compute the size of the bitfields or the indices of the fields within the bitfields, as these details are handled automatically by `llvm_points_to_bitfield`. The positions of the fields within bitfields are also no longer important. --- codebuild/bin/install_saw.sh | 2 +- tests/saw/spec/handshake/handshake.saw | 41 ++++++-- .../spec/handshake/handshake_io_lowlevel.saw | 98 +++++-------------- tls/s2n_config.h | 11 --- tls/s2n_connection.h | 11 --- 5 files changed, 59 insertions(+), 104 deletions(-) diff --git a/codebuild/bin/install_saw.sh b/codebuild/bin/install_saw.sh index 0834fb0ca43..a1cff08e82e 100755 --- a/codebuild/bin/install_saw.sh +++ b/codebuild/bin/install_saw.sh @@ -37,7 +37,7 @@ mkdir -p "$DOWNLOAD_DIR" cd "$DOWNLOAD_DIR" #download saw binaries -curl --retry 3 https://s2n-public-test-dependencies.s3-us-west-2.amazonaws.com/saw-0.6.0.99-2020-10-12-Ubuntu14.04-64.tar.gz --output saw.tar.gz +curl --retry 3 https://s2n-public-test-dependencies.s3.us-west-2.amazonaws.com/saw-0.9.0.99-Linux-x86_64.tar.gz --output saw.tar.gz mkdir -p saw && tar -xzf saw.tar.gz --strip-components=1 -C saw mkdir -p "$INSTALL_DIR" && mv saw/* "$INSTALL_DIR" diff --git a/tests/saw/spec/handshake/handshake.saw b/tests/saw/spec/handshake/handshake.saw index 2ebe7d3fdb9..42982e944c5 100644 --- a/tests/saw/spec/handshake/handshake.saw +++ b/tests/saw/spec/handshake/handshake.saw @@ -24,6 +24,10 @@ // //////////////////////////////////////////////////////////////////////////// +// WARNING: handshake_io_lowlevel.saw enables lax_loads_and_stores, which is +// currently only supported by SAW's What4 backend. As a result, all of the +// llvm_verify commands in this file use What4-based tactics (e.g., w4_unint_z3) +// rather than SBV-based tactics (e.g., sbv_unint_z3 or z3). include "handshake_io_lowlevel.saw"; import "rfc_handshake_tls12.cry"; import "rfc_handshake_tls13.cry"; @@ -39,6 +43,13 @@ 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))"; // Low-level handshake_io correspondence proof +// +// WARNING: Because `enable_lax_loads_and_stores` is enabled in this module, +// these proofs must use What4-based proof tactics (i.e., those with a `w4_` +// prefix). Otherwise, they will fail, likely with an error message to the +// effect of: +// +// FOTArray unimplemented for backend let prove_handshake_io_lowlevel = do { print "Beginning the low-level spec equivalence proof"; @@ -63,9 +74,9 @@ let prove_handshake_io_lowlevel = do { let dependencies = [s2n_socket_write_uncork, s2n_socket_write_cork, s2n_socket_was_corked, s2n_connection_is_managed_corked, s2n_socket_quickack]; print "Proving correctness of get_auth_type"; - 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;}); + 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); (w4_unint_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; + s2n_advance_message_proof <- crucible_llvm_verify llvm "s2n_advance_message" dependencies false s2n_advance_message_spec (w4_unint_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 @@ -76,34 +87,46 @@ let prove_handshake_io_lowlevel = do { // 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; + 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) (w4_unint_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; + 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) (w4_unint_yices []); print "Done: Verified that the low-level specification corresponds to the C code"; return (); }; +// WARNING: Because `enable_lax_loads_and_stores` is enabled in this module, +// these proofs must use What4-based proof tactics (i.e., those with a `w4_` +// prefix). Otherwise, they will fail, likely with an error message to the +// effect of: +// +// FOTArray unimplemented for backend let prove_state_machine = do { print "Checking proof that the TLS1.2 RFC simulates our Cryptol s2n spec"; - prove_print abc {{ tls12rfcSimulatesS2N `{16} }}; + prove_print (w4_unint_z3 []) {{ tls12rfcSimulatesS2N `{16} }}; print "Checking proof that the TLS1.3 RFC simulates our Cryptol s2n spec"; - prove_print z3 {{ tls13rfcSimulatesS2N `{16} }}; + prove_print (w4_unint_z3 []) {{ tls13rfcSimulatesS2N `{16} }}; return (); }; +// WARNING: Because `enable_lax_loads_and_stores` is enabled in this module, +// these proofs must use What4-based proof tactics (i.e., those with a `w4_` +// prefix). Otherwise, they will fail, likely with an error message to the +// effect of: +// +// FOTArray unimplemented for backend let prove_cork_uncork = do { print "Verifying the low-level->high-level cork-uncork simulation"; - prove_print z3 {{ highLevelSimulatesLowLevel `{16} }}; + prove_print (w4_unint_z3 []) {{ highLevelSimulatesLowLevel `{16} }}; print "Verifying that double uncorking or corking cannot occur in server mode"; - prove_print z3 {{ noDoubleCorkUncork `{16} }}; + prove_print (w4_unint_z3 []) {{ noDoubleCorkUncork `{16} }}; print "Expecting failure when proving low-high simulation without the server mode assumption"; - sat z3 {{ ~highLevelDoesNotSimulateLowLevel `{16} }}; + sat (w4_unint_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 aa2127caac1..dd8799d2d06 100644 --- a/tests/saw/spec/handshake/handshake_io_lowlevel.saw +++ b/tests/saw/spec/handshake/handshake_io_lowlevel.saw @@ -21,6 +21,16 @@ // //////////////////////////////////////////////////////////////// + +enable_experimental; +// lax_loads_and_stores is needed to support the uses of +// llvm_points_to_bitfield in the specifications below. As a result, SAW will +// return fresh, symbolic values when it reads from uninitialized memory. Make +// sure all of the arguments are initialized in the preconditions of a +// specification, or else SAW will fill them in with underconstrained symbolic +// values! +enable_lax_loads_and_stores; + // Low level specifications for some of the functions and constants declared in // tls/s2n_handshake_io.c import "s2n_handshake_io.cry"; @@ -61,59 +71,14 @@ 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"; -// At the moment, we care about the following fields that are located in -// bitfields: -// -// * conn->corked_io -// * conn->client_session_resumed -// * conn->quic_enabled -// * conn->config->use_tickets -// * conn->config->quic_enabled -// -// We currently handle this by initializing the entirety of each bitfield with -// a symbolic value and imposing appropriate preconditions on them. See the -// comments in setup_connection_common next to conn_bitfield and -// config_bitfield for more details about these preconditions. - -// It's also noteworthy that we use 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, 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 conn_bitfield pconn = (crucible_elem pconn 0); -let config_bitfield config = (crucible_elem config 0); - -// These represent the amount of memory that LLVM will use to represent the -// bitfields in s2n_connection and s2n_config, respectively. The size is -// determined by counting the number of fields in the bitfield and rounding -// up to the nearest power of 2. -let conn_bitfield_size = 32; -let config_bitfield_size = 16; - let {{ -// The position (0-indexed) of each field of interest in -// s2n_connection's bitfield. -conn_corked_io_index : [conn_bitfield_size] -conn_corked_io_index = 0 - -conn_client_session_resumed_index : [conn_bitfield_size] -conn_client_session_resumed_index = 1 - -conn_quic_enabled_index : [conn_bitfield_size] -conn_quic_enabled_index = 2 - -// The position (0-indexed) of each field of interest in -// s2n_config's bitfield. -config_use_tickets_index : [config_bitfield_size] -config_use_tickets_index = 0 - -config_quic_enabled_index : [config_bitfield_size] -config_quic_enabled_index = 1 +// Convert a Bit to a length-1 bitvector. +bit_to_bv1 : Bit -> [1] +bit_to_bv1 b = [b] -// Check if a field at a particular index in a bitfield is set. -bitfield_is_set : {n} (fin n, n >= 1) => [n] -> [n] -> Bit -bitfield_is_set bitfield field_index = (bitfield && (1 << field_index)) != zero +// Convert a length-1 bitvector to a Bit. +bv1_to_bit : [1] -> Bit +bv1_to_bit bv1 = bv1 @ 0 }}; //conn->session_ticket_status @@ -208,37 +173,28 @@ let setup_connection_common chosen_psk_null = do { crucible_points_to (ocsp_status_size cak) (crucible_term status_size); crucible_equal (crucible_term status_size) (crucible_term {{zero : [32]}}); - // Here, we initialize two bitfields: one in s2n_connection (conn_bitfield) - // and the other in s2n_config (config_bitfield). We start by initializing - // the entirety of each bitfield with a symbolic value of the appropriate - // size... - conn_bitfield_value <- crucible_fresh_var "conn_bitfield" (llvm_int conn_bitfield_size); - crucible_points_to_untyped (conn_bitfield pconn) (crucible_term conn_bitfield_value); - config_bitfield_value <- crucible_fresh_var "config_bitfield" (llvm_int config_bitfield_size); - crucible_points_to_untyped (config_bitfield config) (crucible_term config_bitfield_value); - - // ...next, we impose preconditions on these symbolic values as appropriate. - // // We assume that corking/uncorking is managed by s2n, so set the corked_io // bit in s2n_connection to one... - let corked_io = {{ bitfield_is_set conn_bitfield_value conn_corked_io_index : Bit }}; - crucible_precond corked_io; + let corked_io = {{ True }}; + llvm_points_to_bitfield pconn "corked_io" (llvm_term {{ bit_to_bv1 corked_io }}); // ...we assume that the client_session_resumed bit in s2n_connection must // be zero... - crucible_precond {{ ~(bitfield_is_set conn_bitfield_value conn_client_session_resumed_index) }}; + llvm_points_to_bitfield pconn "client_session_resumed" (llvm_term {{ 0 : [1] }}); // ...we currently require that the use_tickets bit in s2n_config must be // zero... - crucible_precond {{ ~(bitfield_is_set config_bitfield_value config_use_tickets_index) }}; + llvm_points_to_bitfield config "use_tickets" (llvm_term {{ 0 : [1] }}); // ...on the other hand, the quic_enabled bits in both s2n_connection and // s2n_config are allowed to be either 0 or 1. As such, we don't need to // impose any direct constraints on them. We simply query which values // they have taken on during simulation and remember them for later. - let quic_enabled_bit = {{ bitfield_is_set conn_bitfield_value conn_quic_enabled_index - \/ bitfield_is_set config_bitfield_value config_quic_enabled_index - }}; + conn_quic_enabled <- llvm_fresh_var "conn_quic_enabled" (llvm_int 1); + llvm_points_to_bitfield pconn "quic_enabled" (llvm_term conn_quic_enabled); + 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 }}; 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); @@ -397,9 +353,7 @@ let s2n_advance_message_spec = do { // of the post-state of the s2n_connection struct. let conn' = {{ advance_message conn }}; crucible_ghost_value corked {{ conn'.corked }}; - conn_bitfield_post <- crucible_fresh_var "conn_bitfield_post" (llvm_int conn_bitfield_size); - crucible_points_to_untyped (conn_bitfield pconn) (crucible_term conn_bitfield_post); - crucible_postcond {{ bitfield_is_set conn_bitfield_post conn_corked_io_index == conn'.corked_io }}; + llvm_points_to_bitfield pconn "corked_io" (llvm_term {{ bit_to_bv1 (conn'.corked_io) }}); crucible_points_to (conn_mode pconn) (crucible_term {{ conn'.mode }}); crucible_points_to (conn_handshake_handshake_type pconn) (crucible_term {{ conn'.handshake.handshake_type }}); crucible_points_to (conn_handshake_message_number pconn) (crucible_term {{ conn'.handshake.message_number }}); diff --git a/tls/s2n_config.h b/tls/s2n_config.h index e62d3209602..6091d5b932e 100644 --- a/tls/s2n_config.h +++ b/tls/s2n_config.h @@ -30,23 +30,12 @@ struct s2n_cipher_preferences; struct s2n_config { - /* The following bitfield flags are used in SAW proofs. The positions of - * these flags are important, as SAW looks up each flag by their index - * in the struct starting from 0. See the comments surrounding - * config_bitfield in tests/saw/spec/handshake/handshake_io_lowlevel.saw for - * more details. Make sure that any new flags are added after these ones - * so that the indices in the SAW proofs do not need to be changed each time. - * - * START OF SAW-TRACKED BITFIELD FLAGS */ - unsigned use_tickets:1; /* Whether a connection can be used by a QUIC implementation. * See s2n_quic_support.h */ unsigned quic_enabled:1; - /* END OF SAW-TRACKED BITFIELD FLAGS */ - unsigned cert_allocated:1; unsigned default_certs_are_explicit:1; unsigned use_session_cache:1; diff --git a/tls/s2n_connection.h b/tls/s2n_connection.h index 408cd4b4afa..1672c394578 100644 --- a/tls/s2n_connection.h +++ b/tls/s2n_connection.h @@ -56,15 +56,6 @@ typedef enum { } s2n_session_ticket_status; struct s2n_connection { - /* The following bitfield flags are used in SAW proofs. The positions of - * these flags are important, as SAW looks up each flag by their index - * in the struct starting from 0. See the comments surrounding - * conn_bitfield in tests/saw/spec/handshake/handshake_io_lowlevel.saw for - * more details. Make sure that any new flags are added after these ones - * so that the indices in the SAW proofs do not need to be changed each time. - * - * START OF SAW-TRACKED BITFIELD FLAGS */ - /* Is this connection using CORK/SO_RCVLOWAT optimizations? Only valid when the connection is using * managed_send_io */ @@ -76,8 +67,6 @@ struct s2n_connection { /* Connection can be used by a QUIC implementation */ unsigned quic_enabled:1; - /* END OF SAW-TRACKED BITFIELD FLAGS */ - /* Determines if we're currently sending or receiving in s2n_shutdown */ unsigned close_notify_queued:1;