Review comments, part 1

README.md

@@ -42,7 +42,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 |
+| [<nobr>AES-GCM</nobr>](SPEC.md#AES-GCM) | 256 | EVP_CipherInit_ex, EVP_EncryptUpdate, EVP_DecryptUpdate, EVP_EncryptFinal_ex, EVP_DecryptFinal_ex | SandyBridge+ | MemCorrect, NoInline, GcmSpecGap, GcmMultipleOf16, GcmADNotVerified, GcmIV12Tag16 | 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 |
@@ -81,6 +81,10 @@ The caveats associated with some of the verification results are defined in the
 | SAWBreakpoint | The proof uses SAW's breakpoint feature. This feature assumes the specification on the breakpoint function for the inductive hypothesis. The feature lacks well-foundedness check for the inductive invariant. |
 | ArmSpecGap | The Cryptol specification used in NSym proofs for Arm is different from the one used in the corresponding SAW proofs. Specifically, recursive comprehensions are written as recursions. We verify the body of the recursions are equivalent but the top-level loop structure is not verified. |
 | ToolGap | Adjacent components in the implementation are formally verified using different tools.  These tools may use different language semantics, memory models, etc. It is assumed that a proof of correctness in one tool implies correct behavior as determined by another tool. Additionally, it is assumed that parameter values correctly flow from one component to another. |
+| GcmSpecGap | AES-GCM is verified using an implementation-specific Cryptol spec describing an optimized form of AES-GCM. |
+| GcmMultipleOf16 | EVP_{Encrypt,Decrypt}Update are only verified for cases where whole blocks are encrypted/decrypted, i.e., the length is a multiple of 16. |
+| GcmADNotVerified | Supplying additional data (AD) to AES-GCM is not verified. |
+| GcmIV12Tag16 | The AES-GCM functions are only verified for 12-byte IVs and 16-byte tags. |
 
 
 ### Functions with compiler optimization disabled

SAW/proof/AES/AES-CTR32.saw

@@ -124,6 +124,9 @@ aes_hw_ctr32_copy_thms <- for (eval_list {{ [ 1:[16] .. < MIN_BULK_BLOCKS ] }})
 aes_hw_ctr32_encrypt_blocks_concrete_ovs <- for (eval_list {{ [ 1:[16] .. < MIN_BULK_BLOCKS ] }}) (\i -> do {
   let blocks = eval_int i;
   print (str_concat "aes_hw_ctr32_encrypt blocks=" (show blocks));
+  // track %r11 across function calls during x86 code discovery, resulting in
+  // more accuracy and less performance. This is a proof hint, and does not
+  // introduce any new assumptions.
   add_x86_preserved_reg "r11";
   ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test"
     "aes_hw_ctr32_encrypt_blocks"

SAW/proof/AES/AES-GCM-check-entrypoint.go

@@ -24,19 +24,21 @@ func main() {
 		utility.RunSawScript("verify-AES-GCM-quickcheck.saw")
 		return
 	}
-	// For now, we check a subset of all possible mres/res_mres values.
+	// When 'AES_GCM_SELECTCHECK' is defined, formal verification is executed
+	// with generated saw scripts based on the verification template and
+	// different values of `mres` and `res_mres`. Each of these parameters can
+	// be anything in the range [0, 15], but for now, we only check a subset of
+	// all possible mres/res_mres values.
 	mres_values := [2]int{0, 1}
 	res_mres_values := [2]int{0, 15}
-	// When 'AES_GCM_SELECTCHECK' is defined, formal verification is executed with different `evp_cipher_update_len`.
-	// Generate saw scripts based on the verification template and evp_cipher_update_len range [1, 384].
 	var wg sync.WaitGroup
 	process_count := 0
 
 	total_memory := utility.SystemMemory()
 	num_parallel_process := int(math.Floor((float64(total_memory) / float64(memory_used_per_test))))
 	log.Printf("System has %d bytes of memory, running %d jobs in parallel", total_memory, num_parallel_process)
 	for i := 0; i < 2; i++ {
-		for j := 0; i < 2; i++ {
+		for j := 0; j < 2; i++ {
 			wg.Add(1)
 			saw_template := "verify-AES-GCM-selectcheck-template.txt"
 			mres_placeholder_name := "TARGET_MRES_PLACEHOLDER"

SAW/proof/AES/AES-GCM.saw

@@ -33,7 +33,7 @@ let aes_block_size = 1;
 // The same value as AES_GCM_NONCE_LENGTH in crypto/fipsmodule/cipher/e_aes.c,
 // which is what EVP_aes_256_gcm uses to set iv_len.
 //
-// The IV for AES-GCM consists of 12 32-bit integers.
+// The IV for AES-GCM consists of 12 bytes.
 let aes_iv_len = 12;
 
 // This computes the total number of message blocks that can be
@@ -243,12 +243,38 @@ llvm_verify m "EVP_CipherInit_ex"
   (EVP_CipherInit_ex_spec {{ 0 : [32] }})
   evp_cipher_tactic;
 
-
+// The proofs of EVP_{Encrypt,Decrypt}Update are tricky and require some custom
+// SAW settings to make them go through:
+//
+// Enable hash consing at the What4 level, i.e., aggressively deduplicate common
+// subexpressions. This can make certain proof goals easier for SMT solvers to
+// analyze.
 enable_what4_hash_consing;
+// Translate SAWCore terms to What4 during symbolic execution. Translating to
+// What4 can simplify certain proof goals via What4's optimizations.
 enable_what4_eval;
+// Symbolic execution proof goals involving out of potentially invalid writes
+// will directly generate a failing proof goal rather than a fresh constant.
+// The former is more difficult to trace in the output of proof goals, but it
+// has the advantage of being easier to optimize, which is why we use it here.
 disable_no_satisfying_write_fresh_constant;
+// Push certain operations (e.g., zero-extension) down to the branches of
+// if-then-else expressions. In some circumstances, this can result in SMT
+// queries that are easier for solvers to analyze.
 enable_what4_push_mux_ops;
 
+// Below are two proofs of EVP_EncryptUpdate, one where the length is zero
+// and another where the length is non-zero. Attempting to prove this for all
+// lengths takes an infeasibly long time to prove, so we need to apply a
+// rewrite (EncryptUpdate_slice_ite_prop) to make a key proof goal simpler
+// (and solvable within a reasonable amount of time). This rewrite only applies
+// when the length is non-zero, however, motivating the need to split the proofs
+// in two.
+//
+// Thankfully, we don't need to apply this rewrite in the proof where the length
+// is zero, as the resulting proof goals are simple enough that SMT solvers can
+// handle them without much difficulty.
+
 llvm_verify m "EVP_EncryptUpdate"
   [ aes_gcm_from_cipher_ctx_ov
   , aes_hw_encrypt_ov

SAW/proof/AES/AESNI-GCM.saw

@@ -63,6 +63,14 @@ disable_no_satisfying_write_fresh_constant;
 enable_what4_push_mux_ops;
 
 // Prove that aesni_gcm_{encrypt,decrypt} adhere to aesni_gcm_cipher_array_spec.
+// These are among the most difficult AES-GCM proofs, as they involve an
+// unbounded loop. In order for SAW to reason about this loop, we use the
+// llvm_verify_fixpoint_chc_x86 command, which computes a symbolic fixpoint
+// expression for the loop and solves for the resulting proof goals using Z3's
+// Constrained Horn Clauses (CHC) feature. As part of this, we need to supply
+// a Cryptol specification for the loop itself
+// (aesni_gcm_{encrypt,decrypt}_impl_loop) to make it easier for SAW to reason
+// about the loop's behavior.
 
 aesni_gcm_encrypt_array_ov <- llvm_verify_fixpoint_chc_x86' m "../../build/x86/crypto/crypto_test" "aesni_gcm_encrypt"
   [ ("byte64_len_to_mask_table", 704) // We need .Lbswap_mask. Its location is <byte64_len_to_mask_table+0x240>. 704 bytes is an offset that would be large enough to contain the right bytes after alignment.

SAW/proof/AES/GHASH.saw

@@ -132,10 +132,6 @@ gcm_ghash_avx_concrete_ovs <- for (eval_list {{ [ 1:[16] .. < MIN_BULK_BLOCKS ]
       simplify (addsimps concat_assoc_1_thms empty_ss);
       simplify (addsimps concat_assoc_2_thms empty_ss);
       goal_eval_unint ["pmult", "pmod", "gcm_polyval"];
-      goal_eval_unint ["pmult", "pmod", "gcm_polyval"];
-      goal_eval_unint ["pmult", "pmod", "gcm_polyval"];
-      goal_eval_unint ["pmult", "pmod", "gcm_polyval"];
-      goal_eval_unint ["pmult", "pmod", "gcm_polyval"];
       w4_unint_z3 ["pmult", "pmod", "gcm_polyval"];
     });
 });

SAW/proof/AES/evp-function-specs.saw

@@ -40,6 +40,8 @@ let EVP_CipherInit_ex_spec enc = do {
   points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx 0 {{ 1 : [32] }} 0xffffffff;
 
   points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr enc;
+
+  crucible_return (crucible_term {{ 1 : [32] }});
 };
 
 // A helper function for defining a specification for `EVP_CipherUpdate`.

SAW/proof/AES/goal-rewrites-AES.saw

@@ -148,13 +148,6 @@ let aesenclast_thms =
   , aesenclast_1_thm
   ];
 
-// replace (bvult x y) with (x - y <$ 0) in order for the semiring and abstract
-// domain to work. This simplifies goals related to the 64-byte alignment of
-// the stack.
-let bvult = parse_core "\\(x y : Vec 64 Bool) -> bvult 64 x y";
-cmp_sub_thm <- prove_folding_theorem
-  {{ \x y -> bvult x y == if (x @ 0 == y @ 0) then (x - y <$ 0) else (x @ 0 < y @ 0) }};
-
 natToInt_0  <- prove_folding_theorem (parse_core "\\(seq : Vec 12 (Vec 8 Bool)) -> bvEq 8 (at 12 (Vec 8 Bool) seq (intToNat (natToInt 0)))  (at 12 (Vec 8 Bool) seq 0)");
 natToInt_1  <- prove_folding_theorem (parse_core "\\(seq : Vec 12 (Vec 8 Bool)) -> bvEq 8 (at 12 (Vec 8 Bool) seq (intToNat (natToInt 1)))  (at 12 (Vec 8 Bool) seq 1)");
 natToInt_2  <- prove_folding_theorem (parse_core "\\(seq : Vec 12 (Vec 8 Bool)) -> bvEq 8 (at 12 (Vec 8 Bool) seq (intToNat (natToInt 2)))  (at 12 (Vec 8 Bool) seq 2)");

SAW/proof/AES_KW/goal-rewrites-AES.saw

@@ -146,11 +146,3 @@ let aesenclast_thms =
   [ aesenclast_0_thm
   , aesenclast_1_thm
   ];
-
-// replace (bvult x y) with (x - y <$ 0) in order for the semiring and abstract
-// domain to work. This simplifies goals related to the 64-byte alignment of
-// the stack.
-let bvult = parse_core "\\(x y : Vec 64 Bool) -> bvult 64 x y";
-cmp_sub_thm <- prove_folding_theorem
-  {{ \x y -> bvult x y == if (x @ 0 == y @ 0) then (x - y <$ 0) else (x @ 0 < y @ 0) }};
-

SAW/proof/common/utility.go

@@ -74,7 +74,7 @@ func RunSelectCheckScript(path_to_saw_file string, saw_params []string, path_to_
 	cmd.Stderr = os.Stderr
 	err := cmd.Run()
 	if err != nil {
-		log.Fatal("Failed to run saw script %s. Related template: %s.", path_to_saw_file, path_to_template, err)
+		log.Fatalf("Failed to run saw script %s. Related template: %s.", path_to_saw_file, path_to_template, err)
 	} else {
 		log.Printf("Finished executing saw script %s. Related template: %s.", path_to_saw_file, path_to_template)
 	}

SAW/scripts/x86_64/run_checks_aes_gcm.sh

@@ -5,4 +5,4 @@
 
 set -ex
 
-/usr/bin/python3 ./scripts/parallel.py --file ./scripts/x86_64/release_jobs_aes_gcm.sh
+./scripts/x86_64/release_jobs_aes_gcm.sh

SPEC.md

@@ -41,10 +41,10 @@ The EVP_* functions are verified to have the following properties related to AES
 
 | Function  | Preconditions |  Postconditions |
 | ---------------| -------------| --------------- |
-| EVP_CipherInit_ex | <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 `ctx` parameter's `cipher` field is null.</li><li>The `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li></ul> | <ul><li>The global variable `OPENSSL_ia32cap_P` continues to point to the same value.</li><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `mres` is `0`, `iv_set` is `1`, and `taglen` is `-1`.</li></ul> |
-| EVP_{Encrypt,Decrypt}Update | <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 `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` field's `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `iv_set` is `1` and `taglen` is `-1`.</li><li>The `in_len` parameter is less than `2 ^^ 31`.</li><li>`ctx->gcm->msg.len` is less than `TOTAL_MESSAGE_MAX_LENGTH`, and `ctx->gcm->msg.len` plus `in_len` is less than `TOTAL_MESSAGE_MAX_LENGTH`.</li></ul> | <ul><li>The `out_len` parameter points to `in_len`.</li><li>Let `(ctx_updated, out_updated)` be the result of calling the `aes_gcm_{encrypt,decrypt}_update ctx in in_len out` Cryptol function, where `in`, `in_len`, and `out` correspond to the input parameters to the function.</li><li>The `ctx` parameter points to the key, length, hash table, and Xi values contained in `ctx_updated`.</li><li>The `ctx` parameter's `cipher_data` field is set such that `iv_set` is `1` and `taglen` is `-1`.</li><li>The `out` parameter points to `out_updated`.</li><li>The return value is `1`.</li></ul> |
+| EVP_CipherInit_ex | <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 `ctx` parameter's `cipher` field is null.</li><li>The `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li></ul> | <ul><li>The global variable `OPENSSL_ia32cap_P` continues to point to the same value.</li><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `mres` is `0`, `iv_set` is `1`, and `taglen` is `-1`.</li><li>The return value is `1`.</li></ul> |
+| EVP_{Encrypt,Decrypt}Update | <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 `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` field's `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `iv_set` is `1` and `taglen` is `-1`.</li><li>The `in_len` parameter is less than `2 ^^ 31`.</li><li>`ctx->gcm->msg.len` is less than `TOTAL_MESSAGE_MAX_LENGTH`, and `ctx->gcm->msg.len` plus `in_len` is less than `TOTAL_MESSAGE_MAX_LENGTH`.</li></ul> | <ul><li>The `out_len` parameter points to `in_len`.</li><li>Let `(ctx_updated, out_updated)` be the result of calling the `aes_gcm_{encrypt,decrypt}_update ctx in in_len out` Cryptol function, where `in`, `in_len`, and `out` correspond to the input parameters to the function.</li><li>The `ctx` parameter points to the key, length, hash table, and Xi values contained in `ctx_updated`.</li><li>The `ctx` parameter's `cipher_data` field is set such that `iv_set` is `1` and `taglen` is `-1`.</li><li>The `out` parameter points to `out_updated`.</li><li>The return value is `1`.</li></ul> |
 | EVP_EncryptFinal_ex | <ul><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` field's `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `iv_set` is `1` and `taglen` is `-1`.</li></ul> | <ul><li>The `ctx` parameter's `buf` field points to the result of calling the `cipher_final ctx` Cryptol function.</li><li>The `ctx` parameter's `cipher_data` field is set such that the `mres` value is the same as before calling the function, `iv_set` is `0`, and `taglen` is `AES_BLOCK_SIZE`.</li><li>The `out_len` parameter points to 0.</li><li>The return value is 1.</li></ul> |
-| EVP_DecryptFinal_ex | <ul><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` field's `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `iv_set` is `1` and `taglen` is `AES_BLOCK_SIZE`.</li><li>The `ctx` parameter's `buf` field is allocated.</li></ul> | <ul><li>The `ctx` parameter's `buf` field points to the result of calling the `cipher_final ctx` Cryptol function.</li><li>The `ctx` parameter's `cipher_data` field is set such that the `mres` value is the same as before calling the function, `iv_set` is `1` if the initial value of the `ctx` parameter's `buf` field is equal to the result of calling the `cipher_final ctx` Cryptol functio (and `0` otherwise), and `taglen` is `AES_BLOCK_SIZE`.</li><li>The `out_len` parameter points to 0.</li><li>If the initial value of the `ctx` parameter's `buf` field is equal to the result of calling the `cipher_final ctx` Cryptol function, then the return value will be 1. Otherwise, the return value will be 0.</li></ul> |
+| EVP_DecryptFinal_ex | <ul><li>The `ctx` field is initialized for AES-GCM using AES-256.</li><li>The `ctx` field's `cipher` parameter is a valid `EVP_CIPHER` such as the value returned by `EVP_aes_256_gcm()`.</li><li>The `ctx` parameter's `cipher_data` field is initialized such that `iv_set` is `1` and `taglen` is `AES_BLOCK_SIZE`.</li><li>The `ctx` parameter's `buf` field is allocated.</li></ul> | <ul><li>The `ctx` parameter's `buf` field points to the result of calling the `cipher_final ctx` Cryptol function.</li><li>The `ctx` parameter's `cipher_data` field is set such that the `mres` value is the same as before calling the function, `iv_set` is `1` if the initial value of the `ctx` parameter's `buf` field is equal to the result of calling the `cipher_final ctx` Cryptol function (and `0` otherwise), and `taglen` is `AES_BLOCK_SIZE`.</li><li>The `out_len` parameter points to 0.</li><li>If the initial value of the `ctx` parameter's `buf` field is equal to the result of calling the `cipher_final ctx` Cryptol function, then the return value will be 1. Otherwise, the return value will be 0.</li></ul> |
 
 ## Elliptic Curve Keys and Parameters