From e8312e7b7d07cf2e916a36e01b31a05860e18eee Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Tue, 23 Apr 2024 15:04:24 -0400
Subject: [PATCH] Document preconditions, postconditions, and limitations of
 AES-GCM proofs

---
 README.md |  1 +
 SPEC.md   | 11 +++++++++++
 2 files changed, 12 insertions(+)

diff --git a/README.md b/README.md
index ae66e364..934aa395 100644
--- a/README.md
+++ b/README.md
@@ -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 |
 | [Elliptic Curve Keys and Parameters](SPEC.md#Elliptic-Curve-Keys-and-Parameters) | with <nobr>P-384</nobr> | EVP_PKEY_CTX_new_id, EVP_PKEY_CTX_new, EVP_PKEY_paramgen_init, EVP_PKEY_CTX_set_ec_paramgen_curve_nid, EVP_PKEY_paramgen, EVP_PKEY_keygen_init, EVP_PKEY_keygen | SandyBridge+ | SAWCore_Coq, EC_Fiat_Crypto, ToolGap, NoEngine, MemCorrect, CRYPTO_refcount_Correct, CRYPTO_once_Correct, OptNone, SAWBreakpoint | SAW, Coq |
 | [ECDSA](SPEC.md#ECDSA) | with <nobr>P-384</nobr>, <nobr>SHA-384</nobr> | EVP_DigestSignInit, EVP_DigestVerifyInit, EVP_DigestSignUpdate, EVP_DigestVerifyUpdate, EVP_DigestSignFinal, EVP_DigestVerifyFinal, EVP_DigestSign, EVP_DigestVerify | SandyBridge+ | EC_Pub_Mul_Correct, EC_Constants_Correct, EC_Conversion_Correct, SAWCore_Coq, EC_Fiat_Crypto, NoEngine, MemCorrect, ECDSA_k_Valid, ECDSA_SignatureLength, CRYPTO_refcount_Correct, CRYPTO_once_Correct, ERR_put_error_Correct, NoInline | SAW, Coq |
 | [ECDH](SPEC.md#ECDH) | with <nobr>P-384</nobr> | EVP_PKEY_derive_init, EVP_PKEY_derive | SandyBridge+ | SAWCore_Coq, EC_Fiat_Crypto, ECDH_InfinityTestCorrect, ToolGap, MemCorrect, NoEngine, CRYPTO_refcount_Correct, PubKeyValid | SAW, Coq |
diff --git a/SPEC.md b/SPEC.md
index 4543c6de..893b3b27 100644
--- a/SPEC.md
+++ b/SPEC.md
@@ -35,6 +35,17 @@ The AES_(un)wrap_key_* functions are verified to have the following properties r
 | AES_wrap_key_padded | <ul><li>The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.</li><li>The parameters are a 32-byte AES-256 key, a k+p+8-byte output array, a pointer to an integer which accepts the output length, the integer k+p+8, a k-byte input array, and the integer k.</li></ul> | <ul><li>The output buffer holds the value produced by the AES KWP encrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.</li><li>The ouptut length integer holds the value k+p+8.</li><li>The value returned is 1.</li></ul> |
 | AES_unwrap_key_padded | <ul><li>The plaintext length is k, which is an arbitrary positive integer. The integer p is the smallest non-negative value such that k+p is a multiple of 8.</li><li>The parameters are a 32-byte AES-256 key, a k+p-byte output array, a pointer to an integer which accepts the output length, the integer k+p, a k+p+8-byte input array, and the integer k+p+8.</li></ul> | <ul><li>The output buffer holds the value produced by the AES KWP decrypt operation using the key, the constant IV 0xA65959A6, and the input buffer.</li><li>The ouptut length integer holds the correct plaintext length k.</li><li>If the AES KWP decrypt operation should succeed, the function returns 1, otherwise it returns 0.</li></ul> |
 
+## 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> |
+
 ## Elliptic Curve Keys and Parameters
 
 The EVP_PKEY_* functions are verified to have the following properties related to EC using P-384. For more detailed specifications, see [evp-function-specs.saw](SAW/proof/ECDH/evp-function-specs.saw).