1 /* 2 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. 3 * 4 * Licensed under the Apache License, Version 2.0 (the "License"). 5 * You may not use this file except in compliance with the License. 6 * A copy of the License is located at 7 * 8 * http://aws.amazon.com/apache2.0 9 * 10 * or in the "license" file accompanying this file. This file is distributed 11 * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either 12 * express or implied. See the License for the specific language governing 13 * permissions and limitations under the License. 14 */ 15 16 #include "crypto/s2n_fips.h" 17 #include "crypto/s2n_hash.h" 18 19 #include <cbmc_proof/make_common_datastructures.h> 20 s2n_hash_free_harness()21void s2n_hash_free_harness() 22 { 23 /* Non-deterministic inputs. */ 24 struct s2n_hash_state *state = cbmc_allocate_s2n_hash_state(); 25 26 /* Assumptions. */ 27 __CPROVER_assume(s2n_result_is_ok(s2n_hash_state_validate(state))); 28 29 struct rc_keys_from_hash_state saved_hash_state; 30 save_rc_keys_from_hash_state(state, &saved_hash_state); 31 32 /* Operation under verification. */ 33 assert(s2n_hash_free(state) == S2N_SUCCESS); 34 if (state != NULL) { 35 assert(state->hash_impl->free != NULL); 36 if (s2n_is_in_fips_mode()) { 37 assert(state->digest.high_level.evp.ctx == NULL); 38 assert(state->digest.high_level.evp_md5_secondary.ctx == NULL); 39 assert_rc_decrement_on_hash_state(&saved_hash_state); 40 } else { 41 assert_rc_unchanged_on_hash_state(&saved_hash_state); 42 } 43 assert(state->is_ready_for_input == 0); 44 } 45 46 /* Cleanup after expected error cases, for memory leak check. */ 47 if (state != NULL) { 48 /* 1. `free` leftover EVP_MD_CTX objects if `s2n_is_in_fips_mode`, 49 since `s2n_hash_free` is a NO-OP in that case. */ 50 if (!s2n_is_in_fips_mode()) { 51 S2N_EVP_MD_CTX_FREE(state->digest.high_level.evp.ctx); 52 S2N_EVP_MD_CTX_FREE(state->digest.high_level.evp_md5_secondary.ctx); 53 } 54 55 /* 2. `free` leftover reference-counted keys (i.e. those with non-zero ref-count), 56 since they are not automatically `free`d until their ref count reaches 0. */ 57 free_rc_keys_from_hash_state(&saved_hash_state); 58 } 59 /* 3. free our heap-allocated `state` since `s2n_hash_free` only `free`s the contents. */ 60 free(state); 61 } 62