From b9cd276def26bb00a94dcb3b6f0e554a5bf4b168 Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Wed, 17 Jul 2024 10:39:42 -0700 Subject: [PATCH] test(cbmc): add stuffer hex proofs --- .../cbmc/proofs/s2n_stuffer_read_hex/Makefile | 40 ++++++++++ .../s2n_stuffer_read_hex/cbmc-proof.txt | 1 + .../s2n_stuffer_read_hex_harness.c | 66 +++++++++++++++++ .../s2n_stuffer_read_uint16_hex/Makefile | 39 ++++++++++ .../cbmc-proof.txt | 1 + .../s2n_stuffer_read_uint16_hex_harness.c | 44 +++++++++++ .../s2n_stuffer_read_uint8_hex/Makefile | 39 ++++++++++ .../s2n_stuffer_read_uint8_hex/cbmc-proof.txt | 1 + .../s2n_stuffer_read_uint8_hex_harness.c | 44 +++++++++++ .../proofs/s2n_stuffer_write_hex/Makefile | 40 ++++++++++ .../s2n_stuffer_write_hex/cbmc-proof.txt | 1 + .../s2n_stuffer_write_hex_harness.c | 74 +++++++++++++++++++ .../s2n_stuffer_write_uint16_hex/Makefile | 37 ++++++++++ .../cbmc-proof.txt | 1 + .../s2n_stuffer_write_uint16_hex_harness.c | 63 ++++++++++++++++ .../s2n_stuffer_write_uint8_hex/Makefile | 37 ++++++++++ .../cbmc-proof.txt | 1 + .../s2n_stuffer_write_uint8_hex_harness.c | 63 ++++++++++++++++ 18 files changed, 592 insertions(+) create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/s2n_stuffer_read_uint16_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/s2n_stuffer_read_uint8_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_hex/s2n_stuffer_write_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/s2n_stuffer_write_uint16_hex_harness.c create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/s2n_stuffer_write_uint8_hex_harness.c diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile new file mode 100644 index 00000000000..9927b0ef4f8 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile @@ -0,0 +1,40 @@ +# Copyright 2020 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +MAX_BLOB_SIZE = 4 +DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE) + +PROOF_UID = s2n_stuffer_read_hex +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)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.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 += s2n_stuffer_read_hex.8:$(MAX_BLOB_SIZE) + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c new file mode 100644 index 00000000000..461decca069 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c @@ -0,0 +1,66 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_read_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *bytes_out = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(bytes_out))); + + struct s2n_blob *hex_in = cbmc_allocate_s2n_blob(); + __CPROVER_assume(s2n_result_is_ok(s2n_blob_validate(hex_in))); + __CPROVER_assume(s2n_blob_is_bounded(hex_in, MAX_BLOB_SIZE)); + + struct s2n_stuffer old_bytes_out = *bytes_out; + struct store_byte_from_buffer old_bytes_out_byte = { 0 }; + save_byte_from_blob(&bytes_out->blob, &old_bytes_out_byte); + __CPROVER_assume(old_bytes_out_byte.idx < bytes_out->write_cursor); + + struct s2n_blob old_hex_in = *hex_in; + struct store_byte_from_buffer old_hex_in_byte = { 0 }; + save_byte_from_blob(hex_in, &old_hex_in_byte); + + s2n_result result = s2n_stuffer_read_hex(bytes_out, hex_in); + + struct s2n_stuffer expected_bytes_out = old_bytes_out; + struct s2n_blob expected_hex_in = old_hex_in; + + /* On success, the byte equivalent of the hex was written to the stuffer */ + if (s2n_result_is_ok(result)) { + expected_bytes_out.write_cursor += old_hex_in.size / 2; + expected_bytes_out.high_water_mark = MAX(old_bytes_out.write_cursor, + old_bytes_out.high_water_mark); + + } + + /* Memory may be allocated on either success or failure, + * because we allocated the memory before we start writing. */ + if (bytes_out->blob.size > old_bytes_out.blob.size) { + expected_bytes_out.blob = bytes_out->blob; + } + + assert(s2n_result_is_ok(s2n_stuffer_validate(bytes_out))); + assert_stuffer_equivalence(bytes_out, &expected_bytes_out, &old_bytes_out_byte); + assert(s2n_result_is_ok(s2n_blob_validate(hex_in))); + assert_blob_equivalence(hex_in, &expected_hex_in, &old_hex_in_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile new file mode 100644 index 00000000000..1952ae9eb72 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile @@ -0,0 +1,39 @@ +# Copyright 2020 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_read_uint16_hex +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)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.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 + +REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl + +UNWINDSET += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_read_n_bytes.14:5 + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/s2n_stuffer_read_uint16_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/s2n_stuffer_read_uint16_hex_harness.c new file mode 100644 index 00000000000..97211bbd47e --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/s2n_stuffer_read_uint16_hex_harness.c @@ -0,0 +1,44 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_read_uint16_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_in = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_in))); + + struct s2n_stuffer old_hex_in = *hex_in; + struct store_byte_from_buffer old_byte = { 0 }; + save_byte_from_blob(&hex_in->blob, &old_byte); + + uint16_t out; + s2n_stuffer_read_uint16_hex(hex_in, &out); + + size_t expected_read = 4; + struct s2n_stuffer expected_hex_in = old_hex_in; + if (expected_hex_in.write_cursor >= expected_hex_in.read_cursor + expected_read) { + expected_hex_in.read_cursor += expected_read; + } + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_in))); + assert_stuffer_equivalence(hex_in, &expected_hex_in, &old_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile new file mode 100644 index 00000000000..6c05e6c3fdd --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile @@ -0,0 +1,39 @@ +# Copyright 2020 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_read_uint8_hex +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)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.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 + +REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl + +UNWINDSET += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_read_n_bytes.14:3 + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/s2n_stuffer_read_uint8_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/s2n_stuffer_read_uint8_hex_harness.c new file mode 100644 index 00000000000..0738499a4f3 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/s2n_stuffer_read_uint8_hex_harness.c @@ -0,0 +1,44 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_read_uint8_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_in = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_in))); + + struct s2n_stuffer old_hex_in = *hex_in; + struct store_byte_from_buffer old_byte = { 0 }; + save_byte_from_blob(&hex_in->blob, &old_byte); + + uint8_t out; + s2n_stuffer_read_uint8_hex(hex_in, &out); + + size_t expected_read = 2; + struct s2n_stuffer expected_hex_in = old_hex_in; + if (expected_hex_in.write_cursor >= expected_hex_in.read_cursor + expected_read) { + expected_hex_in.read_cursor += expected_read; + } + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_in))); + assert_stuffer_equivalence(hex_in, &expected_hex_in, &old_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile new file mode 100644 index 00000000000..5d245445c13 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile @@ -0,0 +1,40 @@ +# Copyright 2020 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +MAX_BLOB_SIZE = 4 +DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE) + +PROOF_UID = s2n_stuffer_write_hex +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)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.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 += s2n_stuffer_write_hex.3:$(call addone,$(MAX_BLOB_SIZE)) + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_write_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/s2n_stuffer_write_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_write_hex/s2n_stuffer_write_hex_harness.c new file mode 100644 index 00000000000..6b5bdc20a1c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/s2n_stuffer_write_hex_harness.c @@ -0,0 +1,74 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_write_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_out = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + + struct s2n_blob *bytes_in = cbmc_allocate_s2n_blob(); + __CPROVER_assume(s2n_result_is_ok(s2n_blob_validate(bytes_in))); + __CPROVER_assume(s2n_blob_is_bounded(bytes_in, MAX_BLOB_SIZE - 1)); + + size_t expected_written = bytes_in->size * 2; + size_t test_offset = nondet_size_t(); + __CPROVER_assume(0 <= test_offset); + __CPROVER_assume(test_offset < expected_written); + + struct s2n_stuffer old_hex_out = *hex_out; + struct store_byte_from_buffer old_hex_out_byte = { 0 }; + save_byte_from_blob(&hex_out->blob, &old_hex_out_byte); + __CPROVER_assume(old_hex_out_byte.idx < hex_out->write_cursor); + + struct s2n_blob old_bytes_in = *bytes_in; + struct store_byte_from_buffer old_bytes_in_byte = { 0 }; + save_byte_from_blob(bytes_in, &old_bytes_in_byte); + + s2n_result result = s2n_stuffer_write_hex(hex_out, bytes_in); + + struct s2n_stuffer expected_hex_out = old_hex_out; + struct s2n_blob expected_bytes_in = old_bytes_in; + + if (s2n_result_is_ok(result)) { + /* On success, the hex equivalent of the bytes is written to the stuffer */ + expected_hex_out.write_cursor += expected_written; + expected_hex_out.high_water_mark = MAX(expected_hex_out.write_cursor, + old_hex_out.high_water_mark); + + /* Any new bytes written should match the expected hex pattern */ + uint8_t c = hex_out->blob.data[old_hex_out.write_cursor + test_offset]; + assert(('0' <= c && c <= '9') || ('a' <= c && c <= 'f')); + } + + /* Memory may be allocated on either success or failure, + * because we allocated the memory before we start writing. */ + if (hex_out->blob.size > old_hex_out.blob.size) { + expected_hex_out.blob = hex_out->blob; + } + + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + assert_stuffer_equivalence(hex_out, &expected_hex_out, &old_hex_out_byte); + assert(s2n_result_is_ok(s2n_blob_validate(bytes_in))); + assert_blob_equivalence(bytes_in, &expected_bytes_in, &old_bytes_in_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile new file mode 100644 index 00000000000..255787c81b9 --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile @@ -0,0 +1,37 @@ +# Copyright 2020 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_write_uint16_hex +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)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.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 += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_write_n_bytes.4:5 + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/s2n_stuffer_write_uint16_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/s2n_stuffer_write_uint16_hex_harness.c new file mode 100644 index 00000000000..cf40ee82fae --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/s2n_stuffer_write_uint16_hex_harness.c @@ -0,0 +1,63 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_write_uint16_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_out = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + + struct s2n_stuffer old_hex_out = *hex_out; + struct store_byte_from_buffer old_hex_out_byte = { 0 }; + save_byte_from_blob(&hex_out->blob, &old_hex_out_byte); + __CPROVER_assume(old_hex_out_byte.idx < hex_out->write_cursor); + + uint16_t byte_in = nondet_uint16_t(); + s2n_result result = s2n_stuffer_write_uint16_hex(hex_out, byte_in); + + struct s2n_stuffer expected_hex_out = old_hex_out; + size_t expected_written = 4; + size_t test_offset = nondet_size_t(); + __CPROVER_assume(0 <= test_offset); + __CPROVER_assume(test_offset < expected_written); + + if (s2n_result_is_ok(result)) { + /* On success, the hex equivalent of the bytes is written to the stuffer */ + expected_hex_out.write_cursor += expected_written; + expected_hex_out.high_water_mark = MAX(expected_hex_out.write_cursor, + old_hex_out.high_water_mark); + + /* New bytes written should match the expected hex pattern */ + uint8_t c = hex_out->blob.data[old_hex_out.write_cursor + test_offset]; + assert(('0' <= c && c <= '9') || ('a' <= c && c <= 'f')); + } + + /* Memory may be allocated on either success or failure, + * because we allocated the memory before we start writing. */ + if (hex_out->blob.size > old_hex_out.blob.size) { + expected_hex_out.blob = hex_out->blob; + } + + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + assert_stuffer_equivalence(hex_out, &expected_hex_out, &old_hex_out_byte); +} diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile new file mode 100644 index 00000000000..6a5695128fc --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile @@ -0,0 +1,37 @@ +# Copyright 2020 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. + +########### +#Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_stuffer_write_uint8_hex +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)/s2n_calculate_stacktrace.c + +PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.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 += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_write_n_bytes.4:3 + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/cbmc-proof.txt b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/s2n_stuffer_write_uint8_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/s2n_stuffer_write_uint8_hex_harness.c new file mode 100644 index 00000000000..6d5372cea7c --- /dev/null +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/s2n_stuffer_write_uint8_hex_harness.c @@ -0,0 +1,63 @@ +/* + * Copyright 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include +#include +#include + +#include "api/s2n.h" +#include "stuffer/s2n_stuffer.h" + +void s2n_stuffer_write_uint8_hex_harness() +{ + nondet_s2n_mem_init(); + + struct s2n_stuffer *hex_out = cbmc_allocate_s2n_stuffer(); + __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + + struct s2n_stuffer old_hex_out = *hex_out; + struct store_byte_from_buffer old_hex_out_byte = { 0 }; + save_byte_from_blob(&hex_out->blob, &old_hex_out_byte); + __CPROVER_assume(old_hex_out_byte.idx < hex_out->write_cursor); + + uint8_t byte_in = nondet_uint8_t(); + s2n_result result = s2n_stuffer_write_uint8_hex(hex_out, byte_in); + + struct s2n_stuffer expected_hex_out = old_hex_out; + size_t expected_written = 2; + size_t test_offset = nondet_size_t(); + __CPROVER_assume(0 <= test_offset); + __CPROVER_assume(test_offset < expected_written); + + if (s2n_result_is_ok(result)) { + /* On success, the hex equivalent of the bytes is written to the stuffer */ + expected_hex_out.write_cursor += expected_written; + expected_hex_out.high_water_mark = MAX(expected_hex_out.write_cursor, + old_hex_out.high_water_mark); + + /* New bytes written should match the expected hex pattern */ + uint8_t c = hex_out->blob.data[old_hex_out.write_cursor + test_offset]; + assert(('0' <= c && c <= '9') || ('a' <= c && c <= 'f')); + } + + /* Memory may be allocated on either success or failure, + * because we allocated the memory before we start writing. */ + if (hex_out->blob.size > old_hex_out.blob.size) { + expected_hex_out.blob = hex_out->blob; + } + + assert(s2n_result_is_ok(s2n_stuffer_validate(hex_out))); + assert_stuffer_equivalence(hex_out, &expected_hex_out, &old_hex_out_byte); +}