Add CBMC proof for s2n_stuffer_printf (#4309)

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;

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

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

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

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

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

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