diff --git a/stuffer/s2n_stuffer.c b/stuffer/s2n_stuffer.c index 32a9acb9299..6e6814cd54a 100644 --- a/stuffer/s2n_stuffer.c +++ b/stuffer/s2n_stuffer.c @@ -432,3 +432,15 @@ int s2n_stuffer_extract_blob(struct s2n_stuffer *stuffer, struct s2n_blob *out) POSIX_POSTCONDITION(s2n_blob_validate(out)); return S2N_SUCCESS; } + +int s2n_stuffer_shift(struct s2n_stuffer *stuffer) +{ + POSIX_ENSURE_REF(stuffer); + struct s2n_stuffer copy = *stuffer; + POSIX_GUARD(s2n_stuffer_rewrite(©)); + uint8_t *data = stuffer->blob.data + stuffer->read_cursor; + uint32_t data_size = s2n_stuffer_data_available(stuffer); + POSIX_GUARD(s2n_stuffer_write_bytes(©, data, data_size)); + *stuffer = copy; + return S2N_SUCCESS; +} diff --git a/stuffer/s2n_stuffer.h b/stuffer/s2n_stuffer.h index 0758626b144..33acc471f0d 100644 --- a/stuffer/s2n_stuffer.h +++ b/stuffer/s2n_stuffer.h @@ -82,6 +82,7 @@ int S2N_RESULT_MUST_USE s2n_stuffer_resize_if_empty(struct s2n_stuffer *stuffer, int S2N_RESULT_MUST_USE s2n_stuffer_rewind_read(struct s2n_stuffer *stuffer, const uint32_t size); int S2N_RESULT_MUST_USE s2n_stuffer_reread(struct s2n_stuffer *stuffer); int S2N_RESULT_MUST_USE s2n_stuffer_rewrite(struct s2n_stuffer *stuffer); +int S2N_RESULT_MUST_USE s2n_stuffer_shift(struct s2n_stuffer *stuffer); int s2n_stuffer_wipe(struct s2n_stuffer *stuffer); int s2n_stuffer_wipe_n(struct s2n_stuffer *stuffer, const uint32_t n); bool s2n_stuffer_is_consumed(struct s2n_stuffer *stuffer); diff --git a/tests/cbmc/proofs/s2n_stuffer_shift/Makefile b/tests/cbmc/proofs/s2n_stuffer_shift/Makefile new file mode 100644 index 00000000000..b744029ce30 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_shift/Makefile @@ -0,0 +1,41 @@ +# +# +# 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. + +# Expected runtime is 10 seconds. + +MAX_BLOB_SIZE = 20 +DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE) + +CBMCFLAGS += + +PROOF_UID = s2n_stuffer_shift +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)/memmove_simple.c + +PROJECT_SOURCES += $(SRCDIR)/error/s2n_errno.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 += memmove_impl.0:$(call addone,$(MAX_BLOB_SIZE)) +UNWINDSET += memmove_impl.1:$(call addone,$(MAX_BLOB_SIZE)) + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_shift/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_shift/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_shift/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_shift/s2n_stuffer_shift_harness.c b/tests/cbmc/proofs/s2n_stuffer_shift/s2n_stuffer_shift_harness.c new file mode 100644 index 00000000000..a499d7ff53c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_shift/s2n_stuffer_shift_harness.c @@ -0,0 +1,46 @@ +/* + * Copyright 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_shift_harness() +{ + struct s2n_stuffer *stuffer = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(stuffer))); + __CPROVER_assume(s2n_blob_is_bounded(&stuffer->blob, MAX_BLOB_SIZE)); + + /* Save previous state from stuffer. */ + struct s2n_stuffer old_stuffer = *stuffer; + uint32_t shift = old_stuffer.read_cursor; + struct store_byte_from_buffer old_byte = { 0 }; + save_byte_from_blob(&old_stuffer.blob, &old_byte); + __CPROVER_assume(old_byte.idx >= old_stuffer.read_cursor); + __CPROVER_assume(old_byte.idx < old_stuffer.write_cursor); + + int result = s2n_stuffer_shift(stuffer); + assert(s2n_result_is_ok(s2n_stuffer_validate(stuffer))); + + if (result == S2N_SUCCESS) { + old_byte.idx -= shift; + old_stuffer.write_cursor -= shift; + old_stuffer.read_cursor = 0; + } + assert_stuffer_equivalence(stuffer, &old_stuffer, &old_byte); +} diff --git a/tests/cbmc/stubs/memmove_simple.c b/tests/cbmc/stubs/memmove_simple.c new file mode 100644 index 00000000000..612f3cd9beb --- /dev/null +++ b/tests/cbmc/stubs/memmove_simple.c @@ -0,0 +1,65 @@ +/* + * Copyright 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. + */ + +#undef memmove + +#include +#include +#include +#include + +/** + * CBMC can struggle to model memmove. + * If a proof needs real memmove behavior without paying its high cost, + * that proof can use this simple looping based solution. + */ +void *memmove_impl(void *dest, const void *src, size_t n) { + __CPROVER_HIDE:; + if (n > 0) { + assert(dest); + assert(src); + } + + uint8_t *dest_bytes = (uint8_t*) dest; + uint8_t *src_bytes = (uint8_t*) src; + + /* src and dst can overlap, so we need to save a copy of src + * in case modifying dst modifies src */ + uint8_t *src_copy = malloc(n); + if (src_copy == NULL) { + return NULL; + } + for (size_t i = 0; i < n; i++) { + src_copy[i] = src_bytes[i]; + } + + for (size_t i = 0; i < n; i++) { + dest_bytes[i] = src_copy[i]; + } + + free(src_copy); + return dest; +} + +void *memmove(void *dest, const void *src, size_t n) { + __CPROVER_HIDE:; + return memmove_impl(dest, src, n); +} + +void *__builtin___memmove_chk(void *dest, const void *src, size_t n, size_t size) { + __CPROVER_HIDE:; + (void)size; + return memmove_impl(dest, src, n); +} diff --git a/tests/unit/s2n_stuffer_test.c b/tests/unit/s2n_stuffer_test.c index 415ae2f3193..daeda686117 100644 --- a/tests/unit/s2n_stuffer_test.c +++ b/tests/unit/s2n_stuffer_test.c @@ -240,5 +240,107 @@ int main(int argc, char **argv) } }; + /* Test s2n_stuffer_shift */ + { + /* Safety */ + EXPECT_FAILURE_WITH_ERRNO(s2n_stuffer_shift(NULL), S2N_ERR_NULL); + + const uint8_t test_data[] = "hello world"; + const uint32_t test_data_size = sizeof(test_data); + const uint32_t test_offset = 10; + + /* Uninitialized stuffer: no shift */ + { + struct s2n_stuffer test = { 0 }; + + EXPECT_SUCCESS(s2n_stuffer_shift(&test)); + EXPECT_EQUAL(test.read_cursor, 0); + EXPECT_EQUAL(test.write_cursor, 0); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), 0); + } + + /* No data available: no shift */ + { + uint8_t data[100] = { 0 }; + struct s2n_stuffer test = { 0 }; + EXPECT_SUCCESS(s2n_blob_init(&test.blob, data, sizeof(data))); + + EXPECT_SUCCESS(s2n_stuffer_write_bytes(&test, test_data, sizeof(test_data))); + EXPECT_SUCCESS(s2n_stuffer_skip_read(&test, sizeof(test_data))); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), 0); + + EXPECT_SUCCESS(s2n_stuffer_shift(&test)); + EXPECT_EQUAL(test.read_cursor, 0); + EXPECT_EQUAL(test.write_cursor, 0); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), 0); + EXPECT_BYTEARRAY_EQUAL(data, test_data, sizeof(test_data)); + } + + /* Data not offset: no shift */ + { + uint8_t data[100] = { 0 }; + struct s2n_stuffer test = { 0 }; + EXPECT_SUCCESS(s2n_blob_init(&test.blob, data, sizeof(data))); + + EXPECT_SUCCESS(s2n_stuffer_write_bytes(&test, test_data, test_data_size)); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), test_data_size); + + EXPECT_SUCCESS(s2n_stuffer_shift(&test)); + EXPECT_EQUAL(test.read_cursor, 0); + EXPECT_EQUAL(test.write_cursor, test_data_size); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), test_data_size); + EXPECT_BYTEARRAY_EQUAL(data, test_data, test_data_size); + } + + /* Data at offset: shifted */ + { + uint8_t data[100] = { 0 }; + struct s2n_stuffer test = { 0 }; + EXPECT_SUCCESS(s2n_blob_init(&test.blob, data, sizeof(data))); + + EXPECT_SUCCESS(s2n_stuffer_skip_write(&test, test_offset)); + EXPECT_SUCCESS(s2n_stuffer_skip_read(&test, test_offset)); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), 0); + EXPECT_SUCCESS(s2n_stuffer_write_bytes(&test, test_data, test_data_size)); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), test_data_size); + + EXPECT_SUCCESS(s2n_stuffer_shift(&test)); + EXPECT_EQUAL(test.read_cursor, 0); + EXPECT_EQUAL(test.write_cursor, test_data_size); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), test_data_size); + EXPECT_BYTEARRAY_EQUAL(data, test_data, test_data_size); + } + + /* Data overlaps: shifted */ + { + uint8_t data[100] = { 0 }; + struct s2n_stuffer test = { 0 }; + EXPECT_SUCCESS(s2n_blob_init(&test.blob, data, sizeof(data))); + + /* Allocate data large enough that it will overlap when shifted. + * Allocate the entire block to distinctive data, not just all one character. + */ + uint8_t overlap_test_data[sizeof(data) - 1] = { 0 }; + for (size_t i = 0; i < sizeof(overlap_test_data); i++) { + overlap_test_data[i] = i; + } + size_t overlap_test_data_size = sizeof(overlap_test_data); + EXPECT_TRUE(overlap_test_data_size > sizeof(data) / 2); + + EXPECT_SUCCESS(s2n_stuffer_skip_write(&test, 1)); + EXPECT_SUCCESS(s2n_stuffer_skip_read(&test, 1)); + EXPECT_SUCCESS(s2n_stuffer_write_bytes(&test, + overlap_test_data, overlap_test_data_size)); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), overlap_test_data_size); + EXPECT_EQUAL(s2n_stuffer_space_remaining(&test), 0); + + EXPECT_SUCCESS(s2n_stuffer_shift(&test)); + EXPECT_EQUAL(test.read_cursor, 0); + EXPECT_EQUAL(test.write_cursor, overlap_test_data_size); + EXPECT_EQUAL(s2n_stuffer_data_available(&test), overlap_test_data_size); + EXPECT_BYTEARRAY_EQUAL(data, overlap_test_data, overlap_test_data_size); + } + } + END_TEST(); }