Add unbounded AES-GCM verification, isolate newer SAW from other proofs

.github/actions/SAW_X86_64_AES_GCM/action.yml

@@ -0,0 +1,8 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+name: 'AWS-LC Formal Verification SAW Proofs'
+description: 'Check SAW proofs to verify AWS-LC against Cryptol specs'
+runs:
+  using: 'docker'
+  image: '../../../Dockerfile.saw_x86_aes_gcm'

.github/workflows/main.yml

@@ -28,6 +28,21 @@ jobs:
     # Runs the formal verification action
     - name: SAW X86_64 Proofs
       uses: ./.github/actions/SAW_X86_64
+  saw-x86_64-aes-gcm:
+    # The type of runner that the job will run on
+    runs-on: aws-lc-verification_ubuntu-latest_16-core
+
+    # Steps represent a sequence of tasks that will be executed as part of the job
+    steps:
+    # Check out main repo and submodules.
+    - uses: actions/checkout@v2
+      name: check out top-level repository and all submodules
+      with:
+        submodules: true
+
+    # Runs the formal verification action
+    - name: SAW X86_64 AES-GCM Proof
+      uses: ./.github/actions/SAW_X86_64_AES_GCM
   saw-aarch64:
     # The type of runner that the job will run on
     runs-on: aws-lc-verification_ubuntu-latest_16-core

.gitmodules

@@ -6,6 +6,9 @@
 	path = cryptol-specs
 	branch = sha-imperative
 	url = https://github.com/GaloisInc/cryptol-specs.git
+[submodule "cryptol-specs-aes-gcm"]
+	path = cryptol-specs-aes-gcm
+	url = https://github.com/GaloisInc/cryptol-specs.git
 [submodule "Coq/fiat-crypto"]
 	path = Coq/fiat-crypto
 	url = https://github.com/mit-plv/fiat-crypto

Dockerfile.saw_x86_aes_gcm

@@ -0,0 +1,28 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+
+FROM ubuntu:20.04
+ENV GOROOT=/usr/local/go
+ENV PATH="$GOROOT/bin:$PATH"
+ARG GO_VERSION=1.20.1
+ARG GO_ARCHIVE="go${GO_VERSION}.linux-amd64.tar.gz"
+RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections
+RUN apt-get update
+RUN apt-get install -y wget unzip time git cmake clang llvm python3-pip libncurses5 opam libgmp-dev cabal-install
+
+RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \
+   mkdir $GOROOT &&  mv go/* $GOROOT && rm $GO_ARCHIVE
+RUN pip3 install wllvm
+RUN pip3 install psutil
+
+ADD ./SAW/scripts/x86_64 /lc/scripts
+RUN /lc/scripts/docker_install_aes_gcm.sh
+ENV CRYPTOLPATH="../../../cryptol-specs-aes-gcm:../../spec"
+ENV AES_GCM_SELECTCHECK=1
+
+# This container expects all files in the directory to be mounted or copied.
+# The GitHub action will mount the workspace and set the working directory of the container.
+# Another way to mount the files is: docker run -v `pwd`:`pwd` -w `pwd` <name>
+
+ENTRYPOINT ["./SAW/scripts/x86_64/docker_entrypoint_aes_gcm.sh"]

README.md

@@ -17,16 +17,18 @@ The easiest way to build the library and run the proofs is to use [Docker](https
 2. Build a Docker image:
    `docker build --pull --no-cache -f Dockerfile.[...] -t awslc-saw .`
    1. For running SAW proofs on X86_64, use: `Dockerfile.saw_x86`
-   2. For running SAW proofs on AARCH64, use: `Dockerfile.saw_aarch64`
-   3. For running Coq proofs, use: `Dockerfile.coq`
-   4. For running NSym proofs, use: `Dockerfile.nsym`
+   1. For running SAW proofs for AES-GCM on X86_64, use: `Dockerfile.saw_x86_aes_gcm`
+   3. For running SAW proofs on AARCH64, use: `Dockerfile.saw_aarch64`
+   4. For running Coq proofs, use: `Dockerfile.coq`
+   5. For running NSym proofs, use: `Dockerfile.nsym`
 
 3. Run the SAW proofs inside the Docker container: ``docker run -v `pwd`:`pwd` -w `pwd` awslc-saw``
    1. Run SAW proofs on X86_64: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint SAW/scripts/x86_64/docker_entrypoint.sh awslc-saw``
       1. This step will also run formally-verified tests on certain hard-coded constant values.
-   2. Run SAW proofs on AARCH64: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint SAW/scripts/aarch64/docker_entrypoint.sh awslc-saw``
-   3. Use Coq to validate the Cryptol specs used in the SAW proofs: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint Coq/docker_entrypoint.sh awslc-saw``
-   4. Run NSym for AARCH64 assembly: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint NSym/scripts/docker_entrypoint.sh awslc-saw``
+   2. RUN SAW proofs for AES-GCM on x86_64: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint SAW/scripts/x86_64/docker_entrypoint_aes_gcm.sh awslc-saw``
+   3. Run SAW proofs on AARCH64: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint SAW/scripts/aarch64/docker_entrypoint.sh awslc-saw``
+   4. Use Coq to validate the Cryptol specs used in the SAW proofs: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint Coq/docker_entrypoint.sh awslc-saw``
+   5. Run NSym for AARCH64 assembly: ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint NSym/scripts/docker_entrypoint.sh awslc-saw``
 
 Running ``docker run -it -v `pwd`:`pwd` -w `pwd` --entrypoint bash awslc-saw`` will enter an interactive shell within the container, which is often useful for debugging.
 
@@ -40,6 +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 | EVP_CipherInit_ex, EVP_CIPHER_CTX_ctrl, EVP_EncryptUpdate, EVP_DecryptUpdate, EVP_EncryptFinal_ex, EVP_DecryptFinal_ex | SandyBridge+ | MemCorrect, NoInline, GcmSpecGap, GcmMultipleOf16, GcmADNotVerified, GcmIV12Tag16, GcmWellFoundedInduction | 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 |
@@ -78,6 +81,11 @@ 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. |
+| GcmWellFoundedInduction | The AES-GCM proofs make use of inductive proofs to prove theorems about unbounded loops, but the inductive hypotheses are assumed, as SAW lacks a well-foundedness check for the inductive invariants. |
 
 
 ### Functions with compiler optimization disabled

SAW/proof/AES/AES-CTR32.saw

@@ -0,0 +1,154 @@
+/*
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ * SPDX-License-Identifier: Apache-2.0
+*/
+
+// Using experimental proof command "crucible_llvm_verify_x86"
+enable_experimental;
+
+
+////////////////////////////////////////////////////////////////////////////////
+// Specifications
+
+// A bounded specification for aes_hw_ctr32_encrypt_blocks where `in_ptr` and `out_ptr`
+// point to a fixed-size arrays, where the length of the arrays are determined
+// by the supplied number of `blocks`.
+let aes_hw_ctr32_encrypt_blocks_spec blocks = do {
+  let len' = eval_size {| blocks * AES_BLOCK_SIZE |};
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+
+  (in_, in_ptr) <- ptr_to_fresh_readonly "in" (llvm_array len' (llvm_int 8));
+  out_ptr <- crucible_alloc (llvm_array len' (llvm_int 8));
+  key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st");
+  key <- fresh_aes_key_st;
+  points_to_aes_key_st key_ptr key;
+  (ivec, ivec_ptr) <- ptr_to_fresh_readonly "ivec" (llvm_array AES_BLOCK_SIZE (llvm_int 8));
+
+  crucible_execute_func [in_ptr, out_ptr, (crucible_term {{ `blocks : [64] }}), key_ptr, ivec_ptr];
+
+  crucible_points_to out_ptr (crucible_term {{ split`{each=8} (join (aes_ctr32_encrypt_blocks (join key) (join (take ivec)) (join (drop ivec)) (split (join in_)))) }});
+
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+};
+
+// A bounded specification for aes_hw_ctr32_encrypt_blocks where `in_ptr` and `out_ptr`
+// point to a fixed-size arrays, where the length of the arrays are determined
+// by the supplied number of `blocks`.
+//
+// This spec is very nearly the same as `aes_hw_ctr32_encrypt_blocks_spec`
+// above, except that this spec uses SMT arrays to specify the storage for
+// `in_ptr` and `out_ptr`.
+let aes_hw_ctr32_encrypt_blocks_array_spec blocks = do {
+  let len = eval_size {| blocks * AES_BLOCK_SIZE |};
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+
+  (in_, in_ptr) <- ptr_to_fresh_array_readonly "in" {{ `len : [64] }};
+  (out, out_ptr) <- ptr_to_fresh_array "out" {{ `len : [64] }};
+  key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st");
+  key <- fresh_aes_key_st;
+  points_to_aes_key_st key_ptr key;
+  (ivec, ivec_ptr) <- ptr_to_fresh_readonly "ivec" (llvm_array AES_BLOCK_SIZE (llvm_int 8));
+
+  crucible_execute_func [in_ptr, out_ptr, (crucible_term {{ `blocks : [64] }}), key_ptr, ivec_ptr];
+
+  crucible_points_to_array_prefix
+    out_ptr
+    {{ aes_ctr32_encrypt_blocks_array (join key) (join (take ivec)) (join (drop ivec)) in_ `blocks 0 out }}
+    {{ `len : [64] }};
+
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+};
+
+// An unbounded specification for aes_hw_ctr32_encrypt_blocks where `in_ptr` and
+// `out_ptr` point to arrays of symbolic lengths. The number of blocks must be
+// in the range (0, MIN_BULK_BLOCKS) (exclusive).
+let aes_hw_ctr32_encrypt_bounded_array_spec = do {
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+
+  blocks <- llvm_fresh_var "blocks" (llvm_int 64);
+  let len = {{ blocks * `AES_BLOCK_SIZE }};
+  crucible_precond {{ 0 < blocks }};
+  crucible_precond {{ blocks < `MIN_BULK_BLOCKS }};
+
+  (in_, in_ptr) <- ptr_to_fresh_array_readonly "in" len;
+  (out, out_ptr) <- ptr_to_fresh_array "out" len;
+
+  key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st");
+  key <- fresh_aes_key_st;
+  points_to_aes_key_st key_ptr key;
+  (ivec, ivec_ptr) <- ptr_to_fresh_readonly "ivec" (llvm_array AES_BLOCK_SIZE (llvm_int 8));
+
+  crucible_execute_func [in_ptr, out_ptr, crucible_term blocks, key_ptr, ivec_ptr];
+
+  crucible_points_to_array_prefix
+    out_ptr
+    {{ aes_ctr32_encrypt_blocks_array (join key) (join (take ivec)) (join (drop ivec)) in_ blocks 0 out }}
+    len;
+
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+};
+
+
+////////////////////////////////////////////////////////////////////////////////
+// Proof commands
+
+// A tactic for simplifying proof goals in the proof of `aes_hw_ctr32_encrypt_blocks_spec`.
+let aes_hw_ctr32_tactic = do {
+  simplify (cryptol_ss ());
+  simplify (addsimps slice_384_thms basic_ss);
+  goal_eval_unint ["AESRound", "AESFinalRound", "aesenc", "aesenclast"];
+  simplify (addsimps add_xor_slice_thms basic_ss);
+  simplify (addsimps aesenclast_thms basic_ss);
+  w4_unint_yices ["AESRound", "AESFinalRound"];
+};
+
+// Helper theorems for refining `aes_hw_ctr32_encrypt_bounded_array_spec`.
+// These are used to equate calling `aes_ctr32_encrypt_blocks_array` to an
+// equivalent expression involving the SMT arrayCopy operation.
+aes_hw_ctr32_copy_thms <- for (eval_list {{ [ 1:[16] .. < MIN_BULK_BLOCKS ] }}) (\i -> do {
+  let blocks = eval_int i;
+  print (str_concat "aes_hw_ctr32 copy lemma: " (show blocks));
+  prove_theorem
+    (do {
+      w4_unint_z3 ["aes_ctr32_encrypt_block"];
+    })
+    (rewrite (cryptol_ss ()) {{ \key iv ctr in out ->
+      arrayEq
+        (arrayCopy out 0 (aes_ctr32_encrypt_blocks_array key iv ctr in `blocks 0 out) 0 `(16*blocks))
+        (aes_ctr32_encrypt_blocks_array key iv ctr in `blocks 0 out)
+    }});
+});
+
+// For each possible number of blocks, prove `aes_hw_ctr32_encrypt_blocks_spec`
+// and use it to refine `aes_hw_ctr32_encrypt_blocks_array_spec`.
+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"
+    []
+    true
+    (aes_hw_ctr32_encrypt_blocks_spec blocks)
+    aes_hw_ctr32_tactic;
+  default_x86_preserved_reg;
+  llvm_refine_spec' m "aes_hw_ctr32_encrypt_blocks"
+    [ov]
+    (aes_hw_ctr32_encrypt_blocks_array_spec blocks)
+    (w4_unint_z3 ["aes_ctr32_encrypt_block"]);
+});
+
+// Now that we've proven `aes_hw_ctr32_encrypt_blocks_array_spec` overrides at
+// all possible block lengths, use the overrides to refine a proof for
+// `aes_hw_ctr32_encrypt_bounded_array_spec`.
+aes_hw_ctr32_encrypt_blocks_bounded_array_ov <- llvm_refine_spec' m "aes_hw_ctr32_encrypt_blocks"
+  aes_hw_ctr32_encrypt_blocks_concrete_ovs
+  aes_hw_ctr32_encrypt_bounded_array_spec
+  (do {
+    simplify (addsimps aes_hw_ctr32_copy_thms (cryptol_ss ()));
+    w4_unint_z3 ["aes_ctr32_encrypt_blocks_array"];
+  });
+

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

@@ -24,21 +24,28 @@ func main() {
 		utility.RunSawScript("verify-AES-GCM-quickcheck.saw")
 		return
 	}
-	selectcheck_range_start := utility.ParseSelectCheckRange("AES_GCM_SELECTCHECK_START", 1)
-	selectcheck_range_end := utility.ParseSelectCheckRange("AES_GCM_SELECTCHECK_END", 384)
-	// 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].
+	// 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. In particular, we check the following
+	// (mres, res_mres) pairs:
+	//
+	// (0, 0), (1, 0)
+	mres_values := [2]int{0, 1}
+	res_mres_value := 0
 	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 := selectcheck_range_start; i <= selectcheck_range_end; i++ {
+	for i := 0; i < 2; i++ {
 		wg.Add(1)
 		saw_template := "verify-AES-GCM-selectcheck-template.txt"
-		placeholder_name := "TARGET_LEN_PLACEHOLDER"
-		go utility.CreateAndRunSawScript(saw_template, []string{}, placeholder_name, i, &wg)
+		mres_placeholder_name := "TARGET_MRES_PLACEHOLDER"
+		res_mres_placeholder_name := "TARGET_RES_MRES_PLACEHOLDER"
+		go utility.CreateAndRunSawScript(saw_template, []string{}, mres_placeholder_name, mres_values[i], res_mres_placeholder_name, res_mres_value, &wg)
 		utility.Wait(&process_count, num_parallel_process, &wg)
 	}