From e2d9e5d8760b28db7536c29dd17fe1beb96b7f52 Mon Sep 17 00:00:00 2001 From: Andrew Hopkins Date: Tue, 1 Oct 2024 15:11:05 -0700 Subject: [PATCH 1/4] Pin the version of aws-lc-verification to a known working version --- tests/ci/run_formal_verification.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/ci/run_formal_verification.sh b/tests/ci/run_formal_verification.sh index c73aff7cc7..066fec6f89 100755 --- a/tests/ci/run_formal_verification.sh +++ b/tests/ci/run_formal_verification.sh @@ -7,8 +7,11 @@ cd ../ ROOT=$(pwd) rm -rf aws-lc-verification-build -git clone --recurse-submodules https://github.com/awslabs/aws-lc-verification.git aws-lc-verification-build +git clone https://github.com/awslabs/aws-lc-verification.git aws-lc-verification-build cd aws-lc-verification-build +# Checkout a version of the formal verification repo that works with this version of AWS-LC +git checkout 076973cc1ae011beab8df6af4f02464158374b24 +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 From cd2cf5b6f463ef2750814328e92442ee31180a58 Mon Sep 17 00:00:00 2001 From: Andrew Hopkins Date: Tue, 1 Oct 2024 16:34:47 -0700 Subject: [PATCH 2/4] Use older commit before P-384 changes --- tests/ci/run_formal_verification.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ci/run_formal_verification.sh b/tests/ci/run_formal_verification.sh index 066fec6f89..824b25826f 100755 --- a/tests/ci/run_formal_verification.sh +++ b/tests/ci/run_formal_verification.sh @@ -10,7 +10,7 @@ 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 # Checkout a version of the formal verification repo that works with this version of AWS-LC -git checkout 076973cc1ae011beab8df6af4f02464158374b24 +git checkout 7d0a46ac0841d1d9f1c078153d38409af056c482 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. From 45c43eba82875061b32240878c59e10e5c423153 Mon Sep 17 00:00:00 2001 From: Andrew Hopkins Date: Tue, 1 Oct 2024 17:26:45 -0700 Subject: [PATCH 3/4] Use newer commit to account for struct.EC_JACOBIAN --- tests/ci/run_formal_verification.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ci/run_formal_verification.sh b/tests/ci/run_formal_verification.sh index 824b25826f..cd7866b956 100755 --- a/tests/ci/run_formal_verification.sh +++ b/tests/ci/run_formal_verification.sh @@ -10,7 +10,7 @@ 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 # Checkout a version of the formal verification repo that works with this version of AWS-LC -git checkout 7d0a46ac0841d1d9f1c078153d38409af056c482 +git checkout e504944f94b6379eaf95f1146a168feb72ce844f 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. From b9709bf5452bcf7c5f98ad66db5ba98e72e0e422 Mon Sep 17 00:00:00 2001 From: Andrew Hopkins Date: Wed, 2 Oct 2024 14:12:51 -0700 Subject: [PATCH 4/4] Use specific 2022 FIPS branch, also depth 1 --- tests/ci/run_formal_verification.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/ci/run_formal_verification.sh b/tests/ci/run_formal_verification.sh index cd7866b956..3037d18b35 100755 --- a/tests/ci/run_formal_verification.sh +++ b/tests/ci/run_formal_verification.sh @@ -7,11 +7,11 @@ cd ../ ROOT=$(pwd) rm -rf aws-lc-verification-build -git clone https://github.com/awslabs/aws-lc-verification.git aws-lc-verification-build +git clone --branch fips-2022-11-02 --depth 1 https://github.com/awslabs/aws-lc-verification.git aws-lc-verification-build + cd aws-lc-verification-build -# Checkout a version of the formal verification repo that works with this version of AWS-LC -git checkout e504944f94b6379eaf95f1146a168feb72ce844f -git submodule update --init +git submodule update --init --depth 1 + # 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