Security • CI Verification
Verification Matrix
Below are the 12 automated checks configured for the current verification suite. The evidence shown here corresponds to commit e179d2b.
CI status for e179d2b: Passed
Verification specification revision: e179d2b – invariant definitions were updated at this commit; previous IDs may have changed. See the Changelog.
Important Clarification: Passing automated CI tests does not constitute a formal mathematical proof or an independent security audit. Each check demonstrates empirical conformance for the tested code paths and environment. For complete evidence chains, see the Evidence & Verification documentation.
Automated Properties Tested in CI
| ID | Tested Property | Level | Source Code | Test Code |
|---|---|---|---|---|
| INV-01 | Explicit surface: unregistered capability is denied | LEVEL 1 — UNIT TESTED | L295-L301 | L54-L62 |
| INV-02 | Explicit surface: wrong capability version is denied | LEVEL 1 — UNIT TESTED | L302-L307 | L64-L72 |
| INV-03 | Default-deny policy: no matching rule results in denial | LEVEL 1 — UNIT TESTED | L365-L382 | L74-L82 |
| INV-04 | Authoritative risk: caller claimedRisk cannot downgrade declared risk | LEVEL 1 — UNIT TESTED | L337-L347 | L84-L112 |
| INV-05 | Origin is a hint: unknown origin is never treated as local and escalates | LEVEL 1 — UNIT TESTED | L320-L325 | L114-L131 |
| INV-06 | Approval strategy defaults: high/critical risk is never automatic | LEVEL 1 — UNIT TESTED | L437-L449 | L133-L189 |
| INV-07 | Sandbox network deny-by-default: emits --unshare-net; unsupported allowlist throws | LEVEL 1 — UNIT TESTED | L140-L195 | L191-L217 |
| INV-08 | Ambient secrets stripped from child process environment | LEVEL 1 — UNIT TESTED | L85-L125 | L219-L243 |
| INV-09 | Single-use tickets: second redemption is rejected (replay check) | LEVEL 2 — INTEGRATION TESTED | L194-L206 | L245-L263 |
| INV-10 | Tickets are replay- and tamper-resistant via HMAC-SHA256 signatures | LEVEL 1 — UNIT TESTED | L159-L164 | L70-L86 |
| INV-11 | Replacing a capability invalidates previously issued outstanding tickets | LEVEL 2 — INTEGRATION TESTED | L232-L240 | L291-L323 |
| INV-12 | Approval substitution rejected: approval for challenge A cannot authorize B | LEVEL 2 — INTEGRATION TESTED | L470-L520 | L325-L380 |
CI Workflows & Runners
Tests are executed in Vitest under Node 24 on GitHub Actions runners. Platform sandboxes run on their specific OS runner in .github/workflows/sandbox.yml:
security.yml
Runs the 12 invariants on ubuntu-latest. Also runs pipeline and audit integration tests across an OS matrix (Ubuntu, macOS, Windows).
sandbox.yml
Executes real macOS Seatbelt tests on macos-15, bubblewrap checks on ubuntu-latest, and AppContainer checks on windows-latest.