Merge branch 'aws:main' into cbmc_6_minimal

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

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

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

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

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"

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]

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"
 

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

tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

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 <assert.h>
+#include <cbmc_proof/cbmc_utils.h>
+#include <cbmc_proof/make_common_datastructures.h>
+
+#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);
+}

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

tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

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 <assert.h>
+#include <cbmc_proof/cbmc_utils.h>
+#include <cbmc_proof/make_common_datastructures.h>
+
+#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);
+}

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

tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

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 <assert.h>
+#include <cbmc_proof/cbmc_utils.h>
+#include <cbmc_proof/make_common_datastructures.h>
+
+#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);
+}