Memory-safety proofs for aws_byte_buf (#331)

* Memory-safety proofs for aws_byte_buf

Adds invariants and proof harnesses for the following functions:
 - aws_byte_buf_append
 - aws_byte_buf_append_dynamic
 - aws_byte_buf_append_with_lookup
 - aws_byte_buf_clean_up
 - aws_byte_buf_from_array
 - aws_byte_buf_from_empty_array
 - aws_byte_buf_init
 - aws_byte_buf_init_copy_from_cursor
 - aws_byte_buf_reserve
 - aws_byte_buf_secure_zero

Signed-off-by: Felipe R. Monteiro <[email protected]>

.cbmc-batch/include/proof_helpers/make_common_data_structures.h

@@ -27,23 +27,20 @@
 
 #include <stdlib.h>
 
-#define MAX_STR_LEN 2
-#define MAX_BUF_LEN 2
-
-#define ASSUME_VALID_MEMORY(ptr) ptr = malloc(sizeof(*(ptr)))
-#define ASSUME_VALID_MEMORY_COUNT(ptr, count) ptr = malloc(sizeof(*(ptr)) * (count))
+#define ASSUME_VALID_MEMORY(ptr) ptr = bounded_malloc(sizeof(*(ptr)))
+#define ASSUME_VALID_MEMORY_COUNT(ptr, count) ptr = bounded_malloc(sizeof(*(ptr)) * (count))
 #define ASSUME_DEFAULT_ALLOCATOR(allocator) allocator = aws_default_allocator()
 #define ASSUME_CAN_FAIL_ALLOCATOR(allocator) allocator = can_fail_allocator()
 
 /*
  * Checks whether aws_byte_buf is bounded by max_size
  */
-bool is_bounded_byte_buf(const struct aws_byte_buf *const buf, const size_t max_size);
+bool aws_byte_buf_is_bounded(const struct aws_byte_buf *const buf, const size_t max_size);
 
 /*
  * Checks whether aws_byte_buf has the correct allocator
  */
-bool is_byte_buf_expected_alloc(const struct aws_byte_buf *const buf);
+bool aws_byte_buf_has_allocator(const struct aws_byte_buf *const buf);
 
 /*
  * Ensures aws_byte_buf has a proper allocated buffer member
@@ -53,7 +50,7 @@ void ensure_byte_buf_has_allocated_buffer_member(struct aws_byte_buf *const buf)
 /*
  * Checks whether aws_byte_cursor is bounded by max_size
  */
-bool is_bounded_byte_cursor(const struct aws_byte_cursor *const cursor, const size_t max_size);
+bool aws_byte_cursor_is_bounded(const struct aws_byte_cursor *const cursor, const size_t max_size);
 
 /*
  * Ensures aws_byte_cursor has a proper allocated buffer member

.cbmc-batch/jobs/Makefile.aws_byte_buf

@@ -0,0 +1,20 @@
+# Copyright 2019 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.
+
+##########
+
+# Sufficently long to get full coverage on the aws_byte_buf and aws_byte_cursor APIs
+# short enough that all proofs complete in less than a minute
+MAX_BUFFER_SIZE ?= 10
+
+DEFINES += -DMAX_BUFFER_SIZE=$(MAX_BUFFER_SIZE)

.cbmc-batch/jobs/aws_byte_buf_append/Makefile

@@ -12,13 +12,17 @@
 # limitations under the License.
 
 ###########
-CBMC_UNWINDSET =
+include ../Makefile.aws_byte_buf
+
+UNWINDSET += memcpy_impl.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 1)))
 
 CBMCFLAGS +=
 
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
-DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override_no_op.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override.c
 DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 

.cbmc-batch/jobs/aws_byte_buf_append/aws_byte_buf_append_harness.c

@@ -17,22 +17,34 @@
 #include <proof_helpers/make_common_data_structures.h>
 
 void aws_byte_buf_append_harness() {
-    size_t len1 = nondet_size_t();
-    __CPROVER_assume(len1 <= MAX_BUF_LEN);
-    size_t len2 = nondet_size_t();
+    struct aws_byte_buf to;
+    __CPROVER_assume(aws_byte_buf_is_bounded(&to, MAX_BUFFER_SIZE));
+    ensure_byte_buf_has_allocated_buffer_member(&to);
+    __CPROVER_assume(aws_byte_buf_is_valid(&to));
 
-    /* Need arbitrary buf that is "correct enough" */
-    struct aws_byte_buf *to;
-    ASSUME_VALID_MEMORY(to);
-    ASSUME_VALID_MEMORY_COUNT(to->buffer, len1);
-    to->capacity = len1;
-    __CPROVER_assume(to->len <= to->capacity);
+    /* save current state of the data structure */
+    struct aws_byte_buf to_old = to;
 
-    /* Need arbitrary cursor */
-    struct aws_byte_cursor *from;
-    ASSUME_VALID_MEMORY(from);
-    from->ptr = malloc(len2);
-    __CPROVER_assume(from->len <= len2);
+    struct aws_byte_cursor from;
+    __CPROVER_assume(aws_byte_cursor_is_bounded(&from, MAX_BUFFER_SIZE));
+    ensure_byte_cursor_has_allocated_buffer_member(&from);
+    __CPROVER_assume(aws_byte_cursor_is_valid(&from));
 
-    aws_byte_buf_append(to, from);
+    /* save current state of the data structure */
+    struct aws_byte_cursor from_old = from;
+
+    if (aws_byte_buf_append(&to, &from) == AWS_OP_SUCCESS) {
+        assert(to.len == to_old.len + from.len);
+    } else {
+        /* if the operation return an error, to must not change */
+        assert_bytes_match(to_old.buffer, to.buffer, to.len);
+        assert(to_old.len == to.len);
+    }
+
+    assert(aws_byte_buf_is_valid(&to));
+    assert(aws_byte_cursor_is_valid(&from));
+    assert(to_old.allocator == to.allocator);
+    assert(to_old.capacity == to.capacity);
+    assert_bytes_match(from_old.ptr, from.ptr, from.len);
+    assert(from_old.len == from.len);
 }

.cbmc-batch/jobs/aws_byte_buf_append/cbmc-batch.yaml

@@ -1,4 +1,4 @@
 jobos: ubuntu16
-cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--function;aws_byte_buf_append_harness"
+cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--unwindset;memcpy_impl.0:11;--unwind;1"
 goto: aws_byte_buf_append_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_append_dynamic/Makefile

@@ -12,12 +12,15 @@
 # limitations under the License.
 
 ###########
-CBMC_UNWINDSET =
+include ../Makefile.aws_byte_buf
+
+UNWINDSET +=
 
 CBMCFLAGS +=
 
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
 DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override_no_op.c
 DEPENDENCIES += $(SRCDIR)/source/byte_buf.c

.cbmc-batch/jobs/aws_byte_buf_append_dynamic/aws_byte_buf_append_dynamic_harness.c

@@ -21,13 +21,27 @@ void aws_byte_buf_append_dynamic_harness() {
     ensure_byte_buf_has_allocated_buffer_member(&to);
     __CPROVER_assume(aws_byte_buf_is_valid(&to));
 
+    /* save current state of the data structure */
+    struct aws_byte_buf to_old = to;
+
     struct aws_byte_cursor from;
     ensure_byte_cursor_has_allocated_buffer_member(&from);
     __CPROVER_assume(aws_byte_cursor_is_valid(&from));
 
-    aws_byte_buf_append_dynamic(&to, &from);
+    /* save current state of the data structure */
+    struct aws_byte_cursor from_old = from;
+
+    if (aws_byte_buf_append_dynamic(&to, &from) == AWS_OP_SUCCESS) {
+        assert(to.len == to_old.len + from.len);
+    } else {
+        /* if the operation return an error, to must not change */
+        assert_bytes_match(to_old.buffer, to.buffer, to.len);
+        assert(to_old.len == to.len);
+    }
 
     assert(aws_byte_buf_is_valid(&to));
-    assert(is_byte_buf_expected_alloc(&to));
     assert(aws_byte_cursor_is_valid(&from));
+    assert(to_old.allocator == to.allocator);
+    assert_bytes_match(from_old.ptr, from.ptr, from.len);
+    assert(from_old.len == from.len);
 }

.cbmc-batch/jobs/aws_byte_buf_append_dynamic/cbmc-batch.yaml

@@ -1,4 +1,4 @@
 jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
+cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--unwind;1"
 goto: aws_byte_buf_append_dynamic_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/Makefile

@@ -12,16 +12,15 @@
 # limitations under the License.
 
 ###########
-# This size is suficcient to get full code coverage
-MAX_BUF_SIZE ?= 10
-DEFINES += -DMAX_BUF_SIZE=$(MAX_BUF_SIZE)
+include ../Makefile.aws_byte_buf
 
-UNWINDSET += aws_byte_buf_append_with_lookup.0:$(shell echo $$(($(MAX_BUF_SIZE) + 1)))
+UNWINDSET += aws_byte_buf_append_with_lookup.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 1)))
 
 CBMCFLAGS +=
 
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
 DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override_no_op.c
 DEPENDENCIES += $(SRCDIR)/source/byte_buf.c

.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/aws_byte_buf_append_with_lookup_harness.c

@@ -18,23 +18,38 @@
 
 void aws_byte_buf_append_with_lookup_harness() {
     struct aws_byte_buf to;
-    __CPROVER_assume(is_bounded_byte_buf(&to, MAX_BUF_SIZE));
+    __CPROVER_assume(aws_byte_buf_is_bounded(&to, MAX_BUFFER_SIZE));
     ensure_byte_buf_has_allocated_buffer_member(&to);
     __CPROVER_assume(aws_byte_buf_is_valid(&to));
 
+    /* save current state of the data structure */
+    struct aws_byte_buf to_old = to;
+
     struct aws_byte_cursor from;
-    __CPROVER_assume(is_bounded_byte_cursor(&from, MAX_BUF_SIZE));
+    __CPROVER_assume(aws_byte_cursor_is_bounded(&from, MAX_BUFFER_SIZE));
     ensure_byte_cursor_has_allocated_buffer_member(&from);
     __CPROVER_assume(aws_byte_cursor_is_valid(&from));
 
+    /* save current state of the data structure */
+    struct aws_byte_cursor from_old = from;
+
     /**
      * The specification for the function requires that the buffer
      * be at least 256 bytes.
      */
     uint8_t *lookup_table[256];
-    aws_byte_buf_append_with_lookup(&to, &from, lookup_table);
+    if (aws_byte_buf_append_with_lookup(&to, &from, lookup_table) == AWS_OP_SUCCESS) {
+        assert(to.len == to_old.len + from.len);
+    } else {
+        /* if the operation return an error, to must not change */
+        assert_bytes_match(to_old.buffer, to.buffer, to.len);
+        assert(to_old.len == to.len);
+    }
 
     assert(aws_byte_buf_is_valid(&to));
-    assert(is_byte_buf_expected_alloc(&to));
     assert(aws_byte_cursor_is_valid(&from));
+    assert(to_old.allocator == to.allocator);
+    assert(to_old.capacity == to.capacity);
+    assert_bytes_match(from_old.ptr, from.ptr, from.len);
+    assert(from_old.len == from.len);
 }

.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/cbmc-batch.yaml

@@ -1,4 +1,4 @@
 jobos: ubuntu16
-cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--unwindset;aws_byte_buf_append_with_lookup.0:11;--function;aws_byte_buf_append_with_lookup_harness"
+cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--unwindset;aws_byte_buf_append_with_lookup.0:11;--unwind;1"
 goto: aws_byte_buf_append_with_lookup_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_clean_up/Makefile

@@ -0,0 +1,34 @@
+# Copyright 2019 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 ../Makefile.aws_byte_buf
+
+MAX_BUFFER_SIZE=40
+
+# This bound allows us to reach 100% coverage rate
+UNWINDSET += memset_impl.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 1)))
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/stubs/error.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memset_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_clean_up_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_clean_up/aws_byte_buf_clean_up_harness.c

@@ -0,0 +1,30 @@
+/*
+ * Copyright 2019 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 <aws/common/byte_buf.h>
+#include <proof_helpers/make_common_data_structures.h>
+
+void aws_byte_buf_clean_up_harness() {
+    struct aws_byte_buf buf;
+
+    ensure_byte_buf_has_allocated_buffer_member(&buf);
+    __CPROVER_assume(aws_byte_buf_is_valid(&buf));
+
+    aws_byte_buf_clean_up(&buf);
+    assert(buf.allocator == NULL);
+    assert(buf.buffer == NULL);
+    assert(buf.len == 0);
+    assert(buf.capacity == 0);
+}

.cbmc-batch/jobs/aws_byte_buf_from_c_str/cbmc-batch.yaml → .cbmc-batch/jobs/aws_byte_buf_clean_up/cbmc-batch.yaml

@@ -1,4 +1,4 @@
 jobos: ubuntu16
-cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--unwindset;strlen.0:33;--function;aws_byte_buf_from_c_str_harness"
-goto: aws_byte_buf_from_c_str_harness.goto
+cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--unwindset;memset_impl.0:41;--unwind;1"
+goto: aws_byte_buf_clean_up_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_from_c_str/Makefile → .cbmc-batch/jobs/aws_byte_buf_from_array/Makefile

@@ -12,18 +12,18 @@
 # limitations under the License.
 
 ###########
-#NOTE: If we don't use the unwindset, leave it empty
-CBMC_UNWINDSET = --unwindset
-CBMC_UNWINDSET += strlen.0:33
+UNWINDSET +=
 
 CBMCFLAGS +=
 
 DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
 DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 
-ENTRY = aws_byte_buf_from_c_str_harness
+ENTRY = aws_byte_buf_from_array_harness
 ###########
 
 include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_from_array/aws_byte_buf_from_array_harness.c

@@ -0,0 +1,38 @@
+/*
+ * Copyright 2019 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 <aws/common/byte_buf.h>
+#include <proof_helpers/make_common_data_structures.h>
+
+void aws_byte_buf_from_array_harness() {
+    /* parameters */
+    size_t length;
+    uint8_t *array;
+
+    /* assumptions */
+    ASSUME_VALID_MEMORY_COUNT(array, length);
+
+    /* operation under verification */
+    struct aws_byte_buf buf = aws_byte_buf_from_array(array, length);
+
+    /* assertions */
+    assert(aws_byte_buf_is_valid(&buf));
+    assert(buf.len == length);
+    assert(buf.capacity == length);
+    assert(buf.allocator == NULL);
+    if (buf.buffer) {
+        assert_bytes_match(buf.buffer, array, buf.len);
+    }
+}

.cbmc-batch/jobs/aws_byte_buf_from_array/cbmc-batch.yaml

@@ -0,0 +1,4 @@
+jobos: ubuntu16
+cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--unwind;1"
+goto: aws_byte_buf_from_array_harness.goto
+expected: "SUCCESSFUL"