BIKE SAW Memory Safety Properties #5
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…IKE as a part of s2n and run one sanity test. Update BIKE with Makefiles to fix Travis build Remove inline complier warning suppression, use compiler flags instead. Do not include bike types.h in external files
…x other issues from clang build and FIPS openssl build Do not compile post-quantum algorithms when using FIPS OpenSSL
1. Print pid in print_s2n_error function 2. Set SA_NOCLDWAIT to prevent creating zombies 3. close fd in the main event loop after forking
… findings to move to other places.
Make CertificateStatus optional in client mode According to RFC6066 Section 8, server may choose not to send "CertificateStatus" message even if it has sent "status_request" extension in ServerHello message.
…xtension Add client supported_versions extension
1. Skip unsupported extensions 2. Use a bitmask to perform the uniqueness check
Use CMake pthreads (Threads) package to manage pthreads dependency
| crypto_kem_dec_unsuccessful_spec; | ||
|
|
||
| // NOTE: Step 1 of 2 - conditioned on a SUCCESS result | ||
| // crypto_kem_dec_successful_ov <- verify_unint "BIKE1_L1_crypto_kem_dec" |
| /////////////////////////////////////////////////////////////////////////////// | ||
| // Proof commands | ||
|
|
||
| // verify "convert_to_redundant_rep" [] (convert_to_redundant_rep_spec 1); |
| verify_pathsat "__breakpoint__generate_sparse_fake_rep_first_loop#generate_sparse_fake_rep" | ||
| generate_sparse_fake_rep_O | ||
| generate_sparse_fake_rep_first_loop_spec; | ||
| // verify_pathsat "__breakpoint__generate_sparse_fake_rep_second_loop#generate_sparse_fake_rep" |
| @@ -44,7 +44,7 @@ let count_ones_spec n = do { | |||
| /////////////////////////////////////////////////////////////////////////////// | |||
| // Proof commands | |||
|
|
|||
| // verify "convert_to_redundant_rep" [] (convert_to_redundant_rep_spec 1); | |||
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Issue # (if available):
Description of changes:
This pull request adds SAW scripts for BIKE Memory Safety Properties.
A couple of adaptations had to be done in the build process to accommodate both SIKE and BIKE tests to run independently.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.