Skip to content

Commit

Permalink
Use llvm_points_to_bitfield in SAW proofs (#3155)
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@RyanGlScott
RyanGlScott authored Jan 29, 2022
1 parent 99049d5 commit 7f1017e
Show file tree
Hide file tree
Showing 5 changed files with 59 additions and 104 deletions.
2 changes: 1 addition & 1 deletion codebuild/bin/install_saw.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
41 changes: 32 additions & 9 deletions tests/saw/spec/handshake/handshake.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand All @@ -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";

Expand All @@ -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
Expand All @@ -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 ();
};
98 changes: 26 additions & 72 deletions tests/saw/spec/handshake/handshake_io_lowlevel.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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 }});
Expand Down
11 changes: 0 additions & 11 deletions tls/s2n_config.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
11 changes: 0 additions & 11 deletions tls/s2n_connection.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand All @@ -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;

Expand Down

0 comments on commit 7f1017e

Please sign in to comment.