From 667ebedc035eaba73e4913cf33536e0080d99574 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 9 May 2019 17:41:24 -0400 Subject: [PATCH] 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 --- .../make_common_data_structures.h | 13 +-- .cbmc-batch/jobs/Makefile.aws_byte_buf | 20 ++++ .cbmc-batch/jobs/aws_byte_buf_append/Makefile | 8 +- .../aws_byte_buf_append_harness.c | 42 ++++--- .../jobs/aws_byte_buf_append/cbmc-batch.yaml | 2 +- .../jobs/aws_byte_buf_append_dynamic/Makefile | 5 +- .../aws_byte_buf_append_dynamic_harness.c | 18 ++- .../cbmc-batch.yaml | 2 +- .../aws_byte_buf_append_with_lookup/Makefile | 7 +- .../aws_byte_buf_append_with_lookup_harness.c | 23 +++- .../cbmc-batch.yaml | 2 +- .../jobs/aws_byte_buf_clean_up/Makefile | 34 ++++++ .../aws_byte_buf_clean_up_harness.c | 30 +++++ .../cbmc-batch.yaml | 4 +- .../Makefile | 8 +- .../aws_byte_buf_from_array_harness.c | 38 ++++++ .../aws_byte_buf_from_array/cbmc-batch.yaml | 4 + .../aws_byte_buf_from_empty_array/Makefile | 29 +++++ .../aws_byte_buf_from_empty_array_harness.c | 33 ++++++ .../cbmc-batch.yaml | 4 + .cbmc-batch/jobs/aws_byte_buf_init/Makefile | 5 +- .../aws_byte_buf_init_harness.c | 24 +++- .../jobs/aws_byte_buf_init/cbmc-batch.yaml | 2 +- .../aws_byte_buf_init_copy_harness.c | 4 +- .../Makefile | 3 +- ...s_byte_buf_init_copy_from_cursor_harness.c | 23 ++-- .../jobs/aws_byte_buf_reserve/Makefile | 5 +- .../aws_byte_buf_reserve_harness.c | 11 +- .../jobs/aws_byte_buf_reserve/cbmc-batch.yaml | 2 +- .../aws_byte_buf_reserve_relative_harness.c | 2 +- .../jobs/aws_byte_buf_secure_zero/Makefile | 35 ++++++ .../aws_byte_buf_secure_zero_harness.c} | 22 ++-- .../aws_byte_buf_secure_zero/cbmc-batch.yaml | 4 + .../source/make_common_data_structures.c | 10 +- include/aws/common/byte_buf.h | 10 +- source/byte_buf.c | 108 ++++++++++++------ source/encoding.c | 8 +- tests/byte_buf_test.c | 5 +- tests/encoding_test.c | 6 +- 39 files changed, 481 insertions(+), 134 deletions(-) create mode 100644 .cbmc-batch/jobs/Makefile.aws_byte_buf create mode 100644 .cbmc-batch/jobs/aws_byte_buf_clean_up/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_buf_clean_up/aws_byte_buf_clean_up_harness.c rename .cbmc-batch/jobs/{aws_byte_buf_from_c_str => aws_byte_buf_clean_up}/cbmc-batch.yaml (62%) rename .cbmc-batch/jobs/{aws_byte_buf_from_c_str => aws_byte_buf_from_array}/Makefile (84%) create mode 100644 .cbmc-batch/jobs/aws_byte_buf_from_array/aws_byte_buf_from_array_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_buf_from_array/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/aws_byte_buf_from_empty_array/Makefile create mode 100644 .cbmc-batch/jobs/aws_byte_buf_from_empty_array/aws_byte_buf_from_empty_array_harness.c create mode 100644 .cbmc-batch/jobs/aws_byte_buf_from_empty_array/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/aws_byte_buf_secure_zero/Makefile rename .cbmc-batch/jobs/{aws_byte_buf_from_c_str/aws_byte_buf_from_c_str_harness.c => aws_byte_buf_secure_zero/aws_byte_buf_secure_zero_harness.c} (58%) create mode 100644 .cbmc-batch/jobs/aws_byte_buf_secure_zero/cbmc-batch.yaml diff --git a/.cbmc-batch/include/proof_helpers/make_common_data_structures.h b/.cbmc-batch/include/proof_helpers/make_common_data_structures.h index 1afadbb90..0c737b66f 100644 --- a/.cbmc-batch/include/proof_helpers/make_common_data_structures.h +++ b/.cbmc-batch/include/proof_helpers/make_common_data_structures.h @@ -27,23 +27,20 @@ #include -#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 diff --git a/.cbmc-batch/jobs/Makefile.aws_byte_buf b/.cbmc-batch/jobs/Makefile.aws_byte_buf new file mode 100644 index 000000000..db21a486e --- /dev/null +++ b/.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) diff --git a/.cbmc-batch/jobs/aws_byte_buf_append/Makefile b/.cbmc-batch/jobs/aws_byte_buf_append/Makefile index b5e63b3c1..5283a8049 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append/Makefile +++ b/.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 diff --git a/.cbmc-batch/jobs/aws_byte_buf_append/aws_byte_buf_append_harness.c b/.cbmc-batch/jobs/aws_byte_buf_append/aws_byte_buf_append_harness.c index a1a2def7f..62fd54048 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append/aws_byte_buf_append_harness.c +++ b/.cbmc-batch/jobs/aws_byte_buf_append/aws_byte_buf_append_harness.c @@ -17,22 +17,34 @@ #include 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); } diff --git a/.cbmc-batch/jobs/aws_byte_buf_append/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_append/cbmc-batch.yaml index 1036b8a40..a1ec477da 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append/cbmc-batch.yaml +++ b/.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" diff --git a/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/Makefile b/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/Makefile index 3321326b9..bf6fcdcda 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/Makefile +++ b/.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 diff --git a/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/aws_byte_buf_append_dynamic_harness.c b/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/aws_byte_buf_append_dynamic_harness.c index bef2d0ba4..f2bf04a70 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/aws_byte_buf_append_dynamic_harness.c +++ b/.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); } diff --git a/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/cbmc-batch.yaml index 0d4ddcd16..0b9feb10a 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append_dynamic/cbmc-batch.yaml +++ b/.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" diff --git a/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/Makefile b/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/Makefile index f27a32f63..25fe4870e 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/Makefile +++ b/.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 diff --git a/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/aws_byte_buf_append_with_lookup_harness.c b/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/aws_byte_buf_append_with_lookup_harness.c index 34a3b8df1..1cac8d464 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/aws_byte_buf_append_with_lookup_harness.c +++ b/.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); } diff --git a/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/cbmc-batch.yaml index c42dcfb04..d2d2d0503 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/cbmc-batch.yaml +++ b/.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" diff --git a/.cbmc-batch/jobs/aws_byte_buf_clean_up/Makefile b/.cbmc-batch/jobs/aws_byte_buf_clean_up/Makefile new file mode 100644 index 000000000..6c406989d --- /dev/null +++ b/.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 diff --git a/.cbmc-batch/jobs/aws_byte_buf_clean_up/aws_byte_buf_clean_up_harness.c b/.cbmc-batch/jobs/aws_byte_buf_clean_up/aws_byte_buf_clean_up_harness.c new file mode 100644 index 000000000..bf36dd321 --- /dev/null +++ b/.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 +#include + +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); +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_c_str/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_clean_up/cbmc-batch.yaml similarity index 62% rename from .cbmc-batch/jobs/aws_byte_buf_from_c_str/cbmc-batch.yaml rename to .cbmc-batch/jobs/aws_byte_buf_clean_up/cbmc-batch.yaml index 2216f9698..7953c2240 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_from_c_str/cbmc-batch.yaml +++ b/.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" diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_c_str/Makefile b/.cbmc-batch/jobs/aws_byte_buf_from_array/Makefile similarity index 84% rename from .cbmc-batch/jobs/aws_byte_buf_from_c_str/Makefile rename to .cbmc-batch/jobs/aws_byte_buf_from_array/Makefile index 95aef388e..e9f7f1336 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_from_c_str/Makefile +++ b/.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 diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_array/aws_byte_buf_from_array_harness.c b/.cbmc-batch/jobs/aws_byte_buf_from_array/aws_byte_buf_from_array_harness.c new file mode 100644 index 000000000..0aee5963a --- /dev/null +++ b/.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 +#include + +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); + } +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_array/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_from_array/cbmc-batch.yaml new file mode 100644 index 000000000..5909d6994 --- /dev/null +++ b/.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" diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_empty_array/Makefile b/.cbmc-batch/jobs/aws_byte_buf_from_empty_array/Makefile new file mode 100644 index 000000000..1c8149723 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_from_empty_array/Makefile @@ -0,0 +1,29 @@ +# 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. + +########### +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_empty_array_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_empty_array/aws_byte_buf_from_empty_array_harness.c b/.cbmc-batch/jobs/aws_byte_buf_from_empty_array/aws_byte_buf_from_empty_array_harness.c new file mode 100644 index 000000000..d0163132b --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_from_empty_array/aws_byte_buf_from_empty_array_harness.c @@ -0,0 +1,33 @@ +/* + * 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 +#include + +void aws_byte_buf_from_empty_array_harness() { + size_t capacity; + void *array; + + ASSUME_VALID_MEMORY_COUNT(array, capacity); + + struct aws_byte_buf buf = aws_byte_buf_from_empty_array(array, capacity); + assert(aws_byte_buf_is_valid(&buf)); + assert(buf.len == 0); + assert(buf.capacity == capacity); + assert(buf.allocator == NULL); + if (buf.buffer) { + assert_bytes_match(buf.buffer, array, capacity); + } +} diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_empty_array/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_from_empty_array/cbmc-batch.yaml new file mode 100644 index 000000000..fbb9b3071 --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_from_empty_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_empty_array_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_byte_buf_init/Makefile b/.cbmc-batch/jobs/aws_byte_buf_init/Makefile index 672acfdc1..5430fe661 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_init/Makefile +++ b/.cbmc-batch/jobs/aws_byte_buf_init/Makefile @@ -12,8 +12,9 @@ # limitations under the License. ########### -#NOTE: If we don't use the unwindset, leave it empty -#CBMC_UNWINDSET = +include ../Makefile.aws_byte_buf + +UNWINDSET += CBMCFLAGS += diff --git a/.cbmc-batch/jobs/aws_byte_buf_init/aws_byte_buf_init_harness.c b/.cbmc-batch/jobs/aws_byte_buf_init/aws_byte_buf_init_harness.c index 356c78df2..375111c39 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_init/aws_byte_buf_init_harness.c +++ b/.cbmc-batch/jobs/aws_byte_buf_init/aws_byte_buf_init_harness.c @@ -18,12 +18,26 @@ #include void aws_byte_buf_init_harness() { - struct aws_allocator *allocator = can_fail_allocator(); + /* data structure */ + struct aws_byte_buf buf; - struct aws_byte_buf *buf; - ASSUME_VALID_MEMORY(buf); + /* parameters */ + struct aws_allocator *allocator; + size_t capacity; - size_t len = nondet_size_t(); + /* assumptions */ + if (nondet_bool()) { + ASSUME_CAN_FAIL_ALLOCATOR(allocator); + } else { + allocator = NULL; + } + __CPROVER_assume(capacity <= MAX_BUFFER_SIZE); - aws_byte_buf_init(buf, allocator, len); + if (!aws_byte_buf_init(&buf, allocator, capacity)) { + /* assertions */ + assert(aws_byte_buf_is_valid(&buf)); + assert(buf.allocator == allocator); + assert(buf.len == 0); + assert(buf.capacity == capacity); + } } diff --git a/.cbmc-batch/jobs/aws_byte_buf_init/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_init/cbmc-batch.yaml index 9e785c165..ee2946f3d 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_init/cbmc-batch.yaml +++ b/.cbmc-batch/jobs/aws_byte_buf_init/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_init_harness.goto expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_byte_buf_init_copy/aws_byte_buf_init_copy_harness.c b/.cbmc-batch/jobs/aws_byte_buf_init_copy/aws_byte_buf_init_copy_harness.c index fb0d17513..245964a89 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_init_copy/aws_byte_buf_init_copy_harness.c +++ b/.cbmc-batch/jobs/aws_byte_buf_init_copy/aws_byte_buf_init_copy_harness.c @@ -26,7 +26,7 @@ void aws_byte_buf_init_copy_harness() { struct aws_byte_buf src; /* assumptions */ - __CPROVER_assume(is_bounded_byte_buf(&src, MAX_BUFFER_SIZE)); + __CPROVER_assume(aws_byte_buf_is_bounded(&src, MAX_BUFFER_SIZE)); ensure_byte_buf_has_allocated_buffer_member(&src); __CPROVER_assume(aws_byte_buf_is_valid(&src)); ASSUME_VALID_MEMORY(dest); @@ -41,7 +41,7 @@ void aws_byte_buf_init_copy_harness() { if (!aws_byte_buf_init_copy(dest, allocator, &src)) { /* assertions */ assert(aws_byte_buf_is_valid(dest)); - assert(is_byte_buf_expected_alloc(dest)); + assert(aws_byte_buf_has_allocator(dest)); assert(dest->len == src.len); assert(dest->capacity == src.capacity); assert_bytes_match(dest->buffer, src.buffer, dest->len); diff --git a/.cbmc-batch/jobs/aws_byte_buf_init_copy_from_cursor/Makefile b/.cbmc-batch/jobs/aws_byte_buf_init_copy_from_cursor/Makefile index 295a2bd1d..9601dbc3e 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_init_copy_from_cursor/Makefile +++ b/.cbmc-batch/jobs/aws_byte_buf_init_copy_from_cursor/Makefile @@ -12,8 +12,7 @@ # limitations under the License. ########### -MAX_BUFFER_SIZE ?= 10 -DEFINES += -DMAX_BUFFER_SIZE=$(MAX_BUFFER_SIZE) +include ../Makefile.aws_byte_buf UNWINDSET += memcpy_impl.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 1))) diff --git a/.cbmc-batch/jobs/aws_byte_buf_init_copy_from_cursor/aws_byte_buf_init_copy_from_cursor_harness.c b/.cbmc-batch/jobs/aws_byte_buf_init_copy_from_cursor/aws_byte_buf_init_copy_from_cursor_harness.c index 77d6dd10a..d5577a61c 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_init_copy_from_cursor/aws_byte_buf_init_copy_from_cursor_harness.c +++ b/.cbmc-batch/jobs/aws_byte_buf_init_copy_from_cursor/aws_byte_buf_init_copy_from_cursor_harness.c @@ -19,27 +19,28 @@ void aws_byte_buf_init_copy_from_cursor_harness() { /* data structure */ - struct aws_byte_buf *buf; + struct aws_byte_buf buf; /* parameters */ struct aws_allocator *allocator; struct aws_byte_cursor cursor; /* assumptions */ - __CPROVER_assume(is_bounded_byte_cursor(&cursor, MAX_BUFFER_SIZE)); + __CPROVER_assume(aws_byte_cursor_is_bounded(&cursor, MAX_BUFFER_SIZE)); ensure_byte_cursor_has_allocated_buffer_member(&cursor); __CPROVER_assume(aws_byte_cursor_is_valid(&cursor)); - ASSUME_VALID_MEMORY(buf); + ASSUME_CAN_FAIL_ALLOCATOR(allocator); - if (!aws_byte_buf_init_copy_from_cursor(buf, allocator, cursor)) { + if (aws_byte_buf_init_copy_from_cursor(&buf, allocator, cursor) == AWS_OP_SUCCESS) { /* assertions */ - assert(aws_byte_buf_is_valid(buf)); - assert(buf->len == cursor.len); - assert(buf->capacity == cursor.len); - assert(buf->allocator == allocator); - assert_bytes_match(buf->buffer, cursor.ptr, buf->len); + assert(aws_byte_buf_is_valid(&buf)); + assert(aws_byte_cursor_is_valid(&cursor)); + assert(buf.len == cursor.len); + assert(buf.capacity == cursor.len); + assert(buf.allocator == allocator); + if (buf.buffer) { + assert_bytes_match(buf.buffer, cursor.ptr, buf.len); + } } - /* assertions */ - assert(aws_byte_cursor_is_valid(&cursor)); } diff --git a/.cbmc-batch/jobs/aws_byte_buf_reserve/Makefile b/.cbmc-batch/jobs/aws_byte_buf_reserve/Makefile index c23f32065..3dcd94ff9 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_reserve/Makefile +++ b/.cbmc-batch/jobs/aws_byte_buf_reserve/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 += $(HELPERDIR)/stubs/memset_override_no_op.c diff --git a/.cbmc-batch/jobs/aws_byte_buf_reserve/aws_byte_buf_reserve_harness.c b/.cbmc-batch/jobs/aws_byte_buf_reserve/aws_byte_buf_reserve_harness.c index 575969477..bbf6b4d66 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_reserve/aws_byte_buf_reserve_harness.c +++ b/.cbmc-batch/jobs/aws_byte_buf_reserve/aws_byte_buf_reserve_harness.c @@ -23,11 +23,16 @@ void aws_byte_buf_reserve_harness() { struct aws_byte_buf old = buf; size_t requested_capacity; - int rval = aws_byte_buf_reserve(&buf, requested_capacity); - if (rval == AWS_OP_SUCCESS) { + if (aws_byte_buf_reserve(&buf, requested_capacity) == AWS_OP_SUCCESS) { assert(buf.capacity >= requested_capacity); + assert(aws_byte_buf_has_allocator(&buf)); } + assert(aws_byte_buf_is_valid(&buf)); - assert(is_byte_buf_expected_alloc(&buf)); + assert(old.len == buf.len); + assert(old.allocator == buf.allocator); + if (!buf.buffer) { + assert_bytes_match(old.buffer, buf.buffer, buf.len); + } } diff --git a/.cbmc-batch/jobs/aws_byte_buf_reserve/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_reserve/cbmc-batch.yaml index 51fb5deb3..cb6134958 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_reserve/cbmc-batch.yaml +++ b/.cbmc-batch/jobs/aws_byte_buf_reserve/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_reserve_harness.goto expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_byte_buf_reserve_relative/aws_byte_buf_reserve_relative_harness.c b/.cbmc-batch/jobs/aws_byte_buf_reserve_relative/aws_byte_buf_reserve_relative_harness.c index 22d93ef91..e032ecc8c 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_reserve_relative/aws_byte_buf_reserve_relative_harness.c +++ b/.cbmc-batch/jobs/aws_byte_buf_reserve_relative/aws_byte_buf_reserve_relative_harness.c @@ -27,7 +27,7 @@ void aws_byte_buf_reserve_relative_harness() { if (rval == AWS_OP_SUCCESS) { assert(buf.capacity >= (old.len + requested_capacity)); + assert(aws_byte_buf_has_allocator(&buf)); } assert(aws_byte_buf_is_valid(&buf)); - assert(is_byte_buf_expected_alloc(&buf)); } diff --git a/.cbmc-batch/jobs/aws_byte_buf_secure_zero/Makefile b/.cbmc-batch/jobs/aws_byte_buf_secure_zero/Makefile new file mode 100644 index 000000000..eac62599f --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_secure_zero/Makefile @@ -0,0 +1,35 @@ +# 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)/source/utils.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_secure_zero_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_byte_buf_from_c_str/aws_byte_buf_from_c_str_harness.c b/.cbmc-batch/jobs/aws_byte_buf_secure_zero/aws_byte_buf_secure_zero_harness.c similarity index 58% rename from .cbmc-batch/jobs/aws_byte_buf_from_c_str/aws_byte_buf_from_c_str_harness.c rename to .cbmc-batch/jobs/aws_byte_buf_secure_zero/aws_byte_buf_secure_zero_harness.c index f18aafb73..0c43dc1fd 100644 --- a/.cbmc-batch/jobs/aws_byte_buf_from_c_str/aws_byte_buf_from_c_str_harness.c +++ b/.cbmc-batch/jobs/aws_byte_buf_secure_zero/aws_byte_buf_secure_zero_harness.c @@ -16,19 +16,17 @@ #include #include -void aws_byte_buf_from_c_str_harness() { - size_t len = nondet_size_t(); +void aws_byte_buf_secure_zero_harness() { + struct aws_byte_buf buf; - char *c_str; - ASSUME_VALID_MEMORY_COUNT(c_str, len); + __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&buf); + __CPROVER_assume(aws_byte_buf_is_valid(&buf)); - /* Need *c_str to be a '\0'-terminated C string, so assume an arbitrary character is 0 */ - int index = nondet_int(); - __CPROVER_assume(index >= 0 && index < len); - c_str[index] = 0; + /* operation under verification */ + aws_byte_buf_secure_zero(&buf); - /* Assume the length of the string is bounded by some max length */ - __CPROVER_assume(len <= MAX_STR_LEN); - - aws_byte_buf_from_c_str(c_str); + assert(aws_byte_buf_is_valid(&buf)); + assert_all_zeroes(buf.buffer, buf.capacity); + assert(buf.len == 0); } diff --git a/.cbmc-batch/jobs/aws_byte_buf_secure_zero/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_secure_zero/cbmc-batch.yaml new file mode 100644 index 000000000..72c4c854a --- /dev/null +++ b/.cbmc-batch/jobs/aws_byte_buf_secure_zero/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;--unwindset;memset_impl.0:41;--unwind;1" +goto: aws_byte_buf_secure_zero_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/source/make_common_data_structures.c b/.cbmc-batch/source/make_common_data_structures.c index cadfe2f11..6d6fb6ed5 100644 --- a/.cbmc-batch/source/make_common_data_structures.c +++ b/.cbmc-batch/source/make_common_data_structures.c @@ -20,20 +20,20 @@ #include #include -bool is_bounded_byte_buf(const struct aws_byte_buf *const buf, const size_t max_size) { - return buf->capacity <= max_size; +bool aws_byte_buf_is_bounded(const struct aws_byte_buf *const buf, const size_t max_size) { + return (buf->capacity <= max_size); } -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) { return (buf->allocator == can_fail_allocator()); } void ensure_byte_buf_has_allocated_buffer_member(struct aws_byte_buf *const buf) { - buf->allocator = can_fail_allocator(); + buf->allocator = (nondet_bool()) ? NULL : can_fail_allocator(); buf->buffer = bounded_malloc(sizeof(*(buf->buffer)) * buf->capacity); } -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) { return cursor->len <= max_size; } diff --git a/include/aws/common/byte_buf.h b/include/aws/common/byte_buf.h index 5f6fbe20c..a0600545c 100644 --- a/include/aws/common/byte_buf.h +++ b/include/aws/common/byte_buf.h @@ -317,7 +317,7 @@ int aws_byte_buf_append(struct aws_byte_buf *to, const struct aws_byte_cursor *f /** * Copies from to to while converting bytes via the passed in lookup table. * If to is too small, AWS_ERROR_DEST_COPY_TOO_SMALL will be - * returned. dest->len will contain the amount of data actually copied to dest. + * returned. to->len will contain its original size plus the amount of data actually copied to to. * * from and to should not be the same buffer (overlap is not handled) * lookup_table must be at least 256 bytes @@ -458,20 +458,24 @@ AWS_STATIC_IMPL struct aws_byte_buf aws_byte_buf_from_c_str(const char *c_str) { } AWS_STATIC_IMPL struct aws_byte_buf aws_byte_buf_from_array(const void *bytes, size_t len) { + AWS_PRECONDITION(AWS_MEM_IS_WRITABLE(bytes, len)); struct aws_byte_buf buf; - buf.buffer = (uint8_t *)bytes; + buf.buffer = (len > 0) ? (uint8_t *)bytes : NULL; buf.len = len; buf.capacity = len; buf.allocator = NULL; + AWS_POSTCONDITION(aws_byte_buf_is_valid(&buf)); return buf; } AWS_STATIC_IMPL struct aws_byte_buf aws_byte_buf_from_empty_array(const void *bytes, size_t capacity) { + AWS_PRECONDITION(AWS_MEM_IS_WRITABLE(bytes, capacity)); struct aws_byte_buf buf; - buf.buffer = (uint8_t *)bytes; + buf.buffer = (capacity > 0) ? (uint8_t *)bytes : NULL; buf.len = 0; buf.capacity = capacity; buf.allocator = NULL; + AWS_POSTCONDITION(aws_byte_buf_is_valid(&buf)); return buf; } diff --git a/source/byte_buf.c b/source/byte_buf.c index aeed1ee31..6d8eb3968 100644 --- a/source/byte_buf.c +++ b/source/byte_buf.c @@ -25,13 +25,19 @@ #endif int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity) { - buf->buffer = (uint8_t *)aws_mem_acquire(allocator, capacity); - if (!buf->buffer) { + if (!buf || !allocator) { + return aws_raise_error(AWS_ERROR_INVALID_ARGUMENT); + } + + buf->buffer = (capacity == 0) ? NULL : aws_mem_acquire(allocator, capacity); + if (capacity != 0 && buf->buffer == NULL) { return AWS_OP_ERR; } + buf->len = 0; buf->capacity = capacity; buf->allocator = allocator; + AWS_POSTCONDITION(aws_byte_buf_is_valid(buf)); return AWS_OP_SUCCESS; } @@ -40,6 +46,13 @@ int aws_byte_buf_init_copy(struct aws_byte_buf *dest, struct aws_allocator *allo return aws_raise_error(AWS_ERROR_INVALID_ARGUMENT); } + if (!src->buffer) { + AWS_ZERO_STRUCT(*dest); + dest->allocator = allocator; + AWS_POSTCONDITION(aws_byte_buf_is_valid(dest)); + return AWS_OP_SUCCESS; + } + *dest = *src; dest->allocator = allocator; dest->buffer = (uint8_t *)aws_mem_acquire(allocator, src->capacity); @@ -53,26 +66,17 @@ int aws_byte_buf_init_copy(struct aws_byte_buf *dest, struct aws_allocator *allo } bool aws_byte_buf_is_valid(const struct aws_byte_buf *const buf) { - if (!buf) { - return false; - } - bool buffer_is_valid = (buf->buffer && AWS_MEM_IS_WRITABLE(buf->buffer, buf->len)); - bool capacity_is_valid = (buf->capacity > 0); - bool len_is_valid = (buf->len <= buf->capacity); - return capacity_is_valid && buffer_is_valid && len_is_valid; + return buf && ((buf->capacity == 0 && buf->len == 0 && buf->buffer == NULL) || + (buf->capacity > 0 && buf->len <= buf->capacity && AWS_MEM_IS_WRITABLE(buf->buffer, buf->len))); } bool aws_byte_cursor_is_valid(const struct aws_byte_cursor *cursor) { - bool ptr_is_valid; - if (cursor->ptr) { - ptr_is_valid = (cursor->len && AWS_MEM_IS_WRITABLE(cursor->ptr, cursor->len)); - } else { - ptr_is_valid = (!cursor->len); - } - return ptr_is_valid; + return cursor && + ((cursor->len == 0) || (cursor->len > 0 && cursor->ptr && AWS_MEM_IS_WRITABLE(cursor->ptr, cursor->len))); } void aws_byte_buf_clean_up(struct aws_byte_buf *buf) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf)); if (buf->allocator && buf->buffer) { aws_mem_release(buf->allocator, (void *)buf->buffer); } @@ -83,10 +87,12 @@ void aws_byte_buf_clean_up(struct aws_byte_buf *buf) { } void aws_byte_buf_secure_zero(struct aws_byte_buf *buf) { + AWS_PRECONDITION(aws_byte_buf_is_valid(buf)); if (buf->buffer) { aws_secure_zero(buf->buffer, buf->capacity); } buf->len = 0; + AWS_POSTCONDITION(aws_byte_buf_is_valid(buf)); } void aws_byte_buf_clean_up_secure(struct aws_byte_buf *buf) { @@ -118,21 +124,23 @@ int aws_byte_buf_init_copy_from_cursor( struct aws_byte_buf *dest, struct aws_allocator *allocator, struct aws_byte_cursor src) { - if (!allocator || !dest || !aws_byte_cursor_is_valid(&src) || !src.ptr) { + if (!allocator || !dest || !aws_byte_cursor_is_valid(&src)) { return aws_raise_error(AWS_ERROR_INVALID_ARGUMENT); } AWS_ZERO_STRUCT(*dest); - dest->buffer = (uint8_t *)aws_mem_acquire(allocator, src.len); - if (dest->buffer == NULL) { + dest->buffer = (src.len > 0) ? (uint8_t *)aws_mem_acquire(allocator, src.len) : NULL; + if (src.len != 0 && dest->buffer == NULL) { return AWS_OP_ERR; } dest->len = src.len; dest->capacity = src.len; dest->allocator = allocator; - memcpy(dest->buffer, src.ptr, src.len); + if (src.len > 0) { + memcpy(dest->buffer, src.ptr, src.len); + } AWS_POSTCONDITION(aws_byte_buf_is_valid(dest)); return AWS_OP_SUCCESS; } @@ -405,15 +413,25 @@ bool aws_byte_cursor_eq_c_str_ignore_case(const struct aws_byte_cursor *cursor, } int aws_byte_buf_append(struct aws_byte_buf *to, const struct aws_byte_cursor *from) { - assert(from->ptr); - assert(to->buffer); + AWS_PRECONDITION(aws_byte_buf_is_valid(to)); + AWS_PRECONDITION(aws_byte_cursor_is_valid(from)); if (to->capacity - to->len < from->len) { + AWS_POSTCONDITION(aws_byte_buf_is_valid(to)); + AWS_POSTCONDITION(aws_byte_cursor_is_valid(from)); return aws_raise_error(AWS_ERROR_DEST_COPY_TOO_SMALL); } - memcpy(to->buffer + to->len, from->ptr, from->len); - to->len += from->len; + if (from->len > 0) { + /* This assert teaches clang-tidy that from->ptr and to->buffer cannot be null in a non-empty buffers */ + assert(from->ptr); + assert(to->buffer); + memcpy(to->buffer + to->len, from->ptr, from->len); + to->len += from->len; + } + + AWS_POSTCONDITION(aws_byte_buf_is_valid(to)); + AWS_POSTCONDITION(aws_byte_cursor_is_valid(from)); return AWS_OP_SUCCESS; } @@ -421,12 +439,13 @@ int aws_byte_buf_append_with_lookup( struct aws_byte_buf *AWS_RESTRICT to, const struct aws_byte_cursor *AWS_RESTRICT from, const uint8_t *lookup_table) { - AWS_PRECONDITION(from->ptr); AWS_PRECONDITION(aws_byte_buf_is_valid(to)); AWS_PRECONDITION(aws_byte_cursor_is_valid(from)); AWS_PRECONDITION(AWS_MEM_IS_READABLE(lookup_table, 256)); if (to->capacity - to->len < from->len) { + AWS_POSTCONDITION(aws_byte_buf_is_valid(to)); + AWS_POSTCONDITION(aws_byte_cursor_is_valid(from)); return aws_raise_error(AWS_ERROR_DEST_COPY_TOO_SMALL); } @@ -444,9 +463,11 @@ int aws_byte_buf_append_with_lookup( } int aws_byte_buf_append_dynamic(struct aws_byte_buf *to, const struct aws_byte_cursor *from) { - AWS_PRECONDITION(from->ptr); AWS_PRECONDITION(aws_byte_buf_is_valid(to)); AWS_PRECONDITION(aws_byte_cursor_is_valid(from)); + if (!to->allocator) { + return aws_raise_error(AWS_ERROR_INVALID_ARGUMENT); + } if (to->capacity - to->len < from->len) { /* @@ -456,6 +477,8 @@ int aws_byte_buf_append_dynamic(struct aws_byte_buf *to, const struct aws_byte_c size_t required_capacity = 0; if (aws_add_size_checked(to->capacity, missing_capacity, &required_capacity)) { + AWS_POSTCONDITION(aws_byte_buf_is_valid(to)); + AWS_POSTCONDITION(aws_byte_cursor_is_valid(from)); return AWS_OP_ERR; } @@ -485,9 +508,13 @@ int aws_byte_buf_append_dynamic(struct aws_byte_buf *to, const struct aws_byte_c new_capacity = required_capacity; new_buffer = aws_mem_acquire(to->allocator, new_capacity); if (new_buffer == NULL) { + AWS_POSTCONDITION(aws_byte_buf_is_valid(to)); + AWS_POSTCONDITION(aws_byte_cursor_is_valid(from)); return AWS_OP_ERR; } } else { + AWS_POSTCONDITION(aws_byte_buf_is_valid(to)); + AWS_POSTCONDITION(aws_byte_cursor_is_valid(from)); return AWS_OP_ERR; } } @@ -495,13 +522,15 @@ int aws_byte_buf_append_dynamic(struct aws_byte_buf *to, const struct aws_byte_c /* * Copy old buffer -> new buffer */ - memcpy(new_buffer, to->buffer, to->len); - + if (to->len > 0) { + memcpy(new_buffer, to->buffer, to->len); + } /* * Copy what we actually wanted to append in the first place */ - memcpy(new_buffer + to->len, from->ptr, from->len); - + if (from->len > 0) { + memcpy(new_buffer + to->len, from->ptr, from->len); + } /* * Get rid of the old buffer */ @@ -513,7 +542,12 @@ int aws_byte_buf_append_dynamic(struct aws_byte_buf *to, const struct aws_byte_c to->buffer = new_buffer; to->capacity = new_capacity; } else { - memcpy(to->buffer + to->len, from->ptr, from->len); + if (from->len > 0) { + /* This assert teaches clang-tidy that from->ptr and to->buffer cannot be null in a non-empty buffers */ + assert(from->ptr); + assert(to->buffer); + memcpy(to->buffer + to->len, from->ptr, from->len); + } } to->len += from->len; @@ -524,12 +558,17 @@ int aws_byte_buf_append_dynamic(struct aws_byte_buf *to, const struct aws_byte_c } int aws_byte_buf_reserve(struct aws_byte_buf *buffer, size_t requested_capacity) { - AWS_PRECONDITION(aws_byte_buf_is_valid(buffer)); + if (!buffer->allocator || !aws_byte_buf_is_valid(buffer)) { + return aws_raise_error(AWS_ERROR_INVALID_ARGUMENT); + } + if (requested_capacity <= buffer->capacity) { + AWS_POSTCONDITION(aws_byte_buf_is_valid(buffer)); return AWS_OP_SUCCESS; } if (aws_mem_realloc(buffer->allocator, (void **)&buffer->buffer, buffer->capacity, requested_capacity)) { + AWS_POSTCONDITION(aws_byte_buf_is_valid(buffer)); return AWS_OP_ERR; } @@ -540,10 +579,13 @@ int aws_byte_buf_reserve(struct aws_byte_buf *buffer, size_t requested_capacity) } int aws_byte_buf_reserve_relative(struct aws_byte_buf *buffer, size_t additional_length) { - AWS_PRECONDITION(aws_byte_buf_is_valid(buffer)); + if (!buffer->allocator || !aws_byte_buf_is_valid(buffer)) { + return aws_raise_error(AWS_ERROR_INVALID_ARGUMENT); + } size_t requested_capacity = 0; if (AWS_UNLIKELY(aws_add_size_checked(buffer->len, additional_length, &requested_capacity))) { + AWS_POSTCONDITION(aws_byte_buf_is_valid(buffer)); return AWS_OP_ERR; } diff --git a/source/encoding.c b/source/encoding.c index dc1e3c34a..03dfc2893 100644 --- a/source/encoding.c +++ b/source/encoding.c @@ -89,8 +89,8 @@ int aws_hex_compute_encoded_len(size_t to_encode_len, size_t *encoded_length) { } int aws_hex_encode(const struct aws_byte_cursor *AWS_RESTRICT to_encode, struct aws_byte_buf *AWS_RESTRICT output) { - assert(to_encode->ptr); - assert(output->buffer); + AWS_PRECONDITION(aws_byte_cursor_is_valid(to_encode)); + AWS_PRECONDITION(aws_byte_buf_is_valid(output)); size_t encoded_len = 0; @@ -175,8 +175,8 @@ int aws_hex_compute_decoded_len(size_t to_decode_len, size_t *decoded_len) { } int aws_hex_decode(const struct aws_byte_cursor *AWS_RESTRICT to_decode, struct aws_byte_buf *AWS_RESTRICT output) { - assert(to_decode->ptr); - assert(output->buffer); + AWS_PRECONDITION(aws_byte_cursor_is_valid(to_decode)); + AWS_PRECONDITION(aws_byte_buf_is_valid(output)); size_t decoded_length = 0; diff --git a/tests/byte_buf_test.c b/tests/byte_buf_test.c index 61a6cd9ea..b3cfe7262 100644 --- a/tests/byte_buf_test.c +++ b/tests/byte_buf_test.c @@ -220,9 +220,10 @@ AWS_TEST_CASE(test_buffer_init_copy_null_buffer, s_test_buffer_init_copy_null_bu static int s_test_buffer_init_copy_null_buffer_fn(struct aws_allocator *allocator, void *ctx) { (void)ctx; - struct aws_byte_buf src = {0}; + struct aws_byte_buf src; + AWS_ZERO_STRUCT(src); struct aws_byte_buf dest; - ASSERT_ERROR(AWS_ERROR_INVALID_ARGUMENT, aws_byte_buf_init_copy(&dest, allocator, &src)); + ASSERT_SUCCESS(aws_byte_buf_init_copy(&dest, allocator, &src)); return 0; } diff --git a/tests/encoding_test.c b/tests/encoding_test.c index d55d32bfe..1b210cc7d 100644 --- a/tests/encoding_test.c +++ b/tests/encoding_test.c @@ -71,7 +71,11 @@ static int s_run_hex_encoding_test_case( ASSERT_INT_EQUALS(test_str_size - 1, output_size, "Output size on string should be %d", test_str_size - 1); output.capacity = output_size; + if (output.capacity == 0) { + output.buffer = NULL; + } output.len = 0; + struct aws_byte_cursor expected_buf = aws_byte_cursor_from_array(expected, expected_size - 1); ASSERT_SUCCESS(aws_hex_decode(&expected_buf, &output), "decode call should have succeeded"); @@ -304,6 +308,7 @@ static int s_run_base64_encoding_test_case( ASSERT_INT_EQUALS(expected_size, output_size, "Output size on string should be %d", expected_size); struct aws_byte_cursor to_encode = aws_byte_cursor_from_array(test_str, test_str_size); + struct aws_byte_buf allocation; ASSERT_SUCCESS(aws_byte_buf_init(&allocation, allocator, output_size + 2)); memset(allocation.buffer, 0xdd, allocation.capacity); @@ -333,7 +338,6 @@ static int s_run_base64_encoding_test_case( aws_byte_buf_clean_up(&allocation); /* Part 2: decoding */ - struct aws_byte_cursor expected_cur = aws_byte_cursor_from_array(expected, expected_size - 1); ASSERT_SUCCESS( aws_base64_compute_decoded_len(&expected_cur, &output_size),