Add unbounded AES-GCM verification #143
Conversation
RyanGlScott
requested review from
apetcher-amazon,
andrewhop and
pennyannn
as code owners
| @@ -40,6 +40,7 @@ AWS libcrypto includes many cryptographic algorithm implementations for several | |||
| | [SHA-2](SPEC.md#SHA-2) | 384 | EVP_DigestInit, EVP_DigestUpdate, EVP_DigestFinal | neoverse-n1, neoverse-v1 | NoEngine, MemCorrect, ArmSpecGap, ToolGap | SAW, NSym | | |||
| | [HMAC](SPEC.md#HMAC-with-SHA-384) | with <nobr>SHA-384</nobr> | HMAC_CTX_init, HMAC_Init_ex, HMAC_Update, HMAC_Final, HMAC | SandyBridge+ | NoEngine, MemCorrect, InitZero, NoInline, CRYPTO_once_Correct | SAW | | |||
| | [<nobr>AES-KW(P)</nobr>](SPEC.md#AES-KWP) | 256 | AES_wrap_key, AES_unwrap_key, AES_wrap_key_padded, AES_unwrap_key_padded | SandyBridge+ | InputLength, MemCorrect, NoInline | SAW | | |||
| | [<nobr>AES-GCM</nobr>](SPEC.md#AES-GCM) | 256 | gcm_ghash_avx, aes_hw_ctr32_encrypt_blocks, aesni_gcm_encrypt, aesni_gcm_decrypt | SandyBridge+ | MemCorrect, NoInline | SAW | | |||
There was a problem hiding this comment.
@apetcher-amazon: The AES-GCM proofs are documented here in the README.md...
SPEC.md
Outdated
| ## AES-GCM | ||
|
|
||
| These functions are verified to have the following properties related to AES-GCM using AES-256. These functions are defined in [NIST SP 800-38D](https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38d.pdf). For more detailed specifications, see [AES-GCM.saw](SAW/proof/AES/AES-GCM.saw). | ||
|
|
||
| | Function | Preconditions | Postconditions | | ||
| | ---------------| -------------| --------------- | | ||
| | gcm_ghash_avx | <ul><li>The hash table parameter points to values precomputed by calling the `gcm_init_Htable` Cryptol function on a symbolic 128-bit value.</li><li>The input length is a symbolic integer 16 * k such that 0 < k < 18.</li></ul> | <ul><li>The Xi buffer holds the correct hash value as defined by the AES-GCM specification.</li></ul> | | ||
| | aes_hw_ctr32_encrypt_blocks | <ul><li>The global variable `OPENSSL_ia32cap_P` exists and points to a value that [disables AVX512[F|DQ|BW|VL] instructions](https://www.openssl.org/docs/manmaster/man3/OPENSSL_ia32cap.html).</li><li>The length is a symbolic integer 16 * k such that 0 < k < 18.</li><li>The key parameter points to a 32-byte AES-256 key.</li></ul> | <ul><li>The global variable `OPENSSL_ia32cap_P` continues to point to the same value.</li><li>The output buffer holds the value produced by the GCTR function as defined by the AES-GCM specification.</li></ul> | | ||
| | aesni_gcm_encrypt | <ul><li>The input length is a symbolic integer k such that k < 2^36.</li><li>The key parameter points to a 32-byte AES-256 key.</li><li>The hash table parameter points to values precomputed by calling the `get_Htable` Cryptol function on the AES-256 key.</li></ul> | <ul><li>If k >= 288, then the first k bytes of the output buffer will point to the ciphertext produced by the GCM-AE_K function as defined by the AES-GCM specification. If k < 288, then the output buffer will not be modified.</li><li>If k >= 288, then the Xi buffer will point to the updated Xi value computed by the `aesni_gcm_encrypt` Cryptol function. If k < 288, then the Xi buffer will not be modified.</li><li>If k >= 288, then the initialization vector buffer will point to the updated initialization vector value computed by the `aesni_gcm_encrypt` Cryptol function. If k < 288, then the initialization vector will not be updated.</li><li>The return value will be equal to 96 * floor(k / 96).</li></ul> | | ||
| | aesni_gcm_decrypt | <ul><li>The input length is a symbolic integer k such that k < 2^36.</li><li>The key parameter points to a 32-byte AES-256 key.</li><li>The hash table parameter points to values precomputed by calling `get_Htable` on the AES-256 key.</li></ul> | <ul><li>If k >= 96, then the first k bytes of the output buffer will point to the ciphertext produced by the GCM-AD_K function as defined by the AES-GCM specification. If k < 96, then the output buffer will not be modified.</li><li>If k >= 96, then the Xi buffer will point to the updated Xi value computed by the `aesni_gcm_decrypt` Cryptol function. If k < 96, then the Xi buffer will not be modified.</li><li>If k >= 96, then the initialization vector buffer will point to the updated initialization vector value computed by the `aesni_gcm_decrypt` Cryptol function. If k < 96, then the initialization vector will not be updated.</li><li>The return value will be equal to 96 * floor(k / 96).</li></ul> | |
There was a problem hiding this comment.
...as well as here in the SPEC.md.
RyanGlScott
force-pushed
the
rgs/aes-gcm-unbounded
branch
from
072de4c to
8ae6e6a
Compare
RyanGlScott
force-pushed
the
rgs/aes-gcm-unbounded
branch
from
8ae6e6a to
2d7002d
Compare
|
Every invocation of SAW is failing with something like this: I think this might be happening because the version of SAW binary located at the new |
|
@RyanGlScott , Sorry about that! I've uploaded a new SAW for Ubuntu20.04 at |
RyanGlScott
force-pushed
the
rgs/aes-gcm-unbounded
branch
from
2d7002d to
44639c8
Compare
This patch: * Bumps the `cryptol-specs` submodule to bring in the changes from GaloisInc/cryptol-specs#72. These changes are necessary to support a later commit which adds proofs for AES-GCM. As part of bumping the submodule, the names of some modules were renamed, so this patch updates the imports on the `aws-lc-verification` side accordingly. * Updates the Cryptol specifications to support the syntax used in Cryptol 3. Cryptol 3 overhauls its module system, and as a result, some Cryptol code which used to work in Cryptol 2 (primarily involving anonymous submodules) no longer works in Cryptol 3. Luckily, the code is easily repaired by moving definitions around.
Co-authored-by: Robert Dockins <[email protected]> Co-authored-by: Samuel Breese <[email protected]>
The `EVP_EncryptUpdate`, `EVP_DecryptUpdate`, `aesni_gcm_encrypt`, and `aesni_gcm_decrypt` proofs are particularly tricky and require particular SAW settings in order to go through. They also require the use of Constrained Horn Clause (`chc`) in Z3, so we make use of `llvm_verify_fixpoint_chc_x86` instead of `llvm_verify_fixpoint_x86`.
Doing so requires some additional rewrites, which I've added to `goal-rewrites-AES.saw`. This requires splitting up the EVP_EncryptUpdate proof into two parts: one where the `len` is zero, and one where the `len` is non-zero.
This updates the `SAW_URL` environment variables to point to a more recent version of SAW that includes the changes from GaloisInc/saw-script#2037, which are necessary to support the AES-GCM proofs.
Z3's Constrained Horn Clause (CHC) solving is buggy on Z3-4.8.8 and will return incorrect answers, which affects the AES-GCM proof. This patch upgrades to a newer version of Z3 which is not affected by the bug.
RyanGlScott
force-pushed
the
rgs/aes-gcm-unbounded
branch
from
44639c8 to
158e8b7
Compare
|
Based on the most recent pipeline feedback, I was able to identify a failure in the I am less clear on what is causing the failures in the other jobs, however. Specifically:
|
|
If you scroll up in the output of the I suspect that it may take some work to get everything working under one SAW build. Unless you think there is a simple way to resolve all these issues, it may be better to separate the new AES-GCM proof from the others so that it can use a different version of SAW. One way to do this is to create a separate |
Ah, I overlooked the fact that the Coq proofs are using a And indeed, the offending line is different in the more recent version of SAW that I updated to. As you say, it's unclear to me how much work it would take to update the Coq proofs, so best to continue using the previous version of SAW for those.
I agree. The question will be how well we can isolate the AES-GCM proofs from the rest of the proofs. For example, both the What if we use the previous version of SAW for the Coq proofs, but the newer version of SAW for all other proofs? My understanding is that the Coq proofs are relatively isolated from everything else, so this sounds more feasible. |
This is the only dependency, and it would be okay for AES_KW and AES_KWP to depend on only bounded proofs of AES, which work using the previous version of SAW.
That would also be fine. |
|
@RyanGlScott for the error in the |
That sounds reasonable to me. I'll prepare a separate PR for that, since it will likely be more self-contained than this one. I don't want to abandon this PR just yet, as it will be useful should we ever want to migrate the non-AES-GCM proofs over to the latest SAW. I'll leave it open for now. |
|
I've opened #144, an alternative version of this PR which splits out the AES-GCM proofs into something more self-contained. |
|
An update on the The high-level explanation is that this new version of SAW or Z3 does not work with the |
|
Ah, good catch. Indeed, testing locally, it appears that the use of Z3-4.8.14 is (at least partially) to blame, as the |
|
Correction. In my previous experiment, I used the new SAW but old Z3-4.8.8. It will be a non-trivial amount of work to fix all these proofs. |
This proves AES-GCM functions, building on top of the
cryptol-specswork in GaloisInc/cryptol-specs#72 and thesaw-scriptwork in GaloisInc/saw-script#2037. This supersedes previous efforts in #80 and #139.Notes:
aws-lc-verification's CI currently uses, so I needed to update the SAW binary distribution as a result. This version of SAW uses a newer version of Cryptol which overhauls the module system, and as a result, the Cryptol code in theaws-lc-verificationrepo (some of which is unrelated to the AES-GCM proofs) needed to be refactored slightly to work with the newer version of Cryptol. (See the "Update Cryptol code to work with latest Cryptol/cryptol-specs" commit for the details.)aws-lc-verification's CI is currently using Z3-4.8.8, so I upgrade it to a more recent version.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.