-
Notifications
You must be signed in to change notification settings - Fork 96
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.
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
Everest integration #140
Everest integration #140
Conversation
a2d1cc8
to
e6707db
Compare
On the CI the crypto job is passing, the TLS part of the pr jobs is failing, because the Mbed TLS build scripts seem to pick up the the TLS version of the crypto related headers and not the crypto version. (Changing this might make sense since crypto does not have the ssl headers anymore, but since the crypto files will be deleted soon, I don't think it is worth the effort.) |
Just checking: could you give us a rough idea of when this will be merged? |
Splitting the repository into Mbed TLS and Mbed Crypto complicated things: This PR is the part of the changes that need to go in Mbed Crypto. There is another part that needs to go in Mbed TLS. Before we could raise this second PR, we need to finish up a splitting related task in Mbed TLS first. Once it is done we will raise the second PR as soon as possible and we can get both of them merged. |
Sounds good, thanks for the update! |
@yanesca any update on this PR? We would be very keen to pick up a release of mbedtls with these changes in for our project. |
These files are automatically generated by the Everest toolchain from F* files. They do not respect the mbedTLS code style guidelines as manual modification would invalidate verification guarantees. The files in 3rdparty/everest/include/kremli{n,b} are a customized (minimzed) version of the support headers expected by the code extracted using KreMLin.
This allows the use of #ifdef ... #endif in enum definitions (e.g., mbedtls_ecdh_variant in ecdh.h).
This being the first 3rdparty-contribution, we may want to consider the structure of the project file generation scripts. Perhaps add small, constribution-specific scripts to each directory in 3rdparty instead of adding all constraints to generate_visualc_files.pl?
e6707db
to
c25df68
Compare
@achamayou I have rebased this PR, I'll still need to fix the CI failures (if any) and rebase Mbed-TLS/mbedtls#2073 before we could do the reviews and eventually merge. |
CI is only failing, because the PSA API is out of sync between Mbed TLS and Mbed Crypto. This is going to be resolved after merging Mbed-TLS/mbedtls#2767. |
@yanesca thank you for the update, we look forward to using x25519 in mbedtls. |
The CI fails only on the |
At this point Mbed TLS and Mbed Crypto headers with the same name, including the Mbed Crypto headers in `everest_inc` breaks Mbed TLS builds.
API checking fails on the head, because the development has been updated since the PR had been raised. Merging to development should fix this failure. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've reviewed this by comparing it to the approved PR at Mbed-TLS/mbedtls#2073, this PR implements all the relevant parts in the same manner.
I see a check-names failure. Anything we can do to avoid it?
|
@Patater That failure is in the TLS tests, and uses TLS's scripts that can't be updated by this PR but are updated by Mbed-TLS/mbedtls#2799. The failures should go away when 2799 is merged into Mbed TLS. (PR2799 uses this PR as a submodule and the CI is green over there.) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
Before merge, we should have automated tests for Everest crypto on Windows.
@wintersteiger Thanks a lot for your contribution! And especially thanks for your patience working with us to get this in. Much appreciated! |
Many thanks for getting this merged! It took a little longer than expected, but we're very happy it's now in! |
This PR is the result of rebasing Mbed-TLS/mbedtls#2073 on the top of Mbed Crypto development.
This PR has to be merged shortly before Mbed-TLS/mbedtls#2799 to avoid CI failures.