Enable Arm SHA384 proofs in AWS-LC CI (aws#1348)

This commit enables NSym and SAW proofs for SHA384 on Arm machines (Graviton2 and Graviton3). Specifically,

1. Remove legacy selectchecks for SHA2 and AES-GCM
2. Rename previous run called `ubuntu2004_clang10x_formal_verification_quickcheck` to `ubuntu2004_clang10x_formal_verification_saw_x86_64` and a bunch of other renaming
3. Built and uploaded two new docker images: `ubuntu-22.04_clang-14x_formal-verification-nsym-aarch64` and `ubuntu-20.04_clang-10x_formal-verification-saw-aarch64`
4. Update relative files to add two new builds: `ubuntu2004_clang10x_formal_verification_saw_aarch64` and `ubuntu2204_clang14x_formal_verification_nsym_aarch64` in linux-x86 runs

tests/ci/cdk/cdk/codebuild/github_ci_linux_x86_omnibus.yaml

@@ -449,106 +449,42 @@ batch:
         compute-type: BUILD_GENERAL1_LARGE
         image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:fedora-31_clang-9x_latest
 
-    # When no SELECTCHECK env variable is defined, quick check is run with just a few parameters.
     # We parallel the quick check proof scripts.
     # Since each proof script takes around 7GB of memory, this results in a high demand for memory.
     # Current benchmarks show running quick check using 8 processes can consume more than 55 GB of memory.
     # Therefore, BUILD_GENERAL1_2XLARGE (72 vCPUs, 145 GB memory) is selected for quick check.
-    - identifier: ubuntu2004_clang10x_formal_verification_quickcheck
-      buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml
-      env:
-        type: LINUX_CONTAINER
-        privileged-mode: false
-        compute-type: BUILD_GENERAL1_2XLARGE
-        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification_latest
-
-    # In addition, we do select checks to verify more parameters.
-    # For select check, BUILD_GENERAL1_2XLARGE is also used to speed up proof instances by creating multiple processes for each parameter.
-    # When 'SHA512_384_SELECTCHECK' is defined, SHA512-384 formal verification is executed against more parameters.
-    - identifier: ubuntu2004_clang10x_formal_verification_sha_selectcheck
-      buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml
-      env:
-        type: LINUX_CONTAINER
-        privileged-mode: false
-        compute-type: BUILD_GENERAL1_2XLARGE
-        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification_latest
-        variables:
-          SHA512_384_SELECTCHECK: 1
-
-    # When 'AES_GCM_SELECTCHECK' is defined, AES-GCM formal verification is executed against more parameters.
-    # Each dimension only checks |evp_cipher_update_len| from AES_GCM_SELECTCHECK_START to AES_GCM_SELECTCHECK_END.
-    # https://github.com/awslabs/aws-lc-verification/blob/master/SAW/proof/AES/verify-AES-GCM-selectcheck-template.txt
-    - identifier: ubuntu2004_clang10x_formal_verification_aes_gcm_selectcheck_1_140
-      buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml
-      env:
-        type: LINUX_CONTAINER
-        privileged-mode: false
-        compute-type: BUILD_GENERAL1_2XLARGE
-        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification_latest
-        variables:
-          AES_GCM_SELECTCHECK: 1
-          AES_GCM_SELECTCHECK_START: 1
-          AES_GCM_SELECTCHECK_END: 140
-
-    - identifier: ubuntu2004_clang10x_formal_verification_aes_gcm_selectcheck_141_231
-      buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml
-      env:
-        type: LINUX_CONTAINER
-        privileged-mode: false
-        compute-type: BUILD_GENERAL1_2XLARGE
-        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification_latest
-        variables:
-          AES_GCM_SELECTCHECK: 1
-          AES_GCM_SELECTCHECK_START: 141
-          AES_GCM_SELECTCHECK_END: 231
-
-    - identifier: ubuntu2004_clang10x_formal_verification_aes_gcm_selectcheck_232_289
-      buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml
-      env:
-        type: LINUX_CONTAINER
-        privileged-mode: false
-        compute-type: BUILD_GENERAL1_2XLARGE
-        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification_latest
-        variables:
-          AES_GCM_SELECTCHECK: 1
-          AES_GCM_SELECTCHECK_START: 232
-          AES_GCM_SELECTCHECK_END: 289
-
-    - identifier: ubuntu2004_clang10x_formal_verification_aes_gcm_selectcheck_290_325
-      buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml
+    # SAW proofs on platform X86_64
+    - identifier: ubuntu2004_clang10x_formal_verification_saw_x86_64
+      buildspec: ./tests/ci/codebuild/common/run_simple_target.yml
       env:
         type: LINUX_CONTAINER
         privileged-mode: false
         compute-type: BUILD_GENERAL1_2XLARGE
-        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification_latest
+        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification-saw-x86_64_latest
         variables:
-          AES_GCM_SELECTCHECK: 1
-          AES_GCM_SELECTCHECK_START: 290
-          AES_GCM_SELECTCHECK_END: 325
+          AWS_LC_CI_TARGET: "tests/ci/run_formal_verification_saw_x86_64.sh"
 
-    - identifier: ubuntu2004_clang10x_formal_verification_aes_gcm_selectcheck_326_356
-      buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml
+    # SAW proofs on platform AArch64
+    - identifier: ubuntu2004_clang10x_formal_verification_saw_aarch64
+      buildspec: ./tests/ci/codebuild/common/run_simple_target.yml
       env:
         type: LINUX_CONTAINER
         privileged-mode: false
         compute-type: BUILD_GENERAL1_2XLARGE
-        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification_latest
+        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification-saw-aarch64_latest
         variables:
-          AES_GCM_SELECTCHECK: 1
-          AES_GCM_SELECTCHECK_START: 326
-          AES_GCM_SELECTCHECK_END: 356
+          AWS_LC_CI_TARGET: "tests/ci/run_formal_verification_saw_aarch64.sh"
 
-    - identifier: ubuntu2004_clang10x_formal_verification_aes_gcm_selectcheck_357_384
-      buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml
+    # NSym proofs on platform AArch64
+    - identifier: ubuntu2204_clang14x_formal_verification_nsym_aarch64
+      buildspec: ./tests/ci/codebuild/common/run_simple_target.yml
       env:
         type: LINUX_CONTAINER
         privileged-mode: false
         compute-type: BUILD_GENERAL1_2XLARGE
-        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-20.04_clang-10x_formal-verification_latest
+        image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-22.04_clang-14x_formal-verification-nsym-aarch64_latest
         variables:
-          AES_GCM_SELECTCHECK: 1
-          AES_GCM_SELECTCHECK_START: 357
-          AES_GCM_SELECTCHECK_END: 384
+          AWS_LC_CI_TARGET: "tests/ci/run_formal_verification_nsym_aarch64.sh"
 
     # Build and test aws-lc without Perl/Go.
     - identifier: amazonlinux2_gcc7x_x86_64_minimal

tests/ci/docker_images/linux-x86/build_images.sh

@@ -45,7 +45,9 @@ docker build -t fedora-31:clang-9x -f fedora-31_clang-9x/Dockerfile ../dependenc
 # Build images defined in aws-lc-verification GitHub repo #
 ###########################################################
 
-./ubuntu-20.04_clang-10x_formal-verification/create_image.sh ubuntu-20.04:clang-10x_formal-verification
+./ubuntu-20.04_clang-10x_formal-verification-saw-x86_64/create_image.sh ubuntu-20.04:clang-10x_formal-verification-saw-x86_64
+./ubuntu-20.04_clang-10x_formal-verification-saw-aarch64/create_image.sh ubuntu-20.04:clang-10x_formal-verification-saw-aarch64
+./ubuntu-22.04_clang-14x_formal-verification-nsym-aarch64/create_image.sh ubuntu-22.04:clang-14x_formal-verification-nsym-aarch64
 
 ###########################################################
 # Build older unofficial docker image that uses gcc 4.1.3 #

tests/ci/docker_images/linux-x86/push_images.sh

@@ -12,7 +12,7 @@ fi
 
 echo "Uploading docker images to ${ECS_REPO}."
 
-$(aws ecr get-login --no-include-email)
+$(aws ecr get-login --no-include-email --region us-west-2)
 
 # Tag images with date to help find old images, CodeBuild uses the latest tag and gets updated automatically
 tag_and_push_img 'ubuntu-16.04:gcc-5x' "${ECS_REPO}:ubuntu-16.04_gcc-5x"
@@ -24,12 +24,14 @@ tag_and_push_img 'ubuntu-20.04:clang-9x' "${ECS_REPO}:ubuntu-20.04_clang-9x"
 tag_and_push_img 'ubuntu-20.04:clang-10x' "${ECS_REPO}:ubuntu-20.04_clang-10x"
 tag_and_push_img 'ubuntu-20.04:android' "${ECS_REPO}:ubuntu-20.04_android"
 tag_and_push_img 'ubuntu-20.04:clang-7x-bm-framework' "${ECS_REPO}:ubuntu-20.04_clang-7x-bm-framework"
-tag_and_push_img 'ubuntu-20.04:clang-10x_formal-verification' "${ECS_REPO}:ubuntu-20.04_clang-10x_formal-verification"
+tag_and_push_img 'ubuntu-20.04:clang-10x_formal-verification-saw-x86_64' "${ECS_REPO}:ubuntu-20.04_clang-10x_formal-verification-saw-x86_64"
+tag_and_push_img 'ubuntu-20.04:clang-10x_formal-verification-saw-aarch64' "${ECS_REPO}:ubuntu-20.04_clang-10x_formal-verification-saw-aarch64"
 tag_and_push_img 'ubuntu-20.04:gcc-7x' "${ECS_REPO}:ubuntu-20.04_gcc-7x"
 tag_and_push_img 'ubuntu-20.04:gcc-8x' "${ECS_REPO}:ubuntu-20.04_gcc-8x"
 tag_and_push_img 'ubuntu-22.04:clang-14x-sde' "${ECS_REPO}:ubuntu-22.04_clang-14x-sde"
 tag_and_push_img 'ubuntu-22.04:gcc-11x' "${ECS_REPO}:ubuntu-22.04_gcc-11x"
 tag_and_push_img 'ubuntu-22.04:gcc-12x' "${ECS_REPO}:ubuntu-22.04_gcc-12x"
+tag_and_push_img 'ubuntu-22.04:clang-14x_formal-verification-nsym-aarch64' "${ECS_REPO}:ubuntu-22.04_clang-14x_formal-verification-nsym-aarch64"
 tag_and_push_img 'centos-7:gcc-4x' "${ECS_REPO}:centos-7_gcc-4x"
 tag_and_push_img 'centos-8:gcc-8x' "${ECS_REPO}:centos-8_gcc-8x"
 tag_and_push_img 'amazonlinux-2:gcc-7x' "${ECS_REPO}:amazonlinux-2_gcc-7x"

tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification-saw-aarch64/create_image.sh

@@ -0,0 +1,15 @@
+#!/bin/bash -ex
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR ISC
+
+if [ -n "$1" ]; then
+  docker_tag="$1"
+else
+  docker_tag='ubuntu-20.04:clang-10x_formal-verification-saw-aarch64'
+fi
+rm -rf aws-lc-verification
+git clone https://github.com/awslabs/aws-lc-verification.git
+cd aws-lc-verification
+docker build --pull --no-cache -f Dockerfile.saw_aarch64 -t ${docker_tag} .
+cd ..
+rm -rf aws-lc-verification

tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification/create_image.sh → tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification-saw-x86_64/create_image.sh

@@ -5,7 +5,7 @@
 if [ -n "$1" ]; then
   docker_tag="$1"
 else
-  docker_tag='ubuntu-20.04:clang-10x_formal-verification'
+  docker_tag='ubuntu-20.04:clang-10x_formal-verification-saw-x86_64'
 fi
 rm -rf aws-lc-verification
 git clone https://github.com/awslabs/aws-lc-verification.git

tests/ci/docker_images/linux-x86/ubuntu-22.04_clang-14x_formal-verification-nsym-aarch64/create_image.sh

@@ -0,0 +1,15 @@
+#!/bin/bash -ex
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR ISC
+
+if [ -n "$1" ]; then
+  docker_tag="$1"
+else
+  docker_tag='ubuntu-20.04:clang-10x_formal-verification-nsym-aarch64'
+fi
+rm -rf aws-lc-verification
+git clone https://github.com/awslabs/aws-lc-verification.git
+cd aws-lc-verification
+docker build --pull --no-cache -f Dockerfile.nsym -t ${docker_tag} .
+cd ..
+rm -rf aws-lc-verification

tests/ci/run_formal_verification.sh

@@ -2,6 +2,7 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 
+ENTRYDIR=$1
 AWS_LC_DIR=${PWD##*/}
 cd ../
 ROOT=$(pwd)
@@ -16,6 +17,6 @@ git submodule update --init
 # Below is to copy code of **target** aws-lc to 'src' dir.
 rm -rf ./src/* && cp -r "${ROOT}/${AWS_LC_DIR}/"* ./src
 # execute the entry to saw scripts.
-./SAW/scripts/x86_64/docker_entrypoint.sh
+./$ENTRYDIR/docker_entrypoint.sh
 cd ..
 rm -rf aws-lc-verification-build

tests/ci/run_formal_verification_nsym_aarch64.sh

@@ -0,0 +1,5 @@
+#!/bin/bash -ex
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR ISC
+
+./tests/ci/run_formal_verification.sh NSym/scripts

tests/ci/run_formal_verification_saw_aarch64.sh

@@ -0,0 +1,5 @@
+#!/bin/bash -ex
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR ISC
+
+./tests/ci/run_formal_verification.sh SAW/scripts/aarch64

tests/ci/run_formal_verification_saw_x86_64.sh

@@ -0,0 +1,5 @@
+#!/bin/bash -ex
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR ISC
+
+./tests/ci/run_formal_verification.sh SAW/scripts/x86_64