Skip to content

chore: update aws-c-common dependency for CBMC proofs #776

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

chore: update aws-c-common dependency for CBMC proofs #776

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3eda136
chore: use built-in SAT solver for CBMC proofs
tautschnig Apr 24, 2024
669f115
chore: update aws-c-common dependency for CBMC proofs
tautschnig Apr 22, 2024
ca6a7df
chore: compile for CBMC with warnings-as-errors
tautschnig Apr 22, 2024
455984a
Update CBMC version, verbose
tautschnig Apr 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 1 addition & 3 deletions .github/workflows/proof_ci.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,10 +152,8 @@ jobs:
echo "$(pwd)" >> $GITHUB_PATH
- name: Run CBMC proofs
shell: bash
env:
EXTERNAL_SAT_SOLVER: kissat
working-directory: ${{ env.PROOFS_DIR }}
run: ${{ env.RUN_CBMC_PROOFS_COMMAND }}
run: ${{ env.RUN_CBMC_PROOFS_COMMAND }} --verbose --debug
- name: Check repository visibility
shell: bash
run: |
Expand Down
2 changes: 1 addition & 1 deletion aws-encryption-sdk-specification
Open in desktop
Submodule aws-encryption-sdk-specification updated 93 files
+0 −5 .github/CODEOWNERS
+0 −4 .github/PULL_REQUEST_TEMPLATE.md
+1 −1 .github/workflows/ci_static-analysis.yaml
+1 −7 .gitignore
+0 −2 .prettierignore
+0 −91 README.md
+1 −1 changes/2020-05-13_remove-keyring-trace/change.md
+8 −8 changes/2020-06-09_wrapping-key-identifiers/change.md
+0 −301 changes/2022-06-19_seperate_material_providers/background.md
+0 −130 changes/2022-06-19_seperate_material_providers/change.md
+0 −441 changes/2022-11-14_encryption_context_on_decrypt/background.md
+0 −259 changes/2022-11-14_encryption_context_on_decrypt/encryption_context_use_cases.md
+0 −360 changes/2022-11-14_encryption_context_on_decrypt/proposal.md
+0 −217 changes/2023-06-19_thread_safe_cache/background.md
+0 −196 changes/2023-06-19_thread_safe_cache/change.md
+0 −286 changes/2023_7_12_update-keystore-structure/background.md
+0 −150 changes/2023_7_12_update-keystore-structure/proposal.md
+1 −1 ci/prettify.sh
+0 −100 client-apis/client.md
+9 −58 client-apis/decrypt.md
+31 −94 client-apis/encrypt.md
+178 −0 compliance/framework/aws-kms/aws-kms-key-arn.txt
+79 −0 compliance/framework/aws-kms/aws-kms-key-arn/2.5.toml
+47 −0 compliance/framework/aws-kms/aws-kms-key-arn/2.8.toml
+52 −0 compliance/framework/aws-kms/aws-kms-key-arn/2.9.toml
+123 −0 compliance/framework/aws-kms/aws-kms-mrk-are-unique.txt
+48 −0 compliance/framework/aws-kms/aws-kms-mrk-are-unique/2.5.toml
+233 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider.txt
+14 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.5.toml
+102 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.6.toml
+182 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.7.toml
+50 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.8.toml
+106 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.9.toml
+225 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key.txt
+81 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.10.toml
+63 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.11.toml
+14 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.5.toml
+64 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.6.toml
+12 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.7.toml
+12 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.8.toml
+179 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.9.toml
+194 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings.txt
+98 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings/2.5.toml
+163 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings/2.6.toml
+311 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt
+14 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.5.toml
+42 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.6.toml
+258 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.7.toml
+217 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.8.toml
+212 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring.txt
+14 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.5.toml
+61 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.6.toml
+12 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.7.toml
+258 −0 compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.8.toml
+110 −0 compliance/framework/aws-kms/aws-kms-mrk-match-for-decrypt.txt
+48 −0 compliance/framework/aws-kms/aws-kms-mrk-match-for-decrypt/2.5.toml
+3 −1 data-format/message-body.md
+46 −68 data-format/message-header.md
+1 −4 data-format/message.md
+0 −44 framework/README.md
+89 −449 framework/algorithm-suites.md
+0 −112 framework/aws-kms/aws-kms-discovery-keyring.md
+0 −403 framework/aws-kms/aws-kms-hierarchical-keyring.md
+0 −166 framework/aws-kms/aws-kms-keyring.md
+30 −29 framework/aws-kms/aws-kms-mrk-aware-multi-keyrings.md
+36 −36 framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.md
+20 −20 framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring.md
+1 −1 framework/aws-kms/aws-kms-mrk-match-for-decrypt.md
+0 −109 framework/aws-kms/aws-kms-multi-keyrings.md
+0 −267 framework/aws-kms/aws-kms-rsa-keyring.md
+0 −636 framework/branch-key-store.md
+4 −3 framework/caching-cmm.md
+8 −57 framework/cmm-interface.md
+0 −110 framework/commitment-policy.md
+13 −91 framework/cryptographic-materials-cache.md
+25 −48 framework/default-cmm.md
+24 −41 framework/keyring-interface.md
+395 −0 framework/kms-keyring.md
+16 −10 framework/local-cryptographic-materials-cache.md
+12 −9 framework/multi-keyring.md
+24 −35 framework/raw-aes-keyring.md
+6 −6 framework/raw-rsa-keyring.md
+0 −104 framework/required-encryption-context-cmm.md
+0 −162 framework/storm-tracking-cryptographic-materials-cache.md
+8 −239 framework/structures.md
+0 −38 framework/synchronized-local-cryptographic-materials-cache.md
+0 −113 framework/transitive-requirements.md
+0 −0 proposals/2020-07-01_aws-kms-keyring-redesign/background.md
+3 −3 proposals/2020-07-01_aws-kms-keyring-redesign/change.md
+0 −68 proposals/2022-10-27_rsa-keyring-v2/proposal.md
+12 −20 util/extract.js
+1 −1 util/report.js
+0 −17 util/specification_extract.sh
2 changes: 1 addition & 1 deletion verification/cbmc/aws-c-common
Open in desktop
Submodule aws-c-common updated 896 files
1 change: 0 additions & 1 deletion verification/cbmc/include/make_common_data_structures.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@
#include <aws/cryptosdk/private/header.h>
#include <aws/cryptosdk/private/hkdf.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>
#include <proof_helpers/utils.h>
#include <stdint.h>
#include <stdlib.h>
Expand Down
23 changes: 0 additions & 23 deletions verification/cbmc/include/proof_allocators.h
View file
Open in desktop

This file was deleted.

4 changes: 2 additions & 2 deletions verification/cbmc/proofs/Makefile.common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -307,8 +307,8 @@ COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
NONDET_STATIC ?=

# Flags to pass to goto-cc for compilation and linking
COMPILE_FLAGS ?= -Wall
LINK_FLAGS ?= -Wall
COMPILE_FLAGS ?= -Wall -Werror
LINK_FLAGS ?= -Wall -Werror
EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols

# Preprocessor include paths -I...
Expand Down
2 changes: 1 addition & 1 deletion verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c

CBMCFLAGS +=

PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
Expand All @@ -38,7 +39,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
Expand Down
2 changes: 1 addition & 1 deletion verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c

CBMCFLAGS +=

PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
Expand All @@ -38,7 +39,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
Expand Down
1 change: 0 additions & 1 deletion verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,6 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
Expand Down
1 change: 0 additions & 1 deletion verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@
#include <aws/cryptosdk/materials.h>
#include <make_common_data_structures.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>
#include <proof_helpers/utils.h>

void aws_cryptosdk_cmm_base_init_harness() {
Expand Down
2 changes: 1 addition & 1 deletion verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c

PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c
Expand Down
13 changes: 6 additions & 7 deletions .../proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@
#include <make_common_data_structures.h>
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>
#include <proof_helpers/utils.h>

// Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed
Expand Down Expand Up @@ -52,7 +51,7 @@ int decrypt_materials(
assert(AWS_OBJECT_PTR_IS_WRITABLE(output));
assert(aws_cryptosdk_dec_request_is_valid(request));

struct aws_cryptosdk_dec_materials *materials = can_fail_malloc(sizeof(*materials));
struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(*materials));
if (materials == NULL) {
*output = NULL;
return AWS_OP_ERR;
Expand Down Expand Up @@ -92,15 +91,15 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
.decrypt_materials = nondet_bool() ? decrypt_materials : NULL };
__CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));

struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(*cmm));
struct aws_cryptosdk_cmm *cmm = malloc(sizeof(*cmm));
__CPROVER_assume(cmm);
cmm->vtable = &vtable;
__CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm));

struct aws_cryptosdk_dec_request *request = can_fail_malloc(sizeof(*request));
struct aws_cryptosdk_dec_request *request = malloc(sizeof(*request));
__CPROVER_assume(request);
request->alloc = can_fail_allocator();
request->enc_ctx = can_fail_malloc(sizeof(*request->enc_ctx));
request->alloc = aws_default_allocator();
request->enc_ctx = malloc(sizeof(*request->enc_ctx));
__CPROVER_assume(request->enc_ctx);
ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);

Expand All @@ -120,7 +119,7 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
*/
__CPROVER_assume(aws_cryptosdk_dec_request_is_valid(request));

struct aws_cryptosdk_dec_materials **output = can_fail_malloc(sizeof(*output));
struct aws_cryptosdk_dec_materials **output = malloc(sizeof(*output));
__CPROVER_assume(output);

// Run the function under test.
Expand Down
2 changes: 1 addition & 1 deletion verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c

PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c
Expand Down
13 changes: 6 additions & 7 deletions ...s_cryptosdk_cmm_generate_enc_materials/aws_cryptosdk_cmm_generate_enc_materials_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@
#include <make_common_data_structures.h>
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>
#include <proof_helpers/utils.h>

// Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed
Expand Down Expand Up @@ -52,7 +51,7 @@ int generate_enc_materials(
assert(AWS_OBJECT_PTR_IS_WRITABLE(output));
assert(aws_cryptosdk_enc_request_is_valid(request));

struct aws_cryptosdk_enc_materials *materials = can_fail_malloc(sizeof(*materials));
struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(*materials));
if (materials == NULL) {
*output = NULL;
return AWS_OP_ERR;
Expand Down Expand Up @@ -107,20 +106,20 @@ void aws_cryptosdk_cmm_generate_enc_materials_harness() {
.decrypt_materials = nondet_voidp() };
__CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));

struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(*cmm));
struct aws_cryptosdk_cmm *cmm = malloc(sizeof(*cmm));
__CPROVER_assume(cmm);
cmm->vtable = &vtable;
__CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm));

struct aws_cryptosdk_enc_request *request = can_fail_malloc(sizeof(*request));
struct aws_cryptosdk_enc_request *request = malloc(sizeof(*request));
__CPROVER_assume(request);
request->alloc = can_fail_allocator();
request->enc_ctx = can_fail_malloc(sizeof(*request->enc_ctx));
request->alloc = aws_default_allocator();
request->enc_ctx = malloc(sizeof(*request->enc_ctx));
__CPROVER_assume(request->enc_ctx);
ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);
__CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request));

struct aws_cryptosdk_enc_materials **output = can_fail_malloc(sizeof(*output));
struct aws_cryptosdk_enc_materials **output = malloc(sizeof(*output));
__CPROVER_assume(output);

// Run the function under test.
Expand Down
1 change: 0 additions & 1 deletion verification/cbmc/proofs/aws_cryptosdk_cmm_release/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
Expand Down
3 changes: 1 addition & 2 deletions verification/cbmc/proofs/aws_cryptosdk_cmm_release/aws_cryptosdk_cmm_release_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@
#include <aws/cryptosdk/materials.h>
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>
#include <proof_helpers/utils.h>

void destroy(struct aws_cryptosdk_cmm *cmm) {
Expand All @@ -36,7 +35,7 @@ void aws_cryptosdk_cmm_release_harness() {
.decrypt_materials = nondet_voidp() };
__CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));

struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(struct aws_cryptosdk_cmm));
struct aws_cryptosdk_cmm *cmm = malloc(sizeof(struct aws_cryptosdk_cmm));

if (cmm) {
cmm->vtable = &vtable;
Expand Down
1 change: 0 additions & 1 deletion verification/cbmc/proofs/aws_cryptosdk_cmm_retain/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
Expand Down
1 change: 0 additions & 1 deletion verification/cbmc/proofs/aws_cryptosdk_cmm_retain/aws_cryptosdk_cmm_retain_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@
#include <aws/cryptosdk/materials.h>
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>
#include <proof_helpers/utils.h>

void aws_cryptosdk_cmm_retain_harness() {
Expand Down
2 changes: 1 addition & 1 deletion verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,13 @@ HARNESS_FILE = $(HARNESS_ENTRY).c

CBMCFLAGS +=

PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c
PROJECT_SOURCES += $(SRCDIR)/source/utils.c

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
Expand Down
2 changes: 1 addition & 1 deletion verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c

PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c
Expand Down
5 changes: 2 additions & 3 deletions .../proofs/aws_cryptosdk_dec_materials_destroy/aws_cryptosdk_dec_materials_destroy_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,13 +23,12 @@
#include <make_common_data_structures.h>
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>
#include <proof_helpers/utils.h>

void aws_cryptosdk_dec_materials_destroy_harness() {
struct aws_cryptosdk_dec_materials *materials = can_fail_malloc(sizeof(*materials));
struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(*materials));
if (materials) {
materials->alloc = can_fail_allocator();
materials->alloc = aws_default_allocator();
__CPROVER_assume(aws_allocator_is_valid(materials->alloc));

// Set up the signctx
Expand Down
2 changes: 1 addition & 1 deletion verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c

PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
Expand Down
3 changes: 1 addition & 2 deletions ...ion/cbmc/proofs/aws_cryptosdk_dec_materials_new/aws_cryptosdk_dec_materials_new_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,11 +20,10 @@
#include <cipher_openssl.h>
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
#include <proof_helpers/make_common_data_structures.h>
#include <proof_helpers/proof_allocators.h>
#include <proof_helpers/utils.h>

void aws_cryptosdk_dec_materials_new_harness() {
struct aws_allocator *alloc = can_fail_allocator();
struct aws_allocator *alloc = aws_default_allocator();
enum aws_cryptosdk_alg_id alg;

struct aws_cryptosdk_dec_materials *rval = aws_cryptosdk_dec_materials_new(alloc, alg);
Expand Down
6 changes: 3 additions & 3 deletions verification/cbmc/proofs/aws_cryptosdk_decrypt_body/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,23 +34,23 @@ CBMCFLAGS +=

DEFINES += -DMAX_BUFFER_SIZE=$(MAX_BUFFER_SIZE)

PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/err_override.c
PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c
PROJECT_SOURCES += $(SRCDIR)/source/cipher.c

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
PROOF_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c

REMOVE_FUNCTION_BODY += EVP_EncryptUpdate
REMOVE_FUNCTION_BODY += EVP_sha256
REMOVE_FUNCTION_BODY += EVP_sha384
REMOVE_FUNCTION_BODY += aws_raise_error_private
REMOVE_FUNCTION_BODY += nondet_compare

UNWINDSET += aws_cryptosdk_decrypt_body.0:$(call addone,$(MAX_BUFFER_SIZE))
Expand Down
10 changes: 5 additions & 5 deletions verification/cbmc/proofs/aws_cryptosdk_decrypt_body/aws_cryptosdk_decrypt_body_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,33 +22,33 @@ void aws_cryptosdk_decrypt_body_harness() {
struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id);
__CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props));

struct aws_byte_buf *outp = can_fail_malloc(sizeof(*outp));
struct aws_byte_buf *outp = malloc(sizeof(*outp));
__CPROVER_assume(outp != NULL);
__CPROVER_assume(aws_byte_buf_is_bounded(outp, MAX_BUFFER_SIZE));
ensure_byte_buf_has_allocated_buffer_member(outp);
__CPROVER_assume(aws_byte_buf_is_valid(outp));

struct aws_byte_cursor *inp = can_fail_malloc(sizeof(*inp));
struct aws_byte_cursor *inp = malloc(sizeof(*inp));
__CPROVER_assume(inp != NULL);
__CPROVER_assume(aws_byte_cursor_is_bounded(inp, MAX_BUFFER_SIZE));
ensure_byte_cursor_has_allocated_buffer_member(inp);
__CPROVER_assume(aws_byte_cursor_is_valid(inp));

struct aws_byte_buf *message_id = can_fail_malloc(sizeof(*message_id));
struct aws_byte_buf *message_id = malloc(sizeof(*message_id));
__CPROVER_assume(message_id != NULL);
__CPROVER_assume(aws_byte_buf_is_bounded(message_id, MAX_BUFFER_SIZE));
ensure_byte_buf_has_allocated_buffer_member(message_id);
__CPROVER_assume(aws_byte_buf_is_valid(message_id));

uint32_t seqno;

uint8_t *iv = can_fail_malloc(props->iv_len);
uint8_t *iv = malloc(props->iv_len);
__CPROVER_assume(iv != NULL);

struct content_key *content_key;

/* Need to allocate tag_len bytes for writing the tag */
uint8_t *tag = can_fail_malloc(props->tag_len);
uint8_t *tag = malloc(props->tag_len);
__CPROVER_assume(tag != NULL);

int body_frame_type;
Expand Down
Loading
Loading