Renable NSym CI (#2570)

1. Reenable the NSym CI since the build is fixed in AWS-LC-verification.
Related PR: awslabs/aws-lc-verification#172
2. Update the README description to match AWS-LC-verification README

### Testing:
This change will be tested in the CI run. If the fix in
AWS-LC-verification works, the NSym build should pass.

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

Author: pennyannn

README.md

@@ -150,10 +150,11 @@ verified on certain CPUs with caveats include:
 | SHA-2 | 384 | neoverse-n1, neoverse-v1 |
 | HMAC | with <nobr>SHA-384</nobr> | SandyBridge+ |
 | <nobr>AES-KW(P)</nobr> | 256 | SandyBridge+ |
-| Elliptic Curve Keys and Parameters | with <nobr>P-384</nobr> | SandyBridge+ |
-| ECDSA | with <nobr>P-384</nobr>, <nobr>SHA-384</nobr> | SandyBridge+ |
-| ECDH | with <nobr>P-384</nobr> | SandyBridge+ |
-| HKDF | with <nobr>HMAC-SHA384</nobr> | SandyBridge+ |
+| <nobr>AES-GCM</nobr> | 256 | SandyBridge+ |
+<!--- | Elliptic Curve Keys and Parameters | with <nobr>P-384</nobr> | SandyBridge+ | --->
+<!--- | ECDSA | with <nobr>P-384</nobr>, <nobr>SHA-384</nobr> | SandyBridge+ | --->
+<!--- | ECDH | with <nobr>P-384</nobr> | SandyBridge+ | --->
+<!--- | HKDF | with <nobr>HMAC-SHA384</nobr> | SandyBridge+ | --->
 
 The CPUs for which code is verified are defined in the following table.
 

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

@@ -516,6 +516,17 @@ batch:
         variables:
           DOCKER_ENTRYPOINT: SAW/scripts/aarch64/docker_entrypoint.sh
 
+    # NSym proofs on platform AArch64
+    - identifier: ubuntu2204_clang14x_formal_verification_nsym_aarch64
+      buildspec: ./tests/ci/codebuild/common/run_fv_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-22.04_clang-14x_formal-verification-nsym-aarch64_latest
+        variables:
+          DOCKER_ENTRYPOINT: NSym/scripts/docker_entrypoint.sh
+
     # Build and test aws-lc without Perl/Go.
     - identifier: amazonlinux2_gcc7x_x86_64_minimal
       buildspec: ./tests/ci/codebuild/common/run_simple_target.yml

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

@@ -53,6 +53,7 @@ docker build -t fedora-31:clang-9x -f fedora-31_clang-9x/Dockerfile ../dependenc
 ./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-x86_64-aes-gcm/create_image.sh ubuntu-20.04:clang-10x_formal-verification-saw-x86_64-aes-gcm
 ./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

@@ -36,6 +36,7 @@ tag_and_push_img 'ubuntu-22.04:gcc-10x' "${ECS_REPO}:ubuntu-22.04_gcc-10x"
 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:gcc-12x_integration' "${ECS_REPO}:ubuntu-22.04_gcc-12x_integration"
+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-22.04_clang-14x_formal-verification-nsym-aarch64/create_image.sh

@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR ISC
+
+set -ex
+
+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