From b36e5b5924aa5bae6012f2b2331ee84d9779ec18 Mon Sep 17 00:00:00 2001 From: Wesley Rosenblum <55108558+WesleyRosenblum@users.noreply.github.com> Date: Thu, 1 Aug 2024 13:02:35 -0700 Subject: [PATCH 1/3] chore(bindings): release 0.2.10 (#4683) --- bindings/rust/s2n-tls-hyper/Cargo.toml | 5 +++-- bindings/rust/s2n-tls-sys/templates/Cargo.template | 2 +- bindings/rust/s2n-tls-tokio/Cargo.toml | 4 ++-- bindings/rust/s2n-tls/Cargo.toml | 4 ++-- 4 files changed, 8 insertions(+), 7 deletions(-) diff --git a/bindings/rust/s2n-tls-hyper/Cargo.toml b/bindings/rust/s2n-tls-hyper/Cargo.toml index f29f27e0c93..bba1ec7b885 100644 --- a/bindings/rust/s2n-tls-hyper/Cargo.toml +++ b/bindings/rust/s2n-tls-hyper/Cargo.toml @@ -7,13 +7,14 @@ edition = "2021" rust-version = "1.63.0" repository = "https://github.com/aws/s2n-tls" license = "Apache-2.0" +publish = false [features] default = [] [dependencies] -s2n-tls = { version = "=0.2.9", path = "../s2n-tls" } -s2n-tls-tokio = { version = "=0.2.9", path = "../s2n-tls-tokio" } +s2n-tls = { version = "=0.2.10", path = "../s2n-tls" } +s2n-tls-tokio = { version = "=0.2.10", path = "../s2n-tls-tokio" } hyper = { version = "1" } hyper-util = { version = "0.1", features = ["client-legacy", "tokio", "http1"] } tower-service = { version = "0.3" } diff --git a/bindings/rust/s2n-tls-sys/templates/Cargo.template b/bindings/rust/s2n-tls-sys/templates/Cargo.template index 530d50576b4..37ae6bfc870 100644 --- a/bindings/rust/s2n-tls-sys/templates/Cargo.template +++ b/bindings/rust/s2n-tls-sys/templates/Cargo.template @@ -1,7 +1,7 @@ [package] name = "s2n-tls-sys" description = "A C99 implementation of the TLS/SSL protocols" -version = "0.2.9" +version = "0.2.10" authors = ["AWS s2n"] edition = "2021" rust-version = "1.63.0" diff --git a/bindings/rust/s2n-tls-tokio/Cargo.toml b/bindings/rust/s2n-tls-tokio/Cargo.toml index 4783c41c896..d7fd23d96b5 100644 --- a/bindings/rust/s2n-tls-tokio/Cargo.toml +++ b/bindings/rust/s2n-tls-tokio/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "s2n-tls-tokio" description = "An implementation of TLS streams for Tokio built on top of s2n-tls" -version = "0.2.9" +version = "0.2.10" authors = ["AWS s2n"] edition = "2021" rust-version = "1.63.0" @@ -15,7 +15,7 @@ default = [] errno = { version = "0.3" } libc = { version = "0.2" } pin-project-lite = { version = "0.2" } -s2n-tls = { version = "=0.2.9", path = "../s2n-tls" } +s2n-tls = { version = "=0.2.10", path = "../s2n-tls" } tokio = { version = "1", features = ["net", "time"] } [dev-dependencies] diff --git a/bindings/rust/s2n-tls/Cargo.toml b/bindings/rust/s2n-tls/Cargo.toml index e10757cc1e2..ce70bbf6de1 100644 --- a/bindings/rust/s2n-tls/Cargo.toml +++ b/bindings/rust/s2n-tls/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "s2n-tls" description = "A C99 implementation of the TLS/SSL protocols" -version = "0.2.9" +version = "0.2.10" authors = ["AWS s2n"] edition = "2021" rust-version = "1.63.0" @@ -21,7 +21,7 @@ unstable-testing = [] [dependencies] errno = { version = "0.3" } libc = "0.2" -s2n-tls-sys = { version = "=0.2.9", path = "../s2n-tls-sys", features = ["internal"] } +s2n-tls-sys = { version = "=0.2.10", path = "../s2n-tls-sys", features = ["internal"] } pin-project-lite = "0.2" hex = "0.4" From 0685abc65f2e51b09748feb7f6ccbf4836c8422d Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Thu, 1 Aug 2024 22:46:23 -0700 Subject: [PATCH 2/3] fix: don't fail for 0 blinding delay (#4671) --- bin/common.c | 3 +++ bin/s2nc.c | 6 ++++++ bin/s2nd.c | 3 +++ tests/unit/s2n_safety_blinding_test.c | 20 ++++++++++++++++++++ tls/s2n_connection.c | 3 +++ 5 files changed, 35 insertions(+) diff --git a/bin/common.c b/bin/common.c index ff19ace9da6..66c3459f245 100644 --- a/bin/common.c +++ b/bin/common.c @@ -314,6 +314,9 @@ int s2n_setup_external_psk_list(struct s2n_connection *conn, char *psk_optarg_li int s2n_set_common_server_config(int max_early_data, struct s2n_config *config, struct conn_settings conn_settings, const char *cipher_prefs, const char *session_ticket_key_file_path) { + /* The s2n-tls blinding security feature is disabled for testing purposes to make debugging easier. */ + GUARD_EXIT(s2n_config_set_max_blinding_delay(config, 0), "Error setting blinding delay"); + GUARD_EXIT(s2n_config_set_server_max_early_data_size(config, max_early_data), "Error setting max early data"); GUARD_EXIT(s2n_config_add_dhparams(config, dhparams), "Error adding DH parameters"); diff --git a/bin/s2nc.c b/bin/s2nc.c index d96e094026d..5781948e2e3 100644 --- a/bin/s2nc.c +++ b/bin/s2nc.c @@ -76,6 +76,9 @@ const char default_trusted_cert[] = void usage() { /* clang-format off */ + fprintf(stderr, "s2nc is an s2n-tls client testing utility.\n"); + fprintf(stderr, "It is not intended for production use.\n"); + fprintf(stderr, "\n"); fprintf(stderr, "usage: s2nc [options] host [port]\n"); fprintf(stderr, " host: hostname or IP address to connect to\n"); fprintf(stderr, " port: port to connect to\n"); @@ -201,6 +204,9 @@ static void setup_s2n_config(struct s2n_config *config, const char *cipher_prefs exit(1); } + /* The s2n-tls blinding security feature is disabled for testing purposes to make debugging easier. */ + GUARD_EXIT(s2n_config_set_max_blinding_delay(config, 0), "Error setting blinding delay"); + GUARD_EXIT(s2n_config_set_cipher_preferences(config, cipher_prefs), "Error setting cipher prefs"); GUARD_EXIT(s2n_config_set_status_request_type(config, type), "OCSP validation is not supported by the linked libCrypto implementation. It cannot be set."); diff --git a/bin/s2nd.c b/bin/s2nd.c index 886c50b3e35..77733899e7a 100644 --- a/bin/s2nd.c +++ b/bin/s2nd.c @@ -138,6 +138,9 @@ static char default_private_key[] = void usage() { /* clang-format off */ + fprintf(stderr, "s2nd is an s2n-tls server testing utility.\n"); + fprintf(stderr, "It is not intended for production use.\n"); + fprintf(stderr, "\n"); fprintf(stderr, "usage: s2nd [options] host port\n"); fprintf(stderr, " host: hostname or IP address to listen on\n"); fprintf(stderr, " port: port to listen on\n"); diff --git a/tests/unit/s2n_safety_blinding_test.c b/tests/unit/s2n_safety_blinding_test.c index aab11f28888..15305ea9c00 100644 --- a/tests/unit/s2n_safety_blinding_test.c +++ b/tests/unit/s2n_safety_blinding_test.c @@ -151,6 +151,26 @@ int main(int argc, char **argv) EXPECT_BLINDING(conn); }; + /* Skips blinding if set to 0 */ + { + SETUP_TEST(conn); + s2n_errno = S2N_ERR_UNIMPLEMENTED; + + DEFER_CLEANUP(struct s2n_config *config = s2n_config_new(), s2n_config_ptr_free); + EXPECT_SUCCESS(s2n_connection_set_config(conn, config)); + + /* No blinding delay, but closed connection */ + EXPECT_SUCCESS(s2n_config_set_max_blinding_delay(config, 0)); + EXPECT_OK(s2n_connection_apply_error_blinding(&conn)); + EXPECT_EQUAL(s2n_connection_get_delay(conn), 0); + EXPECT_TRUE(s2n_connection_check_io_status(conn, S2N_IO_CLOSED)); + + /* Any non-zero blinding delay still causes blinding */ + EXPECT_SUCCESS(s2n_config_set_max_blinding_delay(config, 1)); + EXPECT_OK(s2n_connection_apply_error_blinding(&conn)); + EXPECT_BLINDING(conn); + } + EXPECT_SUCCESS(s2n_connection_free(conn)); }; diff --git a/tls/s2n_connection.c b/tls/s2n_connection.c index fa218f9ba7e..1f2d2db8348 100644 --- a/tls/s2n_connection.c +++ b/tls/s2n_connection.c @@ -1238,6 +1238,9 @@ static S2N_RESULT s2n_connection_kill(struct s2n_connection *conn) int64_t min = 0, max = 0; RESULT_GUARD(s2n_connection_calculate_blinding(conn, &min, &max)); + if (max == 0) { + return S2N_RESULT_OK; + } /* Keep track of the delay so that it can be enforced */ uint64_t rand_delay = 0; From aacb0ab373af272e817c0d7e822eef87983fbb9f Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Fri, 2 Aug 2024 00:56:52 -0700 Subject: [PATCH 3/3] test(cbmc): add stuffer hex proofs (#4659) --- .../cbmc/proofs/s2n_stuffer_read_hex/Makefile | 40 ++++++++++ .../s2n_stuffer_read_hex/cbmc-proof.txt | 1 + .../s2n_stuffer_read_hex_harness.c | 65 ++++++++++++++++ .../s2n_stuffer_read_uint16_hex/Makefile | 39 ++++++++++ .../cbmc-proof.txt | 1 + .../s2n_stuffer_read_uint16_hex_harness.c | 44 +++++++++++ .../s2n_stuffer_read_uint8_hex/Makefile | 39 ++++++++++ .../s2n_stuffer_read_uint8_hex/cbmc-proof.txt | 1 + .../s2n_stuffer_read_uint8_hex_harness.c | 44 +++++++++++ .../proofs/s2n_stuffer_write_hex/Makefile | 40 ++++++++++ .../s2n_stuffer_write_hex/cbmc-proof.txt | 1 + .../s2n_stuffer_write_hex_harness.c | 74 +++++++++++++++++++ .../s2n_stuffer_write_uint16_hex/Makefile | 37 ++++++++++ .../cbmc-proof.txt | 1 + .../s2n_stuffer_write_uint16_hex_harness.c | 63 ++++++++++++++++ .../s2n_stuffer_write_uint8_hex/Makefile | 37 ++++++++++ .../cbmc-proof.txt | 1 + .../s2n_stuffer_write_uint8_hex_harness.c | 63 ++++++++++++++++ 18 files changed, 591 insertions(+) create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/s2n_stuffer_read_uint16_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/s2n_stuffer_read_uint8_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_hex/s2n_stuffer_write_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/s2n_stuffer_write_uint16_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/s2n_stuffer_write_uint8_hex_harness.c diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile new file mode 100644 index 00000000000..527e2146b25 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile @@ -0,0 +1,40 @@ +# Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +MAX_BLOB_SIZE = 10 +DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE) + +PROOF_UID = s2n_stuffer_read_hex +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) +PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c +PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c +PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c + +UNWINDSET += s2n_stuffer_read_hex.8:$(MAX_BLOB_SIZE) + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c new file mode 100644 index 00000000000..4051edc30cf --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c @@ -0,0 +1,65 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_read_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *output = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(output))); + + struct s2n_blob *hex_in = cbmc_allocate_s2n_blob(); + __CPROVER_assume(s2n_result_is_ok(s2n_blob_validate(hex_in))); + __CPROVER_assume(s2n_blob_is_bounded(hex_in, MAX_BLOB_SIZE)); + + struct s2n_stuffer old_output = *output; + struct store_byte_from_buffer output_saved_byte = { 0 }; + save_byte_from_blob(&output->blob, &output_saved_byte); + __CPROVER_assume(output_saved_byte.idx < output->write_cursor); + + struct s2n_blob old_hex_in = *hex_in; + struct store_byte_from_buffer old_hex_in_byte = { 0 }; + save_byte_from_blob(hex_in, &old_hex_in_byte); + + s2n_result result = s2n_stuffer_read_hex(output, hex_in); + + struct s2n_stuffer expected_bytes_out = old_output; + struct s2n_blob expected_hex_in = old_hex_in; + + /* On success, the byte equivalent of the hex was written to the stuffer */ + if (s2n_result_is_ok(result)) { + expected_bytes_out.write_cursor += old_hex_in.size / 2; + expected_bytes_out.high_water_mark = MAX(expected_bytes_out.write_cursor, + old_output.high_water_mark); + } + + /* Memory may be allocated on either success or failure, + * because we allocated the memory before we start writing. */ + if (output->blob.size > old_output.blob.size) { + expected_bytes_out.blob = output->blob; + } + + assert(s2n_result_is_ok(s2n_stuffer_validate(output))); + assert_stuffer_equivalence(output, &expected_bytes_out, &output_saved_byte); + assert(s2n_result_is_ok(s2n_blob_validate(hex_in))); + assert_blob_equivalence(hex_in, &expected_hex_in, &old_hex_in_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile new file mode 100644 index 00000000000..1952ae9eb72 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile @@ -0,0 +1,39 @@ +# Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_read_uint16_hex +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) +PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c +PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c +PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c + +REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl + +UNWINDSET += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_read_n_bytes.14:5 + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/s2n_stuffer_read_uint16_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/s2n_stuffer_read_uint16_hex_harness.c new file mode 100644 index 00000000000..97211bbd47e --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/s2n_stuffer_read_uint16_hex_harness.c @@ -0,0 +1,44 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_read_uint16_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_in = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_in))); + + struct s2n_stuffer old_hex_in = *hex_in; + struct store_byte_from_buffer old_byte = { 0 }; + save_byte_from_blob(&hex_in->blob, &old_byte); + + uint16_t out; + s2n_stuffer_read_uint16_hex(hex_in, &out); + + size_t expected_read = 4; + struct s2n_stuffer expected_hex_in = old_hex_in; + if (expected_hex_in.write_cursor >= expected_hex_in.read_cursor + expected_read) { + expected_hex_in.read_cursor += expected_read; + } + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_in))); + assert_stuffer_equivalence(hex_in, &expected_hex_in, &old_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile new file mode 100644 index 00000000000..6c05e6c3fdd --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile @@ -0,0 +1,39 @@ +# Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_read_uint8_hex +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) +PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c +PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c +PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c + +REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl + +UNWINDSET += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_read_n_bytes.14:3 + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/s2n_stuffer_read_uint8_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/s2n_stuffer_read_uint8_hex_harness.c new file mode 100644 index 00000000000..0738499a4f3 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/s2n_stuffer_read_uint8_hex_harness.c @@ -0,0 +1,44 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_read_uint8_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_in = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_in))); + + struct s2n_stuffer old_hex_in = *hex_in; + struct store_byte_from_buffer old_byte = { 0 }; + save_byte_from_blob(&hex_in->blob, &old_byte); + + uint8_t out; + s2n_stuffer_read_uint8_hex(hex_in, &out); + + size_t expected_read = 2; + struct s2n_stuffer expected_hex_in = old_hex_in; + if (expected_hex_in.write_cursor >= expected_hex_in.read_cursor + expected_read) { + expected_hex_in.read_cursor += expected_read; + } + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_in))); + assert_stuffer_equivalence(hex_in, &expected_hex_in, &old_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile new file mode 100644 index 00000000000..a09b7f8a6e8 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile @@ -0,0 +1,40 @@ +# Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +MAX_BLOB_SIZE = 10 +DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE) + +PROOF_UID = s2n_stuffer_write_hex +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) +PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c +PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c +PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c + +UNWINDSET += s2n_stuffer_write_hex.3:$(call addone,$(MAX_BLOB_SIZE)) + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_write_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/s2n_stuffer_write_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_write_hex/s2n_stuffer_write_hex_harness.c new file mode 100644 index 00000000000..6b5bdc20a1c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/s2n_stuffer_write_hex_harness.c @@ -0,0 +1,74 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_write_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_out = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + + struct s2n_blob *bytes_in = cbmc_allocate_s2n_blob(); + __CPROVER_assume(s2n_result_is_ok(s2n_blob_validate(bytes_in))); + __CPROVER_assume(s2n_blob_is_bounded(bytes_in, MAX_BLOB_SIZE - 1)); + + size_t expected_written = bytes_in->size * 2; + size_t test_offset = nondet_size_t(); + __CPROVER_assume(0 <= test_offset); + __CPROVER_assume(test_offset < expected_written); + + struct s2n_stuffer old_hex_out = *hex_out; + struct store_byte_from_buffer old_hex_out_byte = { 0 }; + save_byte_from_blob(&hex_out->blob, &old_hex_out_byte); + __CPROVER_assume(old_hex_out_byte.idx < hex_out->write_cursor); + + struct s2n_blob old_bytes_in = *bytes_in; + struct store_byte_from_buffer old_bytes_in_byte = { 0 }; + save_byte_from_blob(bytes_in, &old_bytes_in_byte); + + s2n_result result = s2n_stuffer_write_hex(hex_out, bytes_in); + + struct s2n_stuffer expected_hex_out = old_hex_out; + struct s2n_blob expected_bytes_in = old_bytes_in; + + if (s2n_result_is_ok(result)) { + /* On success, the hex equivalent of the bytes is written to the stuffer */ + expected_hex_out.write_cursor += expected_written; + expected_hex_out.high_water_mark = MAX(expected_hex_out.write_cursor, + old_hex_out.high_water_mark); + + /* Any new bytes written should match the expected hex pattern */ + uint8_t c = hex_out->blob.data[old_hex_out.write_cursor + test_offset]; + assert(('0' <= c && c <= '9') || ('a' <= c && c <= 'f')); + } + + /* Memory may be allocated on either success or failure, + * because we allocated the memory before we start writing. */ + if (hex_out->blob.size > old_hex_out.blob.size) { + expected_hex_out.blob = hex_out->blob; + } + + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + assert_stuffer_equivalence(hex_out, &expected_hex_out, &old_hex_out_byte); + assert(s2n_result_is_ok(s2n_blob_validate(bytes_in))); + assert_blob_equivalence(bytes_in, &expected_bytes_in, &old_bytes_in_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile new file mode 100644 index 00000000000..255787c81b9 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile @@ -0,0 +1,37 @@ +# Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_write_uint16_hex +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) +PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c +PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c +PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c + +UNWINDSET += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_write_n_bytes.4:5 + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/s2n_stuffer_write_uint16_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/s2n_stuffer_write_uint16_hex_harness.c new file mode 100644 index 00000000000..cf40ee82fae --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/s2n_stuffer_write_uint16_hex_harness.c @@ -0,0 +1,63 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_write_uint16_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_out = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + + struct s2n_stuffer old_hex_out = *hex_out; + struct store_byte_from_buffer old_hex_out_byte = { 0 }; + save_byte_from_blob(&hex_out->blob, &old_hex_out_byte); + __CPROVER_assume(old_hex_out_byte.idx < hex_out->write_cursor); + + uint16_t byte_in = nondet_uint16_t(); + s2n_result result = s2n_stuffer_write_uint16_hex(hex_out, byte_in); + + struct s2n_stuffer expected_hex_out = old_hex_out; + size_t expected_written = 4; + size_t test_offset = nondet_size_t(); + __CPROVER_assume(0 <= test_offset); + __CPROVER_assume(test_offset < expected_written); + + if (s2n_result_is_ok(result)) { + /* On success, the hex equivalent of the bytes is written to the stuffer */ + expected_hex_out.write_cursor += expected_written; + expected_hex_out.high_water_mark = MAX(expected_hex_out.write_cursor, + old_hex_out.high_water_mark); + + /* New bytes written should match the expected hex pattern */ + uint8_t c = hex_out->blob.data[old_hex_out.write_cursor + test_offset]; + assert(('0' <= c && c <= '9') || ('a' <= c && c <= 'f')); + } + + /* Memory may be allocated on either success or failure, + * because we allocated the memory before we start writing. */ + if (hex_out->blob.size > old_hex_out.blob.size) { + expected_hex_out.blob = hex_out->blob; + } + + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + assert_stuffer_equivalence(hex_out, &expected_hex_out, &old_hex_out_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile new file mode 100644 index 00000000000..6a5695128fc --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile @@ -0,0 +1,37 @@ +# Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_write_uint8_hex +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) +PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c +PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c +PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c + +UNWINDSET += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_write_n_bytes.4:3 + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/s2n_stuffer_write_uint8_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/s2n_stuffer_write_uint8_hex_harness.c new file mode 100644 index 00000000000..6d5372cea7c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/s2n_stuffer_write_uint8_hex_harness.c @@ -0,0 +1,63 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. 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. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_write_uint8_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_out = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + + struct s2n_stuffer old_hex_out = *hex_out; + struct store_byte_from_buffer old_hex_out_byte = { 0 }; + save_byte_from_blob(&hex_out->blob, &old_hex_out_byte); + __CPROVER_assume(old_hex_out_byte.idx < hex_out->write_cursor); + + uint8_t byte_in = nondet_uint8_t(); + s2n_result result = s2n_stuffer_write_uint8_hex(hex_out, byte_in); + + struct s2n_stuffer expected_hex_out = old_hex_out; + size_t expected_written = 2; + size_t test_offset = nondet_size_t(); + __CPROVER_assume(0 <= test_offset); + __CPROVER_assume(test_offset < expected_written); + + if (s2n_result_is_ok(result)) { + /* On success, the hex equivalent of the bytes is written to the stuffer */ + expected_hex_out.write_cursor += expected_written; + expected_hex_out.high_water_mark = MAX(expected_hex_out.write_cursor, + old_hex_out.high_water_mark); + + /* New bytes written should match the expected hex pattern */ + uint8_t c = hex_out->blob.data[old_hex_out.write_cursor + test_offset]; + assert(('0' <= c && c <= '9') || ('a' <= c && c <= 'f')); + } + + /* Memory may be allocated on either success or failure, + * because we allocated the memory before we start writing. */ + if (hex_out->blob.size > old_hex_out.blob.size) { + expected_hex_out.blob = hex_out->blob; + } + + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + assert_stuffer_equivalence(hex_out, &expected_hex_out, &old_hex_out_byte); +}