Use llvm_points_to_bitfield in SAW proofs

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"

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 ();
 };

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 }});

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;

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;