Add OPENSSL_cleanse override to AES-GCM SAW proofs#186
Merged
Conversation
nebeid
approved these changes
Mar 25, 2026
justsmth
added a commit
to aws/aws-lc
that referenced
this pull request
Mar 26, 2026
#3121) ### Issues Addresses: AWS-LC-1073 ### Related * awslabs/aws-lc-verification#186 ### Description of changes: Several functions were leaving sensitive intermediate values on the stack after returning. This change adds `OPENSSL_cleanse` calls to zeroize those buffers before they go out of scope: - **CTR-DRBG** (`ctrdrbg.c`): Zeroize `seed_material`, `temp`, `entropy_copy`, and partial keystream `block`. - **ECDH** (`ecdh.c`): Zeroize the raw shared secret `buf` in `ECDH_compute_key_fips`. - **ECDSA** (`ecdsa.c`): Zeroize `tmp` after it holds k⁻¹ in `ecdsa_sign_impl`. - **X25519 / Ed25519 nohw** (`curve25519_nohw.c`): Zeroize clamped private scalars, Montgomery ladder intermediates, and nonce-derived values. - **X25519 / Ed25519 s2n-bignum** (`curve25519_s2n_bignum_asm.c`): Same treatment for the s2n-bignum code paths. - **GCM** (`gcm.c`): Zeroize the GHASH hash key `H` (derived from `AES_K(0^128)`) and `ghash_key`. The early `return` statements in `CRYPTO_ghash_init` are refactored to `goto out` so all paths go through a single cleanup site. ### Call-outs: The GCM change is the only one with a structural refactor — the `return` → `goto out` conversion in `CRYPTO_ghash_init`. All other changes are purely additive `OPENSSL_cleanse` calls at function exit points. ### Testing: Existing tests cover the functional behavior of all affected code paths. These changes should be transparent since they only zero memory that is no longer used. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license and the ISC license.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Related
Description
Add
OPENSSL_cleanse_ovto theevp_cipher_ovsoverride list in the AES-GCM SAW proofs.This is needed to support aws/aws-lc#3121, which adds
OPENSSL_cleansecalls to zeroize sensitive stack buffers in several cryptographic functions. Two of those calls land on theEVP_CipherInit_exproof path:CRYPTO_gcm128_init_key— cleansing theghash_key(the raw GHASH subkeyH = AES_K(0^128))CRYPTO_ghash_init— cleansing the byte-swappedH[2]local copy of the same subkeyWithout the override, SAW attempts to symbolically execute
OPENSSL_cleanse, which contains an inline assembly barrier (__asm__ __volatile__) and cannot be interpreted, causing thefv-saw-x86_64-aes-gcmjob to fail.The
OPENSSL_cleanse_ovoverride is already defined inproof/common/memory.saw(whichAES-GCM.sawincludes) and is already used by the ECDSA and ECDH proofs for the same reason.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.