Add wrappers to AES-GCM functions

[jakemas]

Add wrappers to AES-GCM functions

For aws/aws-lc#2902
#P342421881

Overview

This PR fixes the AES-GCM verification proofs by updating them to verify wrapper functions (aes_hw_encrypt_wrapper and aes_hw_ctr32_encrypt_blocks_wrapper) instead of attempting to verify the direct assembly implementations, which were being called through wrappers in the actual code.

Root Cause

The AES-GCM implementation in aws-lc calls wrapper functions for AES encryption operations, so that all AES code is located together when passed through the delocator in the FIPS module. However, the SAW verification proofs were attempting to verify against the direct assembly implementations, causing a mismatch between the code being executed and the code being verified.

Solution Approach

The fix uses a two-stage verification strategy:

1. Assembly Verification: First verify the direct assembly implementations (aes_hw_encrypt and aes_hw_ctr32_encrypt_blocks)
2. Wrapper Verification: Then verify the wrapper functions using the assembly verification results as overrides

Changes

Patch Files

• SAW/patch/noinline_aes_hw_encrypt_wrapper.patch: Adds __attribute__((noinline)) to aes_hw_encrypt_wrapper to prevent inlining during verification
• SAW/patch/noinline_aes_hw_ctr32_encrypt_blocks_wrapper.patch: Adds __attribute__((noinline)) to aes_hw_ctr32_encrypt_blocks_wrapper to prevent inlining during verification

Proof Updates

AES.saw

• Creates aes_hw_encrypt_asm_ov by verifying the aes_hw_encrypt assembly implementation
• Creates aes_hw_encrypt_in_place_asm_ov by verifying the aes_hw_encrypt assembly with in-place specification
• Verifies aes_hw_encrypt_wrapper using the assembly override
• Verifies aes_hw_encrypt_wrapper with in-place specification using the assembly override

AES-CTR32.saw

• Verifies aes_hw_ctr32_encrypt_blocks assembly implementation for each possible block count, creating aes_hw_ctr32_encrypt_blocks_concrete_asm_ovs
• Creates aes_hw_ctr32_encrypt_blocks_bounded_array_asm_ov by refining the assembly specifications
• Verifies aes_hw_ctr32_encrypt_blocks_wrapper using the assembly override to create aes_hw_ctr32_encrypt_blocks_bounded_array_ov

AES-GCM.saw

• Updated to reference aes_hw_encrypt_wrapper
• Updated to reference aes_hw_ctr32_encrypt_blocks_wrapper

Build Script

• SAW/scripts/x86_64/entrypoint_check_aes_gcm.sh: Added patch applications for both wrapper noinline patches

Submodule Updates

• Updated src submodule to point to a branch with the wrapper function changes
• Updated .gitmodules configuration

Testing

The changes have been tested with the AES-GCM verification suite and all proofs pass successfully.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[pennyannn]

LGTM