Repository navigation
Strengthen TLA+ token-lifetime checks for failed jobs - #65904
Conversation
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
|
Great work strengthening the token-lifetime invariants in the TLA+ security model! Exhaustive checks across 10 configurations, 21 negative controls and conformance tests make this look ready for review. 🎯
|
|
@copilot the post step of actions/create-action-token automatically invalidates the minted token. Integrate in TLA+ specification. |
|
@copilot actions also automatically prevent cross-job token communication through action outputs |
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
The queue schema restriction conflicts with an existing test that still expects expression-valued queues to pass validation.
Review effort: Balanced
Findings: 1
Open (1)
What changed in this PR
Strengthens gh-aw’s security model to check token cleanup after failed jobs, without claiming a product vulnerability.
Changes:
- Extends token-lifetime invariants and adds a synthetic retention fault.
- Refreshes the TLC checksum, example metadata, and compiled workflow.
- Restricts concurrency queue values to literals.
| File | Description |
|---|---|
| specs/workflow-security/README.md | Documents failure-path checks and updated checksum. |
| specs/workflow-security/examples.json | Refreshes model and runtime hashes. |
| specs/workflow-security/CompiledWorkflow.tla | Strengthens invariants and adds retention fault. |
| specs/workflow-security/check.py | Registers the fault and updates checksum. |
| pkg/workflow/schemas/github-workflow.json | Limits queue values to single or max. |
| .github/workflows/daily-workflow-security-model.md | Updates pinned TLC checksum. |
| .github/workflows/daily-workflow-security-model.lock.yml | Synchronizes the compiled workflow. |
| "type": "string", | ||
| "enum": ["single", "max"], |
Modeled token revocation as the |
Modeled the masked token as a same-job action output and GitHub Actions redaction at the job-output boundary, with a synthetic bypass mutation and trace for |
|
🎉 This pull request is included in a new release. Release: |
The compiler/job/secrets model checked token cleanup after successful jobs but did not assert it after failures. The review also found that the pinned TLC checksum no longer matched the upstream v1.8.0 asset.