From b0deaa07fac67a4eb2885c188cc4280cfeaac149 Mon Sep 17 00:00:00 2001 From: Doug Chapman <54039637+dougch@users.noreply.github.com> Date: Wed, 29 Jan 2025 09:45:23 -0800 Subject: [PATCH 1/4] Drop use of GITHUB_ENV --- .github/workflows/proof_ci.yaml | 17 ++++++++++------- .../workflows/proof_ci_resources/config.yaml | 9 --------- 2 files changed, 10 insertions(+), 16 deletions(-) delete mode 100644 .github/workflows/proof_ci_resources/config.yaml diff --git a/.github/workflows/proof_ci.yaml b/.github/workflows/proof_ci.yaml index 3a8423e5128..abeff8721aa 100644 --- a/.github/workflows/proof_ci.yaml +++ b/.github/workflows/proof_ci.yaml @@ -12,6 +12,16 @@ on: merge_group: types: [checks_requested] branches: [main] +env: + CMBC_VERSION: "6.2.0" + CMBC_VIEWER_VERSION: latest + KISSAT_TAG: latest + LITANI_VERSION: latest + Z3_VERSION: "4.13.0" + BITWUZLA_VERSION: "0.5.0" + PROOFS_DIR-dir: tests/cbmc/proofs + RUN_CBMC_PROOFS_COMMAND: ./run-cbmc-proofs.py + # USAGE # @@ -37,13 +47,6 @@ jobs: uses: actions/checkout@v4 with: submodules: 'recursive' - - name: Parse config file - run: | - CONFIG_FILE='.github/workflows/proof_ci_resources/config.yaml' - for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version z3-version bitwuzla-version proofs-dir run-cbmc-proofs-command; do - VAR=$(echo $setting | tr "[:lower:]" "[:upper:]" | tr - _) - echo "${VAR}"=$(yq .$setting $CONFIG_FILE) >> $GITHUB_ENV - done - name: Ensure CBMC, CBMC viewer, Litani, Z3, Bitwuzla versions have been specified shell: bash run: | diff --git a/.github/workflows/proof_ci_resources/config.yaml b/.github/workflows/proof_ci_resources/config.yaml deleted file mode 100644 index e78177d0427..00000000000 --- a/.github/workflows/proof_ci_resources/config.yaml +++ /dev/null @@ -1,9 +0,0 @@ -cadical-tag: latest -cbmc-version: "6.2.0" -cbmc-viewer-version: latest -kissat-tag: latest -litani-version: latest -z3-version: "4.13.0" -bitwuzla-version: "0.5.0" -proofs-dir: tests/cbmc/proofs -run-cbmc-proofs-command: ./run-cbmc-proofs.py From 4440989a87e0233f0cc086d284fb93f0793c7e7a Mon Sep 17 00:00:00 2001 From: Doug Chapman <54039637+dougch@users.noreply.github.com> Date: Tue, 4 Feb 2025 13:52:17 -0800 Subject: [PATCH 2/4] chore: ktls buildspec with CodeBuild reserved fleets --- codebuild/spec/buildspec_ktls.yml | 41 ++++++++++++++++++++----------- 1 file changed, 26 insertions(+), 15 deletions(-) diff --git a/codebuild/spec/buildspec_ktls.yml b/codebuild/spec/buildspec_ktls.yml index 1ed9938ed16..7ddb20ad879 100644 --- a/codebuild/spec/buildspec_ktls.yml +++ b/codebuild/spec/buildspec_ktls.yml @@ -11,26 +11,37 @@ # "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or # implied. See the License for the specific language governing permissions and # limitations under the License. +# This is designed to work with CodeBuild's reserved instances fleet and curated Ec2 AMI for AL2023. version: 0.2 +env: + shell: bash + variables: + NIX_CACHE_BUCKET: "s3://s2n-tls-nixcachebucket-x86-64?region=us-west-2" + S2N_KTLS_TESTING_EXPECTED: 1 phases: install: commands: - - apt update - - apt upgrade -y - - apt install -y qemu qemu-system-x86 wget cloud-image-utils + - yum update -y; yum upgrade -y pre_build: commands: - - aws s3 --quiet sync s3://s2n-ktls-testing ./qemu - - cd qemu; bash ./run.sh; cd .. - - rsync -avz --exclude=qemu --exclude=tests/fuzz -e 'ssh -p 2222' . codebuild@localhost:/home/codebuild/s2n-tls + - id; groupadd nixbld||true + - useradd -m -g nixbld -G nixbld nix || true + - | + echo "Working around the faulty yaml parser..." + echo 'nix ALL=NOPASSWD: ALL' > /etc/sudoers.d/nix + # (Re)Install nix + - sh <(curl -L https://nixos.org/nix/install) --no-daemon + # Make sure nix exists in the PATH + - export PATH=$HOME/.nix-profile/bin:$PATH + # Turn on flakes + - mkdir -p ~/.config/nix; echo "experimental-features = nix-command flakes" >> ~/.config/nix/nix.conf + # Populate the store from the nix cache + - nix copy --from $NIX_CACHE_BUCKET --all --no-check-sigs + # Load the TLS kernel module + - sudo modprobe tls + - echo "Checking that the TLS kernel mod loaded..."; test $(sudo lsmod|grep -c tls) = 1 build: commands: - - codebuild-breakpoint - - | - ssh -p 2222 codebuild@localhost " \ - cd s2n-tls; sudo modprobe tls; \ - export S2N_CMAKE_OPTIONS=${S2N_CMAKE_OPTIONS}; \ - export S2N_KTLS_TESTING_EXPECTED=1; \ - nix develop .#openssl111 --command bash -c \ - 'source ./nix/shell.sh && clean && configure && unit' \ - " + - nix develop .#openssl111 --command bash -c 'source ./nix/shell.sh && clean && configure && unit' + - S2N_CMAKE_OPTIONS="-DASAN=ON" nix develop .#openssl111 --command bash -c 'source ./nix/shell.sh && clean && configure && unit' + From 99658d9a1fac2ed189892b70b580431c73ebb499 Mon Sep 17 00:00:00 2001 From: Doug Chapman <54039637+dougch@users.noreply.github.com> Date: Tue, 4 Feb 2025 14:00:12 -0800 Subject: [PATCH 3/4] Revert unrelated changes --- .github/workflows/proof_ci.yaml | 17 +++++++---------- .../workflows/proof_ci_resources/config.yaml | 9 +++++++++ 2 files changed, 16 insertions(+), 10 deletions(-) create mode 100644 .github/workflows/proof_ci_resources/config.yaml diff --git a/.github/workflows/proof_ci.yaml b/.github/workflows/proof_ci.yaml index abeff8721aa..3a8423e5128 100644 --- a/.github/workflows/proof_ci.yaml +++ b/.github/workflows/proof_ci.yaml @@ -12,16 +12,6 @@ on: merge_group: types: [checks_requested] branches: [main] -env: - CMBC_VERSION: "6.2.0" - CMBC_VIEWER_VERSION: latest - KISSAT_TAG: latest - LITANI_VERSION: latest - Z3_VERSION: "4.13.0" - BITWUZLA_VERSION: "0.5.0" - PROOFS_DIR-dir: tests/cbmc/proofs - RUN_CBMC_PROOFS_COMMAND: ./run-cbmc-proofs.py - # USAGE # @@ -47,6 +37,13 @@ jobs: uses: actions/checkout@v4 with: submodules: 'recursive' + - name: Parse config file + run: | + CONFIG_FILE='.github/workflows/proof_ci_resources/config.yaml' + for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version z3-version bitwuzla-version proofs-dir run-cbmc-proofs-command; do + VAR=$(echo $setting | tr "[:lower:]" "[:upper:]" | tr - _) + echo "${VAR}"=$(yq .$setting $CONFIG_FILE) >> $GITHUB_ENV + done - name: Ensure CBMC, CBMC viewer, Litani, Z3, Bitwuzla versions have been specified shell: bash run: | diff --git a/.github/workflows/proof_ci_resources/config.yaml b/.github/workflows/proof_ci_resources/config.yaml new file mode 100644 index 00000000000..e78177d0427 --- /dev/null +++ b/.github/workflows/proof_ci_resources/config.yaml @@ -0,0 +1,9 @@ +cadical-tag: latest +cbmc-version: "6.2.0" +cbmc-viewer-version: latest +kissat-tag: latest +litani-version: latest +z3-version: "4.13.0" +bitwuzla-version: "0.5.0" +proofs-dir: tests/cbmc/proofs +run-cbmc-proofs-command: ./run-cbmc-proofs.py From c62fbdb80474f161a8fb16c3837fa6b0c7c34e08 Mon Sep 17 00:00:00 2001 From: Doug Chapman <54039637+dougch@users.noreply.github.com> Date: Wed, 5 Feb 2025 11:40:10 -0800 Subject: [PATCH 4/4] PR feedback; switch ktls job to use awslc --- codebuild/spec/buildspec_ktls.yml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/codebuild/spec/buildspec_ktls.yml b/codebuild/spec/buildspec_ktls.yml index 7ddb20ad879..bfe71eedb64 100644 --- a/codebuild/spec/buildspec_ktls.yml +++ b/codebuild/spec/buildspec_ktls.yml @@ -11,8 +11,11 @@ # "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or # implied. See the License for the specific language governing permissions and # limitations under the License. -# This is designed to work with CodeBuild's reserved instances fleet and curated Ec2 AMI for AL2023. + version: 0.2 +# This is designed to work with CodeBuild's reserved instances fleet and +# curated Ec2 AMI for AL2023. +# TODO: Move to a NixOS AMI env: shell: bash variables: @@ -42,6 +45,6 @@ phases: - echo "Checking that the TLS kernel mod loaded..."; test $(sudo lsmod|grep -c tls) = 1 build: commands: - - nix develop .#openssl111 --command bash -c 'source ./nix/shell.sh && clean && configure && unit' - - S2N_CMAKE_OPTIONS="-DASAN=ON" nix develop .#openssl111 --command bash -c 'source ./nix/shell.sh && clean && configure && unit' + - nix develop .#awslc --command bash -c 'source ./nix/shell.sh && clean && configure && unit' + - S2N_CMAKE_OPTIONS="-DASAN=ON" nix develop .#awslc --command bash -c 'source ./nix/shell.sh && clean && configure && unit'