Skip to content
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

Jump to bottom

Unbounded proof and contracts for s2n_constant_time_equals #4704

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open

Unbounded proof and contracts for s2n_constant_time_equals #4704

wants to merge 8 commits into from

Commits on Aug 13, 2024

  1. Update Makefile.common from PR#4703 to work with unbounded proofs 

    Signed-off-by: Rod Chapman <[email protected]>
    @rod-chapman
    rod-chapman committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    d924397 View commit details
    Browse the repository at this point in the history

  2. Add CONTRACT_DECREASES macro for unbounded loop proofs. 

    Signed-off-by: Rod Chapman <[email protected]>
    @rod-chapman
    rod-chapman committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    08adf1d View commit details
    Browse the repository at this point in the history

  3. Add new partial and total versions of s2n_constant_time_equals and th… 

    …eir proofs.

Signed-off-by: Rod Chapman <[email protected]>
    @rod-chapman
    rod-chapman committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    e45bc83 View commit details
    Browse the repository at this point in the history

  4. Correct specification, contracts and code for case when len == 0 

    Signed-off-by: Rod Chapman <[email protected]>
    @rod-chapman
    rod-chapman committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    1633e5d View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2024

  1. Merge branch 'aws:main' into unbound_ct_equals

    @rod-chapman
    rod-chapman authored Aug 14, 2024
    Configuration menu
    Copy the full SHA
    57910fa View commit details
    Browse the repository at this point in the history

  2. Address review comments from colmmac: 

    1. Test and return early from s2n_constant_time_equals_total() when either a or b is NULL
2. Remove declaration of s2n_constant_time_equals_partial() from s2n_safety.h
   and make it "static" in the body of this translation unit. Update contracts accordingly.

Signed-off-by: Rod Chapman <[email protected]>
    @rod-chapman
    rod-chapman committed Aug 14, 2024
    Configuration menu
    Copy the full SHA
    976761d View commit details
    Browse the repository at this point in the history

  3. Tell goto-cc not to export file-local symbols to complete this proof 

    Signed-off-by: Rod Chapman <[email protected]>
    @rod-chapman
    rod-chapman committed Aug 14, 2024
    Configuration menu
    Copy the full SHA
    1b2dddc View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2024

  1. Update utils/s2n_safety.c 

    Correct typo in comment only.

Co-authored-by: Sam Clark <[email protected]>
    @rod-chapman @goatgoose
    rod-chapman and goatgoose authored Sep 10, 2024
    Configuration menu
    Copy the full SHA
    0ed160a View commit details
    Browse the repository at this point in the history