Add s2n_stuffer_shift (#4458)

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(&copy));
+    uint8_t *data = stuffer->blob.data + stuffer->read_cursor;
+    uint32_t data_size = s2n_stuffer_data_available(stuffer);
+    POSIX_GUARD(s2n_stuffer_write_bytes(&copy, data, data_size));
+    *stuffer = copy;
+    return S2N_SUCCESS;
+}

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

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

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

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

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 <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_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);
+}

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 <assert.h>
+#include <cbmc_proof/nondet.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+/**
+ * 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);
+}

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();
 }