From 05d399b4526d1b3af9211da87c13fa53f4cab36e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Sep 2025 11:13:30 +0200 Subject: [PATCH 1/3] Contain CI permissions to avoid global read-write Addresses code scanning alert. Co-authored-by: Copilot Autofix powered by AI <62310815+github-advanced-security[bot]@users.noreply.github.com> --- .github/workflows/release.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 3e56152b5f17..c4bfefef0a25 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -272,6 +272,8 @@ jobs: if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }} name: Release runs-on: ubuntu-24.04 + permissions: + contents: write needs: [build_bundle_macos_x86_64, build_bundle_macos_aarch64, build_bundle_linux_x86_64, build_bundle_linux_aarch64, test_bundle] outputs: version: ${{ steps.versioning.outputs.version }} From 3d839ae45320ddfe5f69287695b027504f4e37a8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Sep 2025 09:19:58 +0000 Subject: [PATCH 2/3] Mark other workflows as read-only --- .github/workflows/bench-compiler.yml | 4 +++- .github/workflows/bench-e2e.yml | 2 ++ .github/workflows/cbmc-latest.yml | 3 +++ .github/workflows/format-check.yml | 2 ++ .github/workflows/release.yml | 2 ++ .github/workflows/slow-tests.yml | 3 +++ .github/workflows/verify-std-check.yml | 2 ++ 7 files changed, 17 insertions(+), 1 deletion(-) diff --git a/.github/workflows/bench-compiler.yml b/.github/workflows/bench-compiler.yml index 7152eb6a7706..bf4bd6deafe9 100644 --- a/.github/workflows/bench-compiler.yml +++ b/.github/workflows/bench-compiler.yml @@ -3,6 +3,8 @@ # # Run performance benchmarks comparing the compiler performance of two different Kani versions. name: Kani Compiler Performance Benchmarks +permissions: + contents: read on: push: branches: @@ -161,4 +163,4 @@ jobs: export PATH="${{ github.workspace }}/new/scripts:$PATH" cd new/tests/perf/s2n-quic && ../../../target/release/compile-timer --out-path compile-times-new.json --also-visit quic/s2n-quic-core --also-visit quic/s2n-quic-platform --also-visit common/s2n-codec --skip-current - name: Run analysis between the two - run: ./new/target/release/compile-analyzer --path-pre old/tests/perf/s2n-quic/compile-times-old.json --path-post new/tests/perf/s2n-quic/compile-times-new.json --only-markdown --suite-name long >> "$GITHUB_STEP_SUMMARY" \ No newline at end of file + run: ./new/target/release/compile-analyzer --path-pre old/tests/perf/s2n-quic/compile-times-old.json --path-post new/tests/perf/s2n-quic/compile-times-new.json --only-markdown --suite-name long >> "$GITHUB_STEP_SUMMARY" diff --git a/.github/workflows/bench-e2e.yml b/.github/workflows/bench-e2e.yml index 196c401ec852..5f4eae1a4e13 100644 --- a/.github/workflows/bench-e2e.yml +++ b/.github/workflows/bench-e2e.yml @@ -7,6 +7,8 @@ # - Changes are pushed to 'main'. # - Triggered by another workflow name: Kani End-To-End Performance Benchmarks +permissions: + contents: read on: push: branches: diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index 6eb5c4788087..17680fd5702f 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -5,6 +5,9 @@ name: >- Nightly: CBMC Latest +permissions: + contents: read + on: schedule: - cron: "0 9 * * *" # Run this every day at 9 AM UTC (4 AM ET/1 AM PT) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index 3014c674dc07..88da968eea59 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -1,6 +1,8 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT name: Kani Format Check +permissions: + contents: read on: pull_request: merge_group: diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index c4bfefef0a25..765efdae744c 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -6,6 +6,8 @@ # The release will create a draft release and upload the bundles to it, and it will only run when we push a new # release tag (i.e.: tag named `kani-*`). name: Release Bundle +permissions: + contents: read on: pull_request: merge_group: diff --git a/.github/workflows/slow-tests.yml b/.github/workflows/slow-tests.yml index d7ab784aa22f..132b2d4a6f38 100644 --- a/.github/workflows/slow-tests.yml +++ b/.github/workflows/slow-tests.yml @@ -5,6 +5,9 @@ name: >- Nightly: Slow tests +permissions: + contents: read + on: schedule: - cron: "30 5 * * *" # Run this every day at 05:30 UTC diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml index 03a83cf53a56..f1fc12904b63 100644 --- a/.github/workflows/verify-std-check.yml +++ b/.github/workflows/verify-std-check.yml @@ -13,6 +13,8 @@ # Changes unrelated to the toolchain should match the current status of main. name: Check Std Verification +permissions: + contents: read on: pull_request: workflow_call: From cacf487a9b6bc12808accbdc48f7dd2590de91dc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Sep 2025 20:09:49 +0000 Subject: [PATCH 3/3] Fix permissions in extra_jobs.yml With the newly-restricted permissions we got an "Invalid workflow file" error in https://github.com/model-checking/kani/actions/runs/17593954849. --- .github/workflows/extra_jobs.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index df045c8da74b..78a7912fb549 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -18,6 +18,8 @@ # See https://github.com/actions/labeler?tab=readme-ov-file#recommended-permissions for more details. name: Kani Extra +permissions: + contents: read on: pull_request_target: merge_group: @@ -27,7 +29,6 @@ jobs: auto-label: name: Auto Label permissions: - contents: read pull-requests: write outputs: all-labels: ${{ steps.labeler.outputs.all-labels }} @@ -46,13 +47,11 @@ jobs: end-to-end-bench: name: End-to-End Benchmarks needs: auto-label - permissions: {} if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-EndToEndBenchCI') && github.event_name != 'merge_group' }} uses: ./.github/workflows/bench-e2e.yml compiler-bench: name: Compiler Benchmarks needs: auto-label - permissions: {} if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-CompilerBenchCI') && github.event_name != 'merge_group' }} uses: ./.github/workflows/bench-compiler.yml