diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7dca800588..6919a51091 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -740,10 +740,12 @@ jobs: # TODO(https://github.com/model-checking/kani-github-action/issues/56): # Go back to testing all features once the Kani GitHub Action supports # specifying a particular toolchain. - args: "--manifest-path zerocopy/Cargo.toml --package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse -Zfunction-contracts --randomize-layout --memory-safety-checks --overflow-checks --undefined-function-checks --unwinding-checks" + # Memory-safety, overflow, undefined-function, and unwinding checks + # are enabled by default. Kani 0.65 removed their positive flags. + args: "--manifest-path zerocopy/Cargo.toml --package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse -Zfunction-contracts --randomize-layout" # This version is automatically rolled by # `roll-pinned-toolchain-versions.yml`. - kani-version: 0.60.0 + kani-version: 0.67.0 # NEON intrinsics are currently broken on big-endian platforms. [1] This test ensures # that we don't accidentally attempt to compile these intrinsics on such platforms. We diff --git a/.github/workflows/roll-pinned-toolchain-versions.yml b/.github/workflows/roll-pinned-toolchain-versions.yml index 0a795c44dd..a0b108cadf 100644 --- a/.github/workflows/roll-pinned-toolchain-versions.yml +++ b/.github/workflows/roll-pinned-toolchain-versions.yml @@ -189,28 +189,48 @@ jobs: )" KANI_LATEST="$( sed -nE \ - 's/^kani-verifier = "([0-9]+\.[0-9]+\.[0-9]+)".*/\1/p' \ + 's/^kani-verifier = "((0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*))".*/\1/p' \ <<< "$KANI_SEARCH" )" - if ! [[ "$KANI_LATEST" =~ ^[0-9]+\.[0-9]+\.[0-9]+$ ]]; then + KANI_SEMVER_CORE='(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)' + KANI_VERSION_REGEX="^${KANI_SEMVER_CORE}$" + if ! [[ "$KANI_LATEST" =~ $KANI_VERSION_REGEX ]]; then echo "Could not parse a Kani version from: $KANI_SEARCH" >&2 exit 1 fi echo "ZC_KANI_LATEST=$KANI_LATEST" >> "$GITHUB_ENV" - # Update the `kani-version:` argument in-place. - MATCH_COUNT="$( - grep -Ec '^ *kani-version: [0-9]+\.[0-9]+\.[0-9]+$' \ - .github/workflows/ci.yml || true - )" - if [ "$MATCH_COUNT" -ne 1 ]; then - echo "Expected exactly one Kani version in ci.yml; found $MATCH_COUNT" >&2 + # Update only the executable `kani-version:` argument in-place. Do + # not mechanically update the manual compiler/CBMC audit in + # `agent_docs/validation.md`: on branches which carry that audit, + # `ci/check_actions.sh` deliberately fails until a human replaces + # the audit and its version label after checking the new release. + mapfile -t KANI_PIN_LINES < <( + # Count every non-comment textual candidate before requiring the + # one canonical spelling below. This catches quoted YAML keys, + # whitespace before `:`, and malformed duplicates. + awk ' + { + line = $0 + sub(/^[[:space:]]*/, "", line) + if (line !~ /^#/ && line ~ /kani-version/) print + } + ' .github/workflows/ci.yml + ) + if [ "${#KANI_PIN_LINES[@]}" -ne 1 ]; then + echo "Expected exactly one Kani pin candidate in ci.yml; found ${#KANI_PIN_LINES[@]}" >&2 + exit 1 + fi + KANI_PIN_LINE_REGEX="^([[:space:]]*)kani-version:[[:space:]]+${KANI_SEMVER_CORE}$" + if ! [[ "${KANI_PIN_LINES[0]}" =~ $KANI_PIN_LINE_REGEX ]]; then + echo "Malformed Kani pin in ci.yml: ${KANI_PIN_LINES[0]}" >&2 exit 1 fi + KANI_PIN_INDENT="${BASH_REMATCH[1]}" sed -i -E -e \ - "s/^( *kani-version:)( [0-9]+\.[0-9]+\.[0-9]+)/\1 $KANI_LATEST/" \ + "s/^([[:space:]]*)kani-version:[[:space:]]+${KANI_SEMVER_CORE}$/\1kani-version: $KANI_LATEST/" \ .github/workflows/ci.yml - grep -E "^ *kani-version: $KANI_LATEST$" \ + grep -F -x "${KANI_PIN_INDENT}kani-version: $KANI_LATEST" \ .github/workflows/ci.yml >/dev/null - name: Submit PR id: submit-pr @@ -220,6 +240,16 @@ jobs: author: Google PR Creation Bot committer: Google PR Creation Bot title: "[ci] Roll pinned Kani version" + body: | + This automation updates only the executable Kani pin; it does not + claim that the prior manual compiler/CBMC audit applies to the new + release. + + On branches carrying that audit, `ci/check_actions.sh` will fail + closed until a human installs the new release, replaces the + compiler/target/CBMC record, rechecks every versioned Rust contract + and tool-option premise, updates the audited-version label, and + reruns the complete Kani suite. branch: roll-pinned-kani-to-${{ env.ZC_KANI_LATEST }}-for-${{ matrix.branch }} push-to-fork: google-pr-creation-bot/zerocopy token: ${{ secrets.GOOGLE_PR_CREATION_BOT_TOKEN }} # zizmor: ignore[secrets-outside-env] diff --git a/ci/check_actions.sh b/ci/check_actions.sh index 12e56d4f67..de94cc592a 100755 --- a/ci/check_actions.sh +++ b/ci/check_actions.sh @@ -13,6 +13,70 @@ cd "$(dirname "$0")/.." script_name="ci/check_actions.sh" +# The Kani toolchain audit is manual: it records the bundled compiler, target, +# CBMC, option behavior, and the applicability of versioned Rust contracts. +# Require its visible version label to match the executable workflow pin so an +# automated pin-only roll cannot silently make that record stale. +semver_core='(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)' +kani_pin_line_regex="^[[:space:]]*kani-version:[[:space:]]+(${semver_core})$" +kani_audit_line_regex="^[[:space:]]*-[[:space:]]+\*\*Recorded toolchain audit for \`kani-version: (${semver_core})\`:\*\*.*$" + +# Count every candidate before parsing. A valid line must not hide an +# additional malformed or duplicate key/label. +kani_pin_lines=() +# Process substitution keeps this loop in the current shell, while `IFS=` and +# `read -r` preserve every candidate verbatim. This spelling works in Bash 3, +# which does not provide `mapfile`. +while IFS= read -r line || [[ -n "$line" ]]; do + kani_pin_lines[${#kani_pin_lines[@]}]="$line" +done < <( + # Deliberately conservative: catch quoted keys, whitespace before `:`, and + # other noncanonical YAML spellings. The strict parser below accepts only + # the one canonical line, so an equivalent duplicate cannot hide from the + # audit-version comparison. + awk ' + { + line = $0 + sub(/^[[:space:]]*/, "", line) + if (line !~ /^#/ && line ~ /kani-version/) print + } + ' .github/workflows/ci.yml +) +kani_audit_lines=() +while IFS= read -r line || [[ -n "$line" ]]; do + kani_audit_lines[${#kani_audit_lines[@]}]="$line" +done < <( + grep -F 'Recorded toolchain audit for' zerocopy/agent_docs/validation.md || true +) + +if [[ ${#kani_pin_lines[@]} -ne 1 ]]; then + echo "$script_name: expected exactly one Kani workflow-pin candidate; found ${#kani_pin_lines[@]}" >&2 + exit 1 +fi +if [[ ${#kani_audit_lines[@]} -ne 1 ]]; then + echo "$script_name: expected exactly one recorded Kani audit-label candidate; found ${#kani_audit_lines[@]}" >&2 + exit 1 +fi +if [[ "${kani_pin_lines[0]}" =~ $kani_pin_line_regex ]]; then + kani_version="${BASH_REMATCH[1]}" +else + echo "$script_name: malformed Kani workflow pin: '${kani_pin_lines[0]}'" >&2 + exit 1 +fi +if [[ "${kani_audit_lines[0]}" =~ $kani_audit_line_regex ]]; then + kani_audit_version="${BASH_REMATCH[1]}" +else + echo "$script_name: malformed recorded Kani audit label: '${kani_audit_lines[0]}'" >&2 + exit 1 +fi +if [[ "$kani_version" != "$kani_audit_version" ]]; then + printf '%s\n' \ + "$script_name: Kani $kani_version is pinned, but the manual toolchain audit covers Kani $kani_audit_version." \ + "$script_name: replace the compiler/target/CBMC audit, recheck every versioned contract and tool-option premise, update its version label, and rerun the complete Kani suite." \ + >&2 + exit 1 +fi + # Ensure action-validator is installed if [ ! -x "$HOME/.cargo/bin/action-validator" ]; then echo "$script_name: action-validator not found, installing..." >&2 diff --git a/tools/cargo-zerocopy/src/main.rs b/tools/cargo-zerocopy/src/main.rs index 7ca066aa8a..4cd8e20fa0 100644 --- a/tools/cargo-zerocopy/src/main.rs +++ b/tools/cargo-zerocopy/src/main.rs @@ -329,6 +329,15 @@ fn get_toolchain_rustflags(name: &str) -> String { format!("--cfg __ZEROCOPY_TOOLCHAIN=\"{}\"", name) } +fn join_flags(flags: &[&str]) -> String { + flags + .iter() + .map(|flag| flag.trim()) + .filter(|flag| !flag.is_empty()) + .collect::>() + .join(" ") +} + fn rustup<'a>(args: impl IntoIterator, env: Option<(&str, &str)>) -> Command { let mut cmd = Command::new("rustup"); // It's important to set `RUSTUP_TOOLCHAIN` to override any value set while @@ -414,13 +423,12 @@ fn delegate_cargo() -> Result<(), Error> { .next() .unwrap_or_default(); - let rustflags = format!( - "{} {} {}", - get_rustflags(name), - get_toolchain_rustflags(name), - env_rustflags, - ); - let rustdocflags = format!("{rustflags} {env_rustdocflags}"); + let rustflags = join_flags(&[ + &get_rustflags(name), + &get_toolchain_rustflags(name), + &env_rustflags, + ]); + let rustdocflags = join_flags(&[&rustflags, &env_rustdocflags]); // Rustdoc needs the wrapper's cfgs and the caller's RUSTFLAGS // in addition to any rustdoc-specific flags supplied through @@ -495,12 +503,20 @@ fn delegate_cargo() -> Result<(), Error> { mod tests { use std::{ffi::OsStr, process::Command}; - use super::{capture_feature_selection_args, set_ui_test_feature_args}; + use super::{capture_feature_selection_args, join_flags, set_ui_test_feature_args}; fn strings(args: &[&str]) -> Vec { args.iter().map(|arg| (*arg).to_string()).collect() } + #[test] + fn joins_nonempty_flags_without_outer_whitespace() { + assert_eq!( + join_flags(&["", " --cfg foo ", " ", "-C opt-level=2"]), + "--cfg foo -C opt-level=2" + ); + } + #[test] fn captures_feature_selection_before_separator() { let args = strings(&[ diff --git a/zerocopy/agent_docs/validation.md b/zerocopy/agent_docs/validation.md index feeadb7427..7bebeae74a 100644 --- a/zerocopy/agent_docs/validation.md +++ b/zerocopy/agent_docs/validation.md @@ -60,8 +60,10 @@ usually sufficient. - **Purpose:** Use the [Kani Rust Verifier](https://model-checking.github.io/kani/) to prove the soundness of `unsafe` code or code relied upon by `unsafe` blocks. Unlike - testing, which checks specific inputs, Kani proves properties for *all* - possible inputs. + testing, which checks selected executions, Kani exhaustively checks a + harness's modeled state space. That state space is limited by the + harness's bounds and assumptions, its target and feature configuration, + and Kani's model of Rust. - **How to Write Proofs:** - **Harnesses:** Mark proof functions with `#[kani::proof]`. - **Inputs:** Use `kani::any()` to generate arbitrary inputs. @@ -69,10 +71,112 @@ usually sufficient. valid states (e.g., `align.is_power_of_two()`). - **Assertions:** Use `assert!(condition)` to verify the properties you want to prove. - - **CI:** Kani runs in CI using the `model-checking/kani-github-action` with - specific feature flags to ensure compatibility. + - **Oracles:** Every oracle must be independent of the implementation + under proof. Prefer a safe Rust language or standard-library + operation whose documented contract directly supplies the expected + behavior. Do not call the target, reuse its zerocopy helper or policy, + or manually reconstruct the same unchecked operation. For every + oracle, state its normative basis, why it is independent, and its + limitations. If no safe oracle exists, isolate the smallest manual + rule and cite its normative basis. If a predicate merely restates a + zerocopy acceptance policy, label it as a policy oracle rather than + evidence of Rust-level validity. + - **Factoring:** Share repeated case generation, oracle construction, + and postcondition checks within the proof module. Keep distinct + harnesses when they exercise different entry points or contracts. + - **Domain:** Document every scope dimension independently: the + symbolic input domain; concrete size, allocation, loop, and unwind + bounds; assumptions and excluded boundary cases; Kani and bundled + compiler selection; target and data model; enabled features and + verifier flags; randomized-layout count or seed; the established + properties; and explicit non-goals. Shared configuration may be + factored into a nearby family or module scope only when every covered + harness refers to it unambiguously. + - **Bit validity:** `kani::any::()` produces only valid instances of + `T`. To verify a byte validator, generate arbitrary bytes and decide + expected acceptance using an independent oracle before consulting the + target. Never materialize `T` merely because the validator under + proof accepts: that validator may be the bug. Construct `T` only + through an independently safe checked operation. If no such operation + exists, exercise only a non-materializing decision path for invalid + candidates and document that limitation. + - **Soundness boundary:** State which obligations Kani does not prove. + In particular, Kani does not completely check reference aliasing, + pointer provenance, invalid values, or uninitialized memory. Kani's + official [Rust feature support] table marks breaking pointer aliasing + rules and producing invalid values as unsupported (where unsupported + analyses "should not be trusted"), and describes uninitialized-memory + checking as partial and experimental. Its [undefined-behaviour guide] + also explains the corresponding reference-lifetime and invalid-value + gaps. Treat conclusions that depend on those semantics as TOOL/TCB + premises rather than proof results. + - **Layout randomization:** `--randomize-layout` checks one randomized + layout per run; it does not prove behavior for every layout or target. + - **Kani CI configuration:** The exact Kani release is the single + `kani-version` pin in `.github/workflows/ci.yml`; its bundled compiler is + the proof toolchain. CI runs on `x86_64-unknown-linux-gnu` (64-bit, + little-endian) with + `__internal_use_only_features_that_work_on_stable` (`alloc`, `derive`, + `simd`, and `std`), `-Zfunction-contracts`, and one layout selected by + `--randomize-layout` per invocation. Source-level proof scopes should + refer to this common configuration and state any deviations. + - **Compiler and documentation compatibility:** After installing the + pinned Kani release, inspect the `kani-compiler` executable in that + release's installation directory (normally + `~/.kani/kani-/bin/kani-compiler`) with `--version --verbose`, + and inspect its data model with `--print cfg`. Proof premises must cite + versioned Rust Reference or standard-library documentation. When changing + the Kani pin, manually recheck every such premise against the new compiler + snapshot; mechanically changing citation versions does not establish that + a guarantee still applies. This compatibility check is a manual TOOL/TCB + premise: a successful Kani run does not itself establish that the cited + documentation describes the bundled compiler snapshot. + - **Fail-closed audit synchronization:** `ci/check_actions.sh`, run by + pre-push and CI, requires the `kani-version` pin to equal the version named + by the recorded audit below. The scheduled Kani roller intentionally + changes only the executable pin, so its PR cannot pass this check until a + human completes the audit workflow. Do not mechanically update the audit + version label: first install the new release; replace the compiler, + target, CBMC, and option-behavior record; recheck every versioned Rust + contract against the new compiler snapshot; and rerun the complete Kani + suite. Only then update the label to the new pin. + - **Recorded toolchain audit for `kani-version: 0.67.0`:** On 2026-09-08, + `kani-compiler --version --verbose` reported `rustc 1.93.0-nightly`, commit + `53732d5e076329a62f71d3c6901886ce8a71e812` dated 2025-11-20, LLVM 21.1.5, + and host `x86_64-unknown-linux-gnu`; `kani-compiler --print cfg` reported + Linux/gnu, x86_64, little endian, 64-bit pointers, and panic unwinding. + The bundled `cbmc --version` reported CBMC 6.8.0, and its `--help` + reported `--no-malloc-may-fail disable potential malloc failure` and + `--malloc-may-fail allow malloc calls to return a null pointer`. The + admitted compatibility proposition is that the versioned Rust 1.93.0 + contracts cited by the current proofs describe the corresponding + behavior of this nightly snapshot. This was checked manually, not proved + by Kani. Kani 0.67 [does not model stack unwinding][Kani panic strategies] + even though + its bundled compiler's target cfg reports `panic="unwind"`; proofs may + use reachable panics as failed properties but may not infer cleanup or + post-panic behavior. + +[Rust feature support]: https://model-checking.github.io/kani/rust-feature-support.html +[undefined-behaviour guide]: https://model-checking.github.io/kani/undefined-behaviour.html +[Kani panic strategies]: https://github.com/model-checking/kani/blob/kani-0.67.0/docs/src/rust-feature-support.md#panic-strategies + +Before running proofs locally, install the Kani version pinned in +`.github/workflows/ci.yml`. Run Kani locally through the required repository +wrapper with: - +```bash +./cargo.sh +stable kani \ + --package zerocopy \ + --features __internal_use_only_features_that_work_on_stable \ + --output-format=terse \ + -Zfunction-contracts \ + --randomize-layout +``` + +At this intermediate commit, CI invokes `cargo-kani` directly while the +wrapper injects project source-selection cfgs. Consequently, the local and CI +source-selection configurations are not identical. ## Feature Gates