////////////////////////////////////////////////////////////////
// Copyright 2019 Galois, Inc. All Rights Reserved
//
// Licensed under the Apache License, Version 2.0 (the "License").
// You may not use this file except in compliance with the License.
// A copy of the License is located at
//
//  http://aws.amazon.com/apache2.0
//
// or in the "license" file accompanying this file. This file is distributed
// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
// express or implied. See the License for the specific language governing
// permissions and limitations under the License.
//
////////////////////////////////////////////////////////////////
//
// This file describes the correspondence between the Cryptol
// specification of the TLS handshake and the C code in
// tls/s2n_handshake_io.c, allowing SAW to prove that the code
// corresponds to the specification.
//
////////////////////////////////////////////////////////////////


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";

llvm <- llvm_load_module "../../bitcode/all_llvm.bc";
print "Loaded bitcode via Crucible";

////////////////////////////////////////////////////////////////
// References to various components of the connection state:
// The Cryptol definitions are located in the s2n_handshake_io.cry file.
// Those Cryptol definitions will be compared against the actual C
// definitions by this SAW script.
////////////////////////////////////////////////////////////////

//conn->mode
let conn_mode pconn = crucible_field pconn "mode";

let secure_crypto_params pconn = crucible_field pconn "secure";

//conn->secure->cipher_suite->key_exchange_alg->flags
let conn_secure_cipher_suite crypto_params = crucible_field crypto_params "cipher_suite";

//let key_exchange_algorithm csuite = crucible_elem csuite 3;
let key_exchange_algorithm csuite = crucible_field csuite "key_exchange_alg";

let kea_is_ephemeral kea = crucible_elem kea 0;
//let kea_is_ephemeral kea = crucible_field kea "is_ephemeral";

//conn->status_type
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";

let {{
// Convert a Bit to a length-1 bitvector.
bit_to_bv1 : Bit -> [1]
bit_to_bv1 b = [b]

// Convert a length-1 bitvector to a Bit.
bv1_to_bit : [1] -> Bit
bv1_to_bit bv1 = bv1 @ 0
}};

//conn->session_ticket_status
let conn_session_ticket_status pconn = (crucible_field pconn "session_ticket_status");

//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";

//conn->handshake.message_number
let conn_handshake_message_number pconn =
    crucible_field (crucible_field pconn "handshake") "message_number";

//conn->handshake.state_machine
let conn_handshake_state_machine pconn =
    crucible_field (crucible_field pconn "handshake") "state_machine";

//conn->handshake_params.our_chain_and_key
let conn_chain_and_key pconn =
    crucible_field (crucible_field pconn "handshake_params") "our_chain_and_key";

//conn->psk_params.chosen_psk
let conn_chosen_psk pconn =
    crucible_field (crucible_field pconn "psk_params") "chosen_psk";

//conn->early_data_state
let conn_early_data_state pconn = crucible_field pconn "early_data_state";

// Ghost state that represents the number of times the connection write socket
// has been corked/uncorked. 
corked <- crucible_declare_ghost_state "corked";
crucible_ghost_value corked {{ 0 : [2] }};

// setup_handshake_common de-serializes parts of the s2n_handshake and
// s2n_connection structs into a Cryptol record. It also deserializes the ghost
// state. We use the suffix "_common" since it captures the properties shared
// in common between setup_connection and setup_psk_connection.
//
// The chosen_psk_null argument is true if conn->psk_params.chosen_psk should
// be set to NULL, which enables the use of FULL_HANDSHAKE if TLS 1.3 is used.
// If false, then chosen_psk is set to a non-NULL value, disabling
// FULL_HANDSHAKE if TLS 1.3 is used. The value of conn->psk_params.chosen_psk
// has no effect if TLS 1.2 is used.
let setup_connection_common chosen_psk_null = do {
   pconn <- crucible_alloc (llvm_struct "struct.s2n_connection");
   
   version <- crucible_fresh_var "version" (llvm_int 8);
   crucible_precond {{ version != S2N_UNKNOWN_PROTOCOL_VERSION /\ version <= S2N_TLS13 }};
   crucible_points_to (crucible_field pconn "actual_protocol_version") (crucible_term version);
   
   mode <- crucible_fresh_var "mode" (llvm_int 32);
   crucible_points_to (conn_mode pconn) (crucible_term mode);
   
   handshake_type <- crucible_fresh_var "handshake_type" (llvm_int 32);
   crucible_points_to (conn_handshake_handshake_type pconn)
                      (crucible_term handshake_type); 

   message_number <- crucible_fresh_var "message_number" (llvm_int 32);
   crucible_points_to (conn_handshake_message_number pconn)
                      (crucible_term message_number);

   state_machine <- crucible_fresh_var "state_machine" (llvm_int 32);
   crucible_points_to (conn_handshake_state_machine pconn)
   (crucible_term state_machine);

   cork_val <- crucible_fresh_var "corked" (llvm_int 2);
   crucible_ghost_value corked cork_val;

   // We assume that the client_cert_auth_type_overridden flag 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.
   cca_ov <- crucible_fresh_var "cca_ov" (llvm_int 8);
   crucible_points_to (cca_type_ov pconn) (crucible_term cca_ov);
   crucible_equal (crucible_term cca_ov) (crucible_term {{1 : [8]}});

   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;

   cipher_suite <- crucible_alloc (llvm_struct "struct.s2n_cipher_suite");
   crucible_points_to (conn_secure_cipher_suite secure) cipher_suite;

   kea <- crucible_alloc (llvm_struct "struct.s2n_kex");
   crucible_points_to (key_exchange_algorithm cipher_suite) kea;

   eph_flag <- crucible_fresh_var "eph_flag" (llvm_int 8);
   crucible_points_to (kea_is_ephemeral kea) (crucible_term eph_flag);

   config <- crucible_alloc (llvm_struct "struct.s2n_config");
   crucible_points_to (conn_config pconn) config;

   cak <- crucible_alloc (llvm_struct "struct.s2n_cert_chain_and_key");
   crucible_points_to (conn_chain_and_key pconn) cak;

   status_size <- crucible_fresh_var "status_size" (llvm_int 32);
   crucible_points_to (ocsp_status_size cak) (crucible_term status_size);
   crucible_equal (crucible_term status_size) (crucible_term {{zero : [32]}});

   // We assume that corking/uncorking is managed by s2n, so set the corked_io
   // bit in s2n_connection to one...
   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...
   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...
   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.
   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);

   ocsp_flag <- crucible_fresh_var "ocsp_flag" (llvm_int 32);
   crucible_points_to (conn_status_type pconn) (crucible_term ocsp_flag);

   if chosen_psk_null
      then crucible_points_to (conn_chosen_psk pconn) crucible_null
      else do { chosen_psk <- crucible_alloc (llvm_struct "struct.s2n_psk");
                crucible_points_to (conn_chosen_psk pconn) chosen_psk;
              };
   let chosen_psk_null_bit = if chosen_psk_null then {{ True }} else {{ False }};

   early_data_state <- crucible_fresh_var "early_data_state" (llvm_int 32);
   crucible_points_to (conn_early_data_state pconn) (crucible_term early_data_state);

   no_client_cert <- crucible_fresh_var "no_client_cert" (llvm_int 8);

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

   // This returns a connection containing a handshake. If the connection or the handshake
   // definitions are changed, they must also be changed here.
   return (pconn, {{ {corked_io = corked_io
                     ,mode      = mode
                     ,handshake = {message_number = message_number
                                  ,handshake_type = handshake_type
                                  ,state_machine = state_machine }
                     ,corked    = cork_val
                     ,is_caching_enabled = False
                     ,key_exchange_eph = eph_flag != zero
                     ,server_can_send_ocsp =
                            ((ocsp_flag == 1) && (status_size > 0)) ||
                            ((mode == 1) && (ocsp_flag == 1))
                     ,resume_from_cache = False
                     ,client_auth_flag = if mode == S2N_CLIENT then cca == S2N_CERT_AUTH_REQUIRED else
                                         if mode == S2N_SERVER then cca != S2N_CERT_AUTH_NONE     else False
                     ,no_client_cert = no_client_cert != zero
                     ,actual_protocol_version = version
                     ,early_data_state = early_data_state
                     ,chosen_psk_null = chosen_psk_null_bit
                     ,quic_enabled = quic_enabled_bit
                     ,npn_negotiated = npn_negotiated_bit
                     }
                  }}); 
};

// Set conn->psk_params.chosen_psk to NULL, which enables the use of FULL_HANDSHAKE
// if TLS 1.3 is used. Note that if TLS 1.2 is used, there is no difference between
// this function and setup_psk_connection.
let setup_connection = setup_connection_common true;

// Set conn->psk_params.chosen_psk to a non-NULL value, which disables the use of FULL_HANDSHAKE
// if TLS 1.3 is used. Note that if TLS 1.2 is used, there is no difference between
// this function and setup_connection.
let setup_psk_connection = setup_connection_common false;


// This function checks that the values of the state_machine array are what we
// expect. 'state_machine' is the pointer to the beginning of the array, 'index_term' 
// is the term representing the index in the array.
let verify_state_machine_elem state_machine state_machine_model index_term = do {
    let index = eval_int index_term;
    let abstract = {{ state_machine_model @ index_term }};

    crucible_points_to (crucible_elem (crucible_elem state_machine index) 0) (crucible_term {{ abstract.record_type }});

    crucible_points_to (crucible_elem (crucible_elem state_machine index) 1) (crucible_term {{ abstract.message_type }});

    crucible_points_to (crucible_elem (crucible_elem state_machine index) 2) (crucible_term {{ abstract.writer }});

};

// For now axiomitize this is always false and see if we can prove something
let s2n_allowed_to_cache_connection_spec = do {
    pconf <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");

    crucible_execute_func [pconf];
    crucible_return (crucible_term {{ 0 : [32] }});
};

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_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");
    crucible_points_to (conn_config pconn) config;

    config_cca_ov <- llvm_fresh_var "config_cca_ov" (llvm_int 8);
    crucible_points_to (crucible_field config "client_cert_auth_type_overridden") (crucible_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);

    cca <- crucible_fresh_var "cca" (llvm_int 32);
    crucible_points_to (cca_type pconn) (crucible_term cca);

    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
        if config_cca_ov != zero then config_cca 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
// by conn_set_handshake_type (low-level model function)
let s2n_conn_set_handshake_type_spec chosen_psk_null = do {
    (pconn, conn) <- setup_connection_common chosen_psk_null;
    // We assume that the connection struct denotes a valid connection state
    crucible_precond {{ valid_connection conn }};

    // symbolically execute s2n_conn_set_handshake_type
    crucible_execute_func [pconn];

    // Next we check that the changes to s2n_connection fields are
    // simulated by the low-level specification of the function. We do
    // this by running the model function conn_set_handshake_type on the
    // deserealized pre-state of the s2n_connection struct and checking
    // that values of the fields of the resulting struct match the fields
    // of the post-state of the s2n_connection struct. In this case only handshake
    // type should change
    let conn' = {{ conn_set_handshake_type conn }};
    crucible_ghost_value corked {{ conn'.corked }};
    crucible_points_to (conn_handshake_handshake_type pconn) (crucible_term {{ conn'.handshake.handshake_type }});

    // assert that s2n_conn_set_handshake_type returns 0 (true if the 4
    // functions it calls don't fail)
    crucible_return (crucible_term {{ 0 : [32] }});
};

// specification for s2n_advance_message that sets up simulation of it
// by advance_message (low-level model function)
let s2n_advance_message_spec = do {
    // Note that s2n_advance_message() doesn't actually care about the value of
    // chosen_psk, so we arbitrarily set it to NULL here by using
    // setup_connection. Using setup_psk_connection would work just as well.
    (pconn, conn) <- setup_connection;
    // We assume that the connection struct denotes a valid connection state
    crucible_precond {{ valid_connection conn }};

    // symbolically execute s2n_advance_message
    crucible_execute_func [pconn];

    // Next we check that the changes to s2n_connection fields are
    // simulated by the low-level specification of the function. We do
    // this by running the model function advance_message on the
    // deserealized pre-state of the s2n_connection struct and checking
    // that values of the fields of the resulting struct match the fields
    // of the post-state of the s2n_connection struct.
    let conn' = {{ advance_message conn }};
    crucible_ghost_value corked {{ conn'.corked }};
    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 }});

    // make sure the low-level spec representation of the declarative
    // handshake/cork-uncork state machine is equivalent to the one in
    // s2n
    // The Cryptol representations are defined here: tests/saw/spec/handshake/s2n_handshake_io.cry
    //
    // Note that we use crucible_points_to_untyped here rather than
    // crucible_points_to because LLVM 7 and later represent static arrays that
    // are partially initialized with zeroes as packed structs. For more
    // information, see
    // https://llvm.discourse.group/t/array-layout-changed-by-clang-llvm-starting-from-version-7/2271
    //
    // Changing the Cryptol definitions of the state machines to match these
    // new types would be annoying, and moreover, it isn't guaranteed that
    // future versions of LLVM won't change the types further. Fortunately, the
    // in-memory representation of the arrays hasn't changed, just the types.
    // As a result, we can use crucible_points_to_untyped to check if the two
    // state machines are bitwise equivalent without checking the types.
    crucible_points_to_untyped (crucible_global "handshakes") (crucible_term {{ handshakes }});
    crucible_points_to_untyped (crucible_global "tls13_handshakes") (crucible_term {{ tls13_handshakes }});
    
    let messages = [ {{CLIENT_HELLO : [5]}}
                   , {{SERVER_HELLO : [5]}}
                   , {{SERVER_NEW_SESSION_TICKET : [5]}}
                   , {{SERVER_CERT : [5]}}
                   , {{SERVER_CERT_STATUS : [5]}}
                   , {{SERVER_KEY : [5]}}
                   , {{SERVER_CERT_REQ : [5]}}
                   , {{SERVER_HELLO_DONE : [5]}}
                   , {{CLIENT_CERT : [5]}}
                   , {{CLIENT_KEY : [5]}}
                   , {{CLIENT_CERT_VERIFY : [5]}}
                   , {{CLIENT_CHANGE_CIPHER_SPEC : [5]}}
                   , {{CLIENT_NPN : [5]}}
                   , {{CLIENT_FINISHED : [5]}}
                   , {{SERVER_CHANGE_CIPHER_SPEC : [5]}}
                   , {{SERVER_FINISHED : [5]}}
                   , {{ENCRYPTED_EXTENSIONS : [5]}}
                   , {{SERVER_CERT_VERIFY : [5]}}
                   , {{HELLO_RETRY_MSG : [5]}}
                   , {{END_OF_EARLY_DATA : [5]}}
                   , {{APPLICATION_DATA : [5]}}
                   ];

    for messages (verify_state_machine_elem (crucible_global "state_machine") {{ state_machine }} );
    for messages (verify_state_machine_elem (crucible_global "tls13_state_machine") {{ tls13_state_machine }} );

    // assert that s2n_advance_message returns 0 (true if the 4
    // functions it calls don't fail)
    crucible_return (crucible_term {{ 0 : [32] }});
};

// Specs for the 5 functions that s2n_advance_message calls. Right now
// we just assume the specs and don't verify them. That's because we
// don't model the state that they depend on, instead, making assumptions
// about it: we use managed corking and the socket was initially uncorked.

// Specification for s2n_socket_write_uncork. The relevant part is
// that it decrements the 'corked' ghost variable to indicate that the socket
// has been uncorked.
let s2n_socket_write_uncork_spec = do {
    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");
    cork_val <- crucible_fresh_var "corked" (llvm_int 2);
    crucible_ghost_value corked cork_val;

    crucible_execute_func [pconn];

    crucible_ghost_value corked {{ cork_val - 1 }};

    crucible_return (crucible_term {{ 0 : [32] }});
};

// Specification for s2n_generate_new_client_session_id. This is essentially
// a noop function that returns 0 from the perspective of our current proof
let s2n_generate_new_client_session_id_spec = do {
    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");
   
    crucible_execute_func [pconn];

    crucible_return (crucible_term {{ 0 : [32] }});
};

// Specification for s2n_resume_decrypt_session_ticket_spec. This is essentially
// a noop function that returns 0 from the perspective of our current proof
let s2n_resume_decrypt_session_ticket_spec = do {
    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");
    from <- crucible_alloc_readonly (llvm_struct "struct.s2n_stuffer");

    crucible_execute_func [pconn, from];
    crucible_return (crucible_term {{ 0 : [32] }});
};

// Specification for s2n_socket_write_cork. The relevant part is
// that it increments the 'corked' ghost variable to 1 to
// indicate that the socket has been corked.
let s2n_socket_write_cork_spec = do {
    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");

    cork_val <- crucible_fresh_var "corked" (llvm_int 2);
    crucible_ghost_value corked cork_val;

    crucible_execute_func [pconn];

    crucible_ghost_value corked {{ cork_val + 1 }};

    crucible_return (crucible_term {{ 0 : [32] }});
};

// Specification for s2n_socket_was_corked.  We assume this function
// always returns 0 to indicate our assumption that the socket was
// uncorked initially. If it was corked, then the cork/uncork state
// machine would be bypassed, making verification moot.
let s2n_socket_was_corked_spec = do {
    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");

    crucible_execute_func [pconn];

    crucible_return (crucible_term {{ 0 : [32] }});
};


// Specification for s2n_socket_quickack. This is essentially
// a noop function that returns 0 from the perspective of our current proof
let s2n_socket_quickack_spec = do {
    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");

    crucible_execute_func [pconn];

    crucible_return (crucible_term {{ 0 : [32] }});
};


// Specification for s2n_connection_is_managed_corked. We assume it
// always returns 1 to reflect our assumption that the library is
// managing the corking and uncorking of the socket. Otherwise, the
//cork/uncork state machine would be bypassed making verification moot.
let s2n_connection_is_managed_corked_spec = do {
    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");

    crucible_execute_func [pconn];

    crucible_return (crucible_term {{ 1 : [32] }});
};