diff --git a/stuffer/s2n_stuffer.c b/stuffer/s2n_stuffer.c index e8d7c883b49..32a9acb9299 100644 --- a/stuffer/s2n_stuffer.c +++ b/stuffer/s2n_stuffer.c @@ -203,14 +203,11 @@ int s2n_stuffer_reread(struct s2n_stuffer *stuffer) int s2n_stuffer_wipe_n(struct s2n_stuffer *stuffer, const uint32_t size) { POSIX_PRECONDITION(s2n_stuffer_validate(stuffer)); - if (size >= stuffer->write_cursor) { - return s2n_stuffer_wipe(stuffer); - } + uint32_t wipe_size = MIN(size, stuffer->write_cursor); - /* We know that size is now less than write_cursor */ - stuffer->write_cursor -= size; - POSIX_CHECKED_MEMSET(stuffer->blob.data + stuffer->write_cursor, S2N_WIPE_PATTERN, size); + stuffer->write_cursor -= wipe_size; stuffer->read_cursor = MIN(stuffer->read_cursor, stuffer->write_cursor); + POSIX_CHECKED_MEMSET(stuffer->blob.data + stuffer->write_cursor, S2N_WIPE_PATTERN, wipe_size); POSIX_POSTCONDITION(s2n_stuffer_validate(stuffer)); return S2N_SUCCESS; diff --git a/stuffer/s2n_stuffer_text.c b/stuffer/s2n_stuffer_text.c index 6a95c9d8f3d..88f6b96b300 100644 --- a/stuffer/s2n_stuffer_text.c +++ b/stuffer/s2n_stuffer_text.c @@ -242,11 +242,12 @@ int s2n_stuffer_vprintf(struct s2n_stuffer *stuffer, const char *format, va_list */ int str_len = vsnprintf(NULL, 0, format, vargs_1.va_list); POSIX_ENSURE_GTE(str_len, 0); + POSIX_ENSURE_LT(str_len, INT_MAX); int mem_size = str_len + 1; /* 'tainted' indicates that pointers to the contents of the stuffer exist, * so resizing / reallocated the stuffer will invalidate those pointers. - * However, we do no resize the stuffer in this method after creating `str` + * However, we do not resize the stuffer in this method after creating `str` * and `str` does not live beyond this method, so ignore `str` for the * purposes of tracking 'tainted'. */ @@ -261,7 +262,11 @@ int s2n_stuffer_vprintf(struct s2n_stuffer *stuffer, const char *format, va_list /* This time, vsnprintf actually writes the formatted string */ int written = vsnprintf(str, mem_size, format, vargs_2.va_list); - POSIX_ENSURE_GTE(written, 0); + if (written != str_len) { + /* If the write fails, undo our raw write */ + POSIX_GUARD(s2n_stuffer_wipe_n(stuffer, mem_size)); + POSIX_BAIL(S2N_ERR_SAFETY); + } /* We don't actually use c-strings, so erase the final '\0' */ POSIX_GUARD(s2n_stuffer_wipe_n(stuffer, 1)); diff --git a/tests/cbmc/proofs/s2n_stuffer_printf/Makefile b/tests/cbmc/proofs/s2n_stuffer_printf/Makefile new file mode 100644 index 00000000000..757d05fed98 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_printf/Makefile @@ -0,0 +1,38 @@ +# +# +# 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. + +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_printf +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)/madvise.c +PROOF_SOURCES += $(PROOF_STUB)/mlock.c +PROOF_SOURCES += $(PROOF_STUB)/munlock.c +PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c +PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c +PROOF_SOURCES += $(PROOF_STUB)/sysconf.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.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_safety.c +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_printf/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_printf/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_printf/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c b/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c new file mode 100644 index 00000000000..e5fb8f593fe --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c @@ -0,0 +1,66 @@ +/* + * 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" +#include "utils/s2n_mem.h" + +void s2n_stuffer_printf_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *stuffer = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(stuffer))); + + size_t format_len; + char *format = ensure_c_str_is_allocated(format_len); + + /* CBMC defines va_list as void** */ + size_t va_list_size; + __CPROVER_assume(va_list_size % sizeof(void*) == 0); + void** va_list_mem = malloc(va_list_size); + + /* Store the stuffer to compare after the write */ + struct s2n_stuffer old_stuffer = *stuffer; + struct store_byte_from_buffer old_byte; + save_byte_from_array(old_stuffer.blob.data, old_stuffer.write_cursor, &old_byte); + + int result = s2n_stuffer_vprintf(stuffer, format, va_list_mem); + assert(s2n_result_is_ok(s2n_stuffer_validate(stuffer))); + + /* The basic stuffer fields should NOT be updated */ + assert(old_stuffer.growable == stuffer->growable); + assert(old_stuffer.tainted == stuffer->tainted); + assert(old_stuffer.alloced == stuffer->alloced); + + /* Any previously written data should NOT be updated */ + if (old_stuffer.write_cursor > 0) { + assert_byte_from_buffer_matches(stuffer->blob.data, &old_byte); + } + + /* The read cursor should NOT be updated */ + assert(old_stuffer.read_cursor == stuffer->read_cursor); + + /* The write cursor should only be updated on success */ + if (result == S2N_SUCCESS) { + assert(old_stuffer.write_cursor <= stuffer->write_cursor); + } else { + assert(old_stuffer.write_cursor == stuffer->write_cursor); + } +} diff --git a/tests/cbmc/proofs/s2n_stuffer_wipe_n/s2n_stuffer_wipe_n_harness.c b/tests/cbmc/proofs/s2n_stuffer_wipe_n/s2n_stuffer_wipe_n_harness.c index 9d99ad67a3c..3cf327c6e82 100644 --- a/tests/cbmc/proofs/s2n_stuffer_wipe_n/s2n_stuffer_wipe_n_harness.c +++ b/tests/cbmc/proofs/s2n_stuffer_wipe_n/s2n_stuffer_wipe_n_harness.c @@ -30,26 +30,38 @@ void s2n_stuffer_wipe_n_harness() __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(stuffer))); /* Save previous state. */ - uint32_t old_n = n; struct s2n_stuffer old_stuffer = *stuffer; - /* Function under verification. */ - if (s2n_stuffer_wipe_n(stuffer, n) == S2N_SUCCESS) - { - assert(s2n_result_is_ok(s2n_stuffer_validate(stuffer))); - assert(old_n == n); - assert(S2N_IMPLIES(n >= old_stuffer.write_cursor, - stuffer->high_water_mark == 0 && - stuffer->tainted == 0 && - stuffer->write_cursor == 0 && - stuffer->read_cursor == 0)); - assert(S2N_IMPLIES(n < old_stuffer.write_cursor, - (stuffer->read_cursor == MIN(old_stuffer.read_cursor, (old_stuffer.write_cursor - n))))); - assert(S2N_IMPLIES(n < old_stuffer.write_cursor, - (stuffer->write_cursor == old_stuffer.write_cursor - n))); - if(n >= old_stuffer.write_cursor) - assert_all_bytes_are(stuffer->blob.data, S2N_WIPE_PATTERN, old_stuffer.high_water_mark); - else - assert_all_bytes_are(stuffer->blob.data+(old_stuffer.write_cursor - n), S2N_WIPE_PATTERN, n); - }; + /* Save byte from untouched portion to compare after the wipe */ + uint32_t expect_wiped = MIN(n, old_stuffer.write_cursor); + uint32_t expected_write_cursor = old_stuffer.write_cursor - expect_wiped; + struct store_byte_from_buffer old_byte; + save_byte_from_array(old_stuffer.blob.data, expected_write_cursor, &old_byte); + + /* Given a valid stuffer, wipe_n always succeeds */ + assert(s2n_stuffer_wipe_n(stuffer, n) == S2N_SUCCESS); + assert(s2n_result_is_ok(s2n_stuffer_validate(stuffer))); + + /* The basic stuffer fields should NOT be updated */ + assert(stuffer->high_water_mark == old_stuffer.high_water_mark); + assert(stuffer->tainted == old_stuffer.tainted); + assert(stuffer->blob == old_stuffer.blob); + assert(stuffer->blob.data == old_stuffer.blob.data); + + /* The read and write cursors should be updated */ + assert(S2N_IMPLIES(expect_wiped < n, stuffer->write_cursor == 0)); + assert(S2N_IMPLIES(expect_wiped < n, stuffer->read_cursor == 0)); + assert(stuffer->write_cursor == expected_write_cursor); + assert(stuffer->read_cursor == MIN(old_stuffer.read_cursor, stuffer->write_cursor)); + + /* Any data before the new write cursor should NOT be updated */ + if (expected_write_cursor > 0) { + assert_byte_from_buffer_matches(stuffer->blob.data, &old_byte); + } + + /* Everything after the new write cursor should be wiped */ + if (expect_wiped > 0) { + assert_all_bytes_are(stuffer->blob.data + stuffer->write_cursor, + S2N_WIPE_PATTERN, expect_wiped); + } }