feat: add EVP_MD_fetch #46
Conversation
| @@ -706,6 +707,35 @@ const EVP_MD *EVP_sha512() { | |||
| return &md; | |||
| } | |||
|
|
|||
| EVP_MD *EVP_MD_fetch(OSSL_LIB_CTX *ctx, const char *algorithm, const char *properties) { | |||
| // Assume this method is always called without a library context | |||
There was a problem hiding this comment.
Should this be:
| // Assume this method is always called without a library context | |
| // Assume this method is never called without a library context |
?
There was a problem hiding this comment.
... as written, yes. But actually I meant to assume the ctx is always NULL. s2n-tls always calls it with NULL. Let me investigate why this is working. s2n-tls's proofs wouldn't have cared about my other dumb mistakes, but this one they really should have cared about.
|
Welp turns out the reason #46 (comment) didn't break this is that my code isn't actually calling EVP_MD_fetch in CBMC 🙃 Our code has feature probes and conditional compilation to handle methods like EVP_MD_fetch that might not exist in old versions of the libcrypto, and CBMC only ever proves the branch that assumes new features are unavailable. So it's proving our non-EVP_MD_fetch branch and completely ignoring my shiny new stub: https://github.com/aws/s2n-tls/blob/2a4c4ab0b5678c66caf674982ad8a1ec8402d56b/crypto/s2n_hash.c#L48-L84 That means we can close this PR, but the lack of coverage seems like a worse problem :/ Is there a way to handle conditional compilation better with CBMC? |
Issue #, if available: None
Description of changes:
s2n-tls needs to call the new openssl3 method EVP_MD_fetch, so this adds it to the model.
Should this method non-deterministically return NULL? I considered this since openssl3 providers might not support even common algorithms like SHA256. But the existing model already assumes EVP_sha256() never returns NULL, and in openssl3 EVP_sha256() is just a wrapper around EVP_MD_fetch(). Also, the rest of the model methods do
assert(md != NULL)rather than returning an error signal when md == NULL, which causes problems if we start unpredictably returning NULLs for mds all over the place. Just making EVP_MD_fetch() a wrapper around the existing EVP md methods seems like the simplest solution.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.