Search results

Add pointer-overflow check for slow proofs

cbmcCBMC proof related workCBMC proof related work

high priorityNeeds attention before low-mediumNeeds attention before low-medium

Status: Open.

#704 In aws/aws-encryption-sdk-c;

· feliperodri opened on May 21, 2021

Determine performance impact of using (init|clean|clear_up) list source functions

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#690 In aws/aws-encryption-sdk-c;

· adpaco-aws opened on Jan 19, 2021

Standardize CBMC stub filenames

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#686 In aws/aws-encryption-sdk-c;

· adpaco-aws opened on Jan 11, 2021

Remove CBMC validator functions

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#685 In aws/aws-encryption-sdk-c;

· adpaco-aws opened on Jan 11, 2021

Investigate how to move assumptions out of <code>ensure_...</code> functions

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#675 In aws/aws-encryption-sdk-c;

· adpaco-aws opened on Dec 22, 2020

Improve documentation of DEFINES across all CBMC proofs

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#669 In aws/aws-encryption-sdk-c;

· tegansb opened on Dec 15, 2020

Update CBMC proofs when allocator functions are updated in c-common

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#668 In aws/aws-encryption-sdk-c;

· tegansb opened on Dec 15, 2020

Expose which_sha implementation to avoid duplicated in CBMC

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#666 In aws/aws-encryption-sdk-c;

· adpaco-aws opened on Dec 10, 2020

Move aws_byte_buf_contents_match to AWS C-common

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#665 In aws/aws-encryption-sdk-c;

· adpaco-aws opened on Dec 10, 2020

Rename all CBMC proof allocators

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#662 In aws/aws-encryption-sdk-c;

· feliperodri opened on Dec 9, 2020

Avoid usage of __CPROVER_havoc_object

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#653 In aws/aws-encryption-sdk-c;

· adpaco-aws opened on Dec 3, 2020

Add templates submodule for libcrypto

cbmcCBMC proof related workCBMC proof related work

Status: Open.

#652 In aws/aws-encryption-sdk-c;

· adpaco-aws opened on Dec 3, 2020