test(cbmc): add stuffer hex proofs

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

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

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

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 <assert.h>
+#include <cbmc_proof/cbmc_utils.h>
+#include <cbmc_proof/make_common_datastructures.h>
+
+#include "api/s2n.h"
+#include "stuffer/s2n_stuffer.h"
+
+void s2n_stuffer_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);
+}

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

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

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

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 <assert.h>
+#include <cbmc_proof/cbmc_utils.h>
+#include <cbmc_proof/make_common_datastructures.h>
+
+#include "api/s2n.h"
+#include "stuffer/s2n_stuffer.h"
+
+void s2n_stuffer_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);
+}

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

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

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

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 <assert.h>
+#include <cbmc_proof/cbmc_utils.h>
+#include <cbmc_proof/make_common_datastructures.h>
+
+#include "api/s2n.h"
+#include "stuffer/s2n_stuffer.h"
+
+void s2n_stuffer_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);
+}

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

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

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