diff --git a/tests/ci/cdk/cdk/codebuild/github_ci_linux_x86_omnibus.yaml b/tests/ci/cdk/cdk/codebuild/github_ci_linux_x86_omnibus.yaml index c3b7f43288..5e02ce5e64 100644 --- a/tests/ci/cdk/cdk/codebuild/github_ci_linux_x86_omnibus.yaml +++ b/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 diff --git a/tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml b/tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml deleted file mode 100644 index 917aeccd7b..0000000000 --- a/tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification.yml +++ /dev/null @@ -1,17 +0,0 @@ -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 OR ISC - -version: 0.2 - -env: - variables: - GOPROXY: https://proxy.golang.org,direct - -phases: - pre_build: - commands: - - export CC=clang-10 - - export CXX=clang++-10 - build: - commands: - - ./tests/ci/run_formal_verification.sh diff --git a/tests/ci/docker_images/linux-x86/build_images.sh b/tests/ci/docker_images/linux-x86/build_images.sh index 2f368609fe..ff845b856d 100755 --- a/tests/ci/docker_images/linux-x86/build_images.sh +++ b/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 # diff --git a/tests/ci/docker_images/linux-x86/push_images.sh b/tests/ci/docker_images/linux-x86/push_images.sh index 508a2a435f..dd97e66f82 100755 --- a/tests/ci/docker_images/linux-x86/push_images.sh +++ b/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" diff --git a/tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification-saw-aarch64/create_image.sh b/tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification-saw-aarch64/create_image.sh new file mode 100755 index 0000000000..4dd4a6a8a1 --- /dev/null +++ b/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 diff --git a/tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification/create_image.sh b/tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification-saw-x86_64/create_image.sh similarity index 85% rename from tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification/create_image.sh rename to tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification-saw-x86_64/create_image.sh index f2e4ed4faf..9a63ddf915 100755 --- a/tests/ci/docker_images/linux-x86/ubuntu-20.04_clang-10x_formal-verification/create_image.sh +++ b/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 diff --git a/tests/ci/docker_images/linux-x86/ubuntu-22.04_clang-14x_formal-verification-nsym-aarch64/create_image.sh b/tests/ci/docker_images/linux-x86/ubuntu-22.04_clang-14x_formal-verification-nsym-aarch64/create_image.sh new file mode 100755 index 0000000000..3b828f891d --- /dev/null +++ b/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 diff --git a/tests/ci/run_formal_verification.sh b/tests/ci/run_formal_verification.sh index e6c95bc934..3a877927bc 100755 --- a/tests/ci/run_formal_verification.sh +++ b/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 diff --git a/tests/ci/run_formal_verification_nsym_aarch64.sh b/tests/ci/run_formal_verification_nsym_aarch64.sh new file mode 100755 index 0000000000..e2fd4a1e08 --- /dev/null +++ b/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 diff --git a/tests/ci/run_formal_verification_saw_aarch64.sh b/tests/ci/run_formal_verification_saw_aarch64.sh new file mode 100755 index 0000000000..b0ea713ca5 --- /dev/null +++ b/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 diff --git a/tests/ci/run_formal_verification_saw_x86_64.sh b/tests/ci/run_formal_verification_saw_x86_64.sh new file mode 100755 index 0000000000..af71c5cfe1 --- /dev/null +++ b/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