Unbounded proof and contracts for s2n_constant_time_equals #4704
Conversation
Signed-off-by: Rod Chapman <[email protected]>
Signed-off-by: Rod Chapman <[email protected]>
…eir proofs. Signed-off-by: Rod Chapman <[email protected]>
Signed-off-by: Rod Chapman <[email protected]>
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]>
Signed-off-by: Rod Chapman <[email protected]>
| bool s2n_constant_time_equals_total(const uint8_t* const a, | ||
| const uint8_t* const b, | ||
| const uint32_t len) |
There was a problem hiding this comment.
Is there a reason to keep s2n_constant_time_equals in addition to s2n_constant_time_equals_total?
There was a problem hiding this comment.
I planned to keep to old version until the other s2n-tls developers are happy with the new version.
There was a problem hiding this comment.
The CBMC results uploaded to the Github action summary indicates that this harness has 0% code coverage:
Is there potentially an issue with this harness? The s2n_constant_time_equals_total harness looks okay. Is there maybe an issue with forward declaring s2n_constant_time_equals_partial() since it's static?
| @@ -148,6 +149,7 @@ void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size); | |||
| #define CONTRACT_ASSIGNS(...) | |||
| #define CONTRACT_ASSIGNS_ERR(...) | |||
| #define CONTRACT_ASSUME(...) | |||
| #define CONTRACT_DECREASES(...) | |||
There was a problem hiding this comment.
It looks like the sidetrail tests are failing to build with these changes. It looks like s2n_ensure.h might need to be included in the sidetrail harnesses?
Correct typo in comment only. Co-authored-by: Sam Clark <[email protected]>
This PR contributes a refactoring of s2n_constant_time_equals() into two functions:
s2_constant_time_equals_partial(), which is efficient and readable, but has an explicit pre-condition.
s2n_constant_time_equals_total(), which is equivalent to the existing s2n_constant_time_equals(), adding
the necessary defensive checks that are required to meet the pre-condition of the earlier version.
We also add unbounded proofs of these functions here, using contracts and loop invariants.
No existing other code has been changed (no calls to s2n_constant_time_equals() have been modified, and the
original function remains unmodified) so no change to existing behaviour.
This PR is mainly to illustrate the use of contract "defensive proof" programming style.