Repository navigation
Add TLA+ workflow security model and fail-closed credential cleanup - #65423
Merged
Merged
Conversation
Model job and step boundaries, classified artifacts and outputs, scoped secrets and GitHub App permissions, private sinks, and per-checkout git semantics. Add bounded TLC checks, mutation controls, witness traces, source concretization, and compiled-YAML conformance checks. Add a daily TLA+ investigation workflow with security critical finding labels and restricted model-refinement PRs. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
Add independent compiler detection-policy metadata, policy-aware conformance, AST guard checks, and trusted invocation artifact matching. Make checkout-time and pre-agent credential cleanup fail closed and verify effective git configuration without logging secrets. Extend TLA+ with cleanup failure, invocation provenance and detector modes, expand regression controls, refresh generated workflows and golden fixtures, and run corpus validation in the daily expert. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
pelikhan
marked this pull request as ready for review
October 3, 2026 20:46
Collaborator
Author
|
@copilot resolve the merge conflicts on this branch. |
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
Effective global Git credentials remain unchecked, and conformance does not enforce final pre-agent verification.
Review effort: Balanced
Findings: 1
Open (2)
What changed in this PR
Adds a bounded workflow-security model, compiled-YAML conformance checks, and fail-closed Git credential cleanup.
Changes:
- Adds TLA+ security-model fixtures and conformance validation.
- Verifies credential removal before agent execution.
- Emits detection-policy metadata and regenerates workflows.
| File | Description |
|---|---|
specs/workflow-security/fixtures/cross-repo.md |
Adds model fixture. |
specs/workflow-security/conformance/policy.go |
Validates detection policy. |
specs/workflow-security/conformance/policy_test.go |
Tests policy validation. |
specs/workflow-security/conformance/guards.go |
Analyzes workflow guards. |
specs/workflow-security/conformance/guards_test.go |
Tests guard analysis. |
specs/workflow-security/conformance/conformance.go |
Implements YAML conformance. |
specs/workflow-security/conformance/conformance_test.go |
Tests profile mutations. |
specs/workflow-security/conformance/checkout.go |
Checks checkout cleanup. |
specs/workflow-security/conformance/checkout_test.go |
Tests credential lifecycle. |
specs/workflow-security/conformance/artifacts.go |
Checks artifact provenance. |
specs/workflow-security/conformance/artifacts_test.go |
Tests artifact checks. |
specs/workflow-security/CompiledWorkflow.cfg |
Configures TLA+ invariants. |
specs/workflow-security/check_test.py |
Tests model runner contracts. |
pkg/workflow/testdata/TestWasmGolden_CompileFixtures/with-imports.golden |
Updates generated cleanup. |
pkg/workflow/testdata/TestWasmGolden_CompileFixtures/playwright-cli-mode.golden |
Updates generated cleanup. |
pkg/workflow/testdata/TestWasmGolden_CompileFixtures/basic-copilot.golden |
Updates generated cleanup. |
pkg/workflow/testdata/TestWasmGolden_AllEngines/pi.golden |
Updates Pi output. |
pkg/workflow/testdata/TestWasmGolden_AllEngines/gemini.golden |
Updates Gemini output. |
pkg/workflow/testdata/TestWasmGolden_AllEngines/copilot.golden |
Updates Copilot output. |
pkg/workflow/testdata/TestWasmGolden_AllEngines/codex.golden |
Updates Codex output. |
pkg/workflow/testdata/TestWasmGolden_AllEngines/claude.golden |
Updates Claude output. |
pkg/workflow/security_model_manifest_test.go |
Tests policy metadata. |
pkg/workflow/safe_update_manifest.go |
Adds detection metadata. |
pkg/workflow/known_action_credentials_test.go |
Tests fail-closed cleanup. |
pkg/workflow/git_configuration_steps.go |
Adds credential verification. |
pkg/workflow/git_config_test.go |
Updates cleanup tests. |
pkg/workflow/compiler_yaml_header.go |
Emits policy manifest data. |
pkg/workflow/checkout_input_render.go |
Extracts checkout rendering. |
pkg/workflow/checkout_credentials_verification_test.go |
Tests verification failures. |
pkg/workflow/checkout_credentials_render.go |
Extracts credential rendering. |
docs/src/content/docs/specs/checkout-behavior-specification.md |
Specifies fail-closed behavior. |
docs/src/content/docs/reference/checkout.md |
Documents verification. |
cmd/gh-aw-security-model/main.go |
Adds verifier command. |
actions/setup/sh/verify_git_credentials.sh |
Verifies Git configuration. |
.github/workflows/windows.lock.yml |
Regenerates Windows workflow. |
.github/workflows/smoke-github-codex.lock.yml |
Regenerates smoke workflow. |
.github/workflows/smoke-copilot-auto.lock.yml |
Regenerates smoke workflow. |
.github/workflows/smoke-codex-auto.lock.yml |
Regenerates smoke workflow. |
.github/workflows/schema-feature-coverage.lock.yml |
Regenerates schema workflow. |
.github/workflows/issue-triage-agent.lock.yml |
Regenerates triage workflow. |
.github/workflows/issue-arborist.lock.yml |
Regenerates arborist workflow. |
.github/workflows/github-remote-mcp-auth-test.lock.yml |
Regenerates MCP test. |
.github/workflows/firewall.lock.yml |
Regenerates firewall workflow. |
.github/workflows/daily-team-status.lock.yml |
Regenerates status workflow. |
.github/workflows/daily-spec-coverage-kiro.lock.yml |
Regenerates coverage workflow. |
.github/workflows/daily-schema-audit-cursor.lock.yml |
Regenerates audit workflow. |
.github/workflows/daily-regression-audit-kiro.lock.yml |
Regenerates regression workflow. |
.github/workflows/daily-github-docs-seo-optimizer.lock.yml |
Regenerates SEO workflow. |
.github/workflows/daily-ecosystem-explorer.lock.yml |
Regenerates explorer workflow. |
.github/workflows/daily-credit-limit-test.lock.yml |
Regenerates credit test. |
.github/workflows/daily-community-attribution.lock.yml |
Regenerates attribution workflow. |
.github/workflows/copilot-pr-merged-report.lock.yml |
Regenerates report workflow. |
.github/workflows/codex-github-remote-mcp-test.lock.yml |
Regenerates MCP test. |
.github/workflows/breaking-change-checker.lock.yml |
Regenerates checker workflow. |
.github/workflows/auto-triage-issues.lock.yml |
Regenerates auto-triage workflow. |
.github/workflows/artifacts-summary.lock.yml |
Regenerates artifact workflow. |
.github/workflows/agentic-token-optimizer.lock.yml |
Regenerates optimizer workflow. |
.github/skills/agentic-workflows/SKILL.md |
Adds work-queue guidance reference. |
| verify_config() { | ||
| local config="$1" entry key status=0 | ||
| snapshot=$(mktemp "${RUNNER_TEMP:-${TMPDIR:-/tmp}}/gh-aw-git-config.XXXXXX") | ||
| if ! git --git-dir="${config%/*}" config --file "$config" --includes --null --list >"$snapshot"; then |
| violations = append(violations, "JobIsolation: agent write scope "+scope) | ||
| } | ||
| } | ||
| violations = append(violations, checkCheckoutCredentials(agent.Steps)...) |
Collaborator
Author
|
@copilot resolve the merge conflicts on this branch. |
Contributor
Resolved the merge conflicts in merge commit |
…urity-formalization # Conflicts: # .github/workflows/agent-job-health.lock.yml # .github/workflows/ai-moderator.lock.yml # .github/workflows/approach-validator.lock.yml # .github/workflows/archivx-agentic-workflows-analyzer.lock.yml # .github/workflows/aw-failure-investigator.lock.yml # .github/workflows/blog-auditor.lock.yml # .github/workflows/claude-code-user-docs-review.lock.yml # .github/workflows/cli-version-checker.lock.yml # .github/workflows/code-scanning-fixer.lock.yml # .github/workflows/copilot-agent-analysis.lock.yml # .github/workflows/copilot-session-insights.lock.yml # .github/workflows/daily-agentrx-trace-optimizer.lock.yml # .github/workflows/daily-arxiv-researcher.lock.yml # .github/workflows/daily-astrostylelite-markdown-spellcheck.lock.yml # .github/workflows/daily-aw-cross-repo-compile-check.lock.yml # .github/workflows/daily-caveman-optimizer.lock.yml # .github/workflows/daily-choice-test.lock.yml # .github/workflows/daily-credit-limit-test.lock.yml # .github/workflows/daily-doc-healer.lock.yml # .github/workflows/daily-elixir-credo-snippet-audit.lock.yml # .github/workflows/daily-formal-spec-verifier.lock.yml # .github/workflows/daily-function-namer.lock.yml # .github/workflows/daily-grader-audit.lock.yml # .github/workflows/daily-harness-experiment-proposer.lock.yml # .github/workflows/daily-hippo-learn.lock.yml # .github/workflows/daily-multi-device-docs-tester.lock.yml # .github/workflows/daily-news.lock.yml # .github/workflows/daily-performance-summary.lock.yml # .github/workflows/daily-rendering-scripts-verifier.lock.yml # .github/workflows/daily-repo-chronicle.lock.yml # .github/workflows/daily-safe-output-optimizer.lock.yml # .github/workflows/daily-safe-outputs-conformance.lock.yml # .github/workflows/daily-safeoutputs-git-simulator.lock.yml # .github/workflows/daily-security-red-team.lock.yml # .github/workflows/daily-spdd-spec-planner.lock.yml # .github/workflows/daily-vulnhunter-scan.lock.yml # .github/workflows/daily-yamllint-fixer.lock.yml # .github/workflows/deep-report.lock.yml # .github/workflows/deepsec-security-scan.lock.yml # .github/workflows/design-decision-gate.lock.yml # .github/workflows/detection-analysis-report.lock.yml # .github/workflows/developer-docs-consolidator.lock.yml # .github/workflows/duplicate-code-detector.lock.yml # .github/workflows/eslint-refiner.lock.yml # .github/workflows/example-workflow-analyzer.lock.yml # .github/workflows/github-mcp-structural-analysis.lock.yml # .github/workflows/github-mcp-tools-report.lock.yml # .github/workflows/go-fan.lock.yml # .github/workflows/go-logger.lock.yml # .github/workflows/go-pattern-detector.lock.yml # .github/workflows/hippo-embed.lock.yml # .github/workflows/hourly-ci-cleaner.lock.yml # .github/workflows/instructions-janitor.lock.yml # .github/workflows/lockfile-stats.lock.yml # .github/workflows/necromancer.lock.yml # .github/workflows/portfolio-analyst.lock.yml # .github/workflows/pr-sous-chef.lock.yml # .github/workflows/prompt-clustering-analysis.lock.yml # .github/workflows/refactoring-cadence.lock.yml # .github/workflows/repo-tree-map.lock.yml # .github/workflows/research.lock.yml # .github/workflows/ruflo-backed-task.lock.yml # .github/workflows/safe-output-health.lock.yml # .github/workflows/scout.lock.yml # .github/workflows/semantic-function-refactor.lock.yml # .github/workflows/sergo.lock.yml # .github/workflows/smoke-agent-all-merged.lock.yml # .github/workflows/smoke-agent-all-none.lock.yml # .github/workflows/smoke-agent-public-approved.lock.yml # .github/workflows/smoke-agent-public-none.lock.yml # .github/workflows/smoke-agent-scoped-approved.lock.yml # .github/workflows/smoke-claude-on-copilot.lock.yml # .github/workflows/smoke-claude.lock.yml # .github/workflows/smoke-copilot-aoai-entra.lock.yml # .github/workflows/smoke-github-claude.lock.yml # .github/workflows/smoke-opencode.lock.yml # .github/workflows/smoke-service-ports.lock.yml # .github/workflows/smoke-temporary-id.lock.yml # .github/workflows/smoke-test-tools.lock.yml # .github/workflows/smoke-work-queue.lock.yml # .github/workflows/smoke-workflow-call.lock.yml # .github/workflows/stale-repo-identifier.lock.yml # .github/workflows/static-analysis-report.lock.yml # .github/workflows/step-name-alignment.lock.yml # .github/workflows/sub-issue-closer.lock.yml # .github/workflows/super-linter.lock.yml # .github/workflows/terminal-stylist.lock.yml # .github/workflows/typist.lock.yml # .github/workflows/unbloat-docs.lock.yml # .github/workflows/video-analyzer.lock.yml # .github/workflows/weekly-issue-summary.lock.yml # .github/workflows/weekly-network-domains-audit.lock.yml # .github/workflows/weekly-safe-outputs-spec-review.lock.yml Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Contributor
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Collaborator
Author
|
@copilot resolve the merge conflicts on this branch. |
…urity-formalization # Conflicts: # .github/workflows/smoke-builtin-ledgers.lock.yml # .github/workflows/smoke-repo-memory-ledger.lock.yml Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Contributor
Merged |
Collaborator
Author
|
@copilot resolve the merge conflicts on this branch. |
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
…urity-formalization # Conflicts: # .github/workflows/smoke-claude.lock.yml # .github/workflows/smoke-codex.lock.yml # .github/workflows/smoke-copilot-aoai-apikey.lock.yml # .github/workflows/smoke-copilot-aoai-entra.lock.yml # .github/workflows/smoke-copilot-arm.lock.yml # .github/workflows/smoke-copilot.lock.yml # .github/workflows/smoke-crush.lock.yml # .github/workflows/smoke-cursor.lock.yml # .github/workflows/smoke-deepseek-harness.lock.yml # .github/workflows/smoke-gemini.lock.yml # .github/workflows/smoke-goose.lock.yml # .github/workflows/smoke-kiro.lock.yml # .github/workflows/smoke-opencode.lock.yml # .github/workflows/smoke-project.lock.yml # .github/workflows/smoke-service-ports.lock.yml # .github/workflows/smoke-temporary-id.lock.yml # .github/workflows/smoke-test-tools.lock.yml Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Contributor
Merged the latest |
Collaborator
Author
|
@copilot resolve the merge conflicts on this branch. |
…urity-formalization # Conflicts: # .github/workflows/avenger.lock.yml # .github/workflows/pr-triage-agent.lock.yml Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Contributor
Merged the latest |
Contributor
|
🎉 This pull request is included in a new release. Release: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Motivation
Add an executable security reference model for compiled agentic workflows so trust-boundary regressions can be explored systematically. Exercising the initial validator against existing workflows exposed unsupported representations and a genuine failure path: ignored credential-cleanup errors could allow agent execution with retained checkout credentials.
Fixes #65421
Approach
security criticalthrough safe outputs.Review considerations
This is bounded reference-model checking plus structural conformance, not an unbounded proof or a complete behavioral refinement of every workflow. External enforcement, manifest provenance, arbitrary scripts, and some warning-mode behavior remain explicit assumptions or refinement work.
The corpus reports detection policy separately: 290 workflows have detection enabled and 15 have compiler-declared disabled policies. Passing the latter does not claim equivalent detector assurance. The finding label is a triage marker, not a demonstrated exploit severity.
Most changed files are regenerated workflow locks and compiler golden fixtures. Touched renderers were split into bounded helpers to satisfy repository linters; a hash comparison confirmed the refactor preserved all 305 compiled outputs.
Validation
make fmt,make recompile, and the finalmake agent-report-progresspassed.TestDailyCacheStrategyAnalyzerUsesCodexCompatibleModels,TestDailyGoTestParallelizerUsesCodexCompatibleModel,TestDailyCLIPerformanceUsesCodexCompatibleModel, andTestCodexWorkflowsUseCodexModels. These also fail at the unchanged pre-fix commit01db09fde7and were not modified.