Skip to content

Commit

Permalink
Enable Arm SHA384 proofs in AWS-LC CI
Browse files Browse the repository at this point in the history
  • Loading branch information
pennyannn committed Dec 8, 2023
1 parent c7c418a commit 1d5f407
Show file tree
Hide file tree
Showing 12 changed files with 122 additions and 86 deletions.
94 changes: 12 additions & 82 deletions tests/ci/cdk/cdk/codebuild/github_ci_linux_x86_omnibus.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -449,106 +449,36 @@ 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
# SAW proofs on platform X86_64
- identifier: ubuntu2004_clang10x_formal_verification_saw_x86_64
buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification-saw-x86_64.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

# 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
# SAW proofs on platform AArch64
- identifier: ubuntu2004_clang10x_formal_verification_saw_aarch64
buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-20.04_clang-10x_formal-verification-saw-aarch64.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
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: 290
AES_GCM_SELECTCHECK_END: 325

- identifier: ubuntu2004_clang10x_formal_verification_aes_gcm_selectcheck_326_356
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: 326
AES_GCM_SELECTCHECK_END: 356
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

- 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
buildspec: ./tests/ci/codebuild/linux-x86/ubuntu-22.04_clang-14x_formal-verification-nsym.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: 357
AES_GCM_SELECTCHECK_END: 384
image: 620771051181.dkr.ecr.us-west-2.amazonaws.com/aws-lc-docker-images-linux-x86:ubuntu-22.04_clang-14x_formal-verification-nsym_latest

# Build and test aws-lc without Perl/Go.
- identifier: amazonlinux2_gcc7x_x86_64_minimal
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
# 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_saw_aarch64.sh
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,4 @@ phases:
- export CXX=clang++-10
build:
commands:
- ./tests/ci/run_formal_verification.sh
- ./tests/ci/run_formal_verification_saw_x86_64.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# 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:
build:
commands:
- ./tests/ci/run_formal_verification_nsym.sh
4 changes: 3 additions & 1 deletion tests/ci/docker_images/linux-x86/build_images.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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/create_image.sh ubuntu-22.04:clang-14x_formal-verification-nsym

###########################################################
# Build older unofficial docker image that uses gcc 4.1.3 #
Expand Down
4 changes: 3 additions & 1 deletion tests/ci/docker_images/linux-x86/push_images.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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' "${ECS_REPO}:ubuntu-22.04_clang-14x_formal-verification-nsym"
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"
Expand Down
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -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'
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
21 changes: 21 additions & 0 deletions tests/ci/run_formal_verification_nsym.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
#!/bin/bash -ex
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: Apache-2.0 OR ISC

AWS_LC_DIR=${PWD##*/}
cd ../
ROOT=$(pwd)

rm -rf aws-lc-verification-build
git clone https://github.com/awslabs/aws-lc-verification.git aws-lc-verification-build

cd aws-lc-verification-build
git submodule update --init

# aws-lc-verification has aws-lc as one submodule under 'src' dir.
# 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.
./NSym/scripts/docker_entrypoint.sh
cd ..
rm -rf aws-lc-verification-build
21 changes: 21 additions & 0 deletions tests/ci/run_formal_verification_saw_aarch64.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
#!/bin/bash -ex
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: Apache-2.0 OR ISC

AWS_LC_DIR=${PWD##*/}
cd ../
ROOT=$(pwd)

rm -rf aws-lc-verification-build
git clone https://github.com/awslabs/aws-lc-verification.git aws-lc-verification-build

cd aws-lc-verification-build
git submodule update --init

# aws-lc-verification has aws-lc as one submodule under 'src' dir.
# 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/aarch64/docker_entrypoint.sh
cd ..
rm -rf aws-lc-verification-build
File renamed without changes.

0 comments on commit 1d5f407

Please sign in to comment.