aws / aws/aws-encryption-sdk-c

CBMC proof stubs do not replace included functions

Open
#624 1 comment 0 reactions 0 assignees View on GitHub
cbmc
Dominant language
C
Stars
63
Forks
59
PR merge metrics
No merged PRs in 30d

Description

In the `aws_cryptosdk_keyring_release` CBMC proof, a few stubs coming from `stubs/` are added to proof sources but not able to replace the corresponding functions coming from `INCLUDES`. Below is the Makefile code.

```
# aws_atomic_fetch_sub_explicit receives a volatile input, which is always model
# as non-deterministic in CBMC; thus, we need a deterministic stub for it
PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_fetch_sub_explicit.c
REMOVE_FUNCTION_BODY += aws_atomic_fetch_sub_explicit

PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_load_int.c
REMOVE_FUNCTION_BODY += aws_atomic_load_int

PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_priv_xlate_order.c
REMOVE_FUNCTION_BODY += aws_atomic_priv_xlate_order

PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c

HARNESS_ENTRY = aws_cryptosdk_keyring_release_harness
HARNESS_FILE = $(HARNESS_ENTRY).c

PROOF_SOURCES += $(HARNESS_FILE)

REMOVE_FUNCTION_BODY += hash_proof_destroy_noop
REMOVE_FUNCTION_BODY += aws_raise_error_private
```

We have tried to force removal by adding
```
REMOVE_FUNCTION_BODY += __CPROVER_file_local_atomics_gnu_inl_aws_atomic_fetch_sub_explicit$link5
```
which is the name given to the function already included. We have also tried with similar names with different escape sequences.

This could be related to #625

Contributor guide

Open the contributing guide

Research direction

Start with the aws_cryptosdk_keyring_release CBMC proof Makefile entries, the stubs under stubs/, and the functions listed in REMOVE_FUNCTION_BODY. Compare how functions from INCLUDES are selected and removed, including the __CPROVER_file_local_atomics_gnu_inl_aws_atomic_fetch_sub_explicit$link5 name, and review related issue #625. Done means the intended stubs replace the included functions in this proof.

Written by the indexing model from the issue text.

Assessment

Tech stack
c
Domain
build-system, testing
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.