V3.35: Verifiable Security — Making Trust Measurable

[deeprnd]

Security must be measurable, not aspirational. V3.35 transforms Tickoni's security from a
plan on paper into a chain of 14 enforceable, deterministic proofs — CodeQL, CBMC proofs,
seccomp validation, clang-tidy, dependency scanning, CI workflow analysis, fuzzing, formal
verification, property invariants, replay determinism, SBOM generation, and binary
hardening. Before this epic, security checks either existed as aspirational references or
executed as no-ops. After V3.35, every lane produces a deterministic pass/fail result
on every run. No skips. No tool-not-found fallbacks. One command shows the full security
posture — the way a financial operator should be able to verify a system's trust boundary.

This epic consolidates the 2026 security tooling plan across Tickoni's CI pipeline,
fixing existing checks that execute as no-ops, adding missing scanners (clang-tidy,
OSV-Scanner, zizmor, TSan, fuzzing), validating the actual architecture with negative
seccomp tests and Tickoni-specific property tests, and hardening release artifacts with
SBOM generation and binary inspection. The transformation is not "we added more tools" —
it is "every claim Tickoni makes about security is now backed by a verifiable gate
that runs on every commit."

Product Intent

Security is not a promise — it's a chain of verifiable proofs.

V3.35 makes security measurable, not aspirational. Every tool in the recommended
stack executes as a real CI gate with deterministic pass/fail. No "tool not found"
excuses. No silent skips. No fallback-to-no-op when a scanner is missing. The
security machinery itself is protected with CODEOWNERS and repository rules. The
operator can look at the CI status page and understand, in one glance, whether
every security layer is passing.

The transformation is structural: security stops being a list of tools that
should run and becomes a chain of gates that must pass. Every claim Tickoni
makes about security is now backed by a deterministic verification that runs on
every commit and every release.

Users And Jobs

• Security reviewer: run just security-check-all and see deterministic results from every layer (SAST, dependency, runtime safety, fuzzing, formal verification, isolation, property tests, supply chain).
• CI workflow author: add a new lane or modify an existing check without guessing which scripts to touch — fully-qualified just recipes from V2.10 handle routing.
• New contributor: commit changes and see targeted security feedback (CodeQL for C/C++, clang-tidy, OSV-Scanner, Gitleaks) before a reviewer has to inspect.
• Release operator: verify that every release artifact has an SBOM, a CVE scan, and a binary hardening check before distribution.

Success Metrics

• CodeQL executes a real build-based database in CI and blocks PRs on findings above the configured threshold.
• CBMC proofs run in CI as a required check with a defined set of proof entry points.
• seccomp checks invoke the real policy validation path and fail closed if the tool is unavailable.
• clang-tidy + Clang Static Analyzer runs on C/C++ changes with clang-analyzer-*, bugprone-*, cert-*, concurrency-* rule families.
• OSV-Scanner runs on every PR against vendored and source-level dependencies.
• zizmor scans .github/ on every PR for unpinned actions, excessive permissions, and unsafe workflow triggers.
• TSan runs as a separate CI lane from ASan/UBSan and flags data races on queue ownership, audit state, replay state, and policy state.
• libFuzzer + ASan/UBSan fuzz targets cover parsers, protocol decoders, C/Zig ABI boundaries, configuration readers, event decoding, and policy inputs.
• Zig built-in fuzzer covers the same trust boundaries for Zig code.
• seccomp/Landlock/capability negative tests prove that forbidden operations actually fail (SIGSYS, denial, impossible escalation).
• Tickoni-specific property tests run as CI gates: exposure <= configured_limit, unknown capability => deny, missing policy => deny, audit log is append-only, replayed identical input produces identical security decision.
• SBOMs generated with Syft in CycloneDX JSON for every release artifact.
• Grype scans release SBOMs for known vulnerabilities.
• Release binaries pass hardening checks: PIE, NX, full RELRO, stack protector, FORTIFY_SOURCE, CET/IBT/shadow-stack where supported.
• All third-party GitHub Actions pinned to full commit SHAs with Dependabot maintenance.
• SECURITY.md or CODEOWNERS protects .github/workflows/, .github/actions/, contrib/security.sh, contrib/codeql/, justfile, and build.zig.

Demo Moment

• Command or flow: on a PR, trigger just security-check-all locally. All 14 security lanes report pass/fail deterministically.
• Expected result: every lane produces a numeric or text result — not "tool not found" or "skipped" — with clear pass/fail semantics. On a release build, just security-release-check produces an SBOM, runs Grype, and validates binary hardening.

Scope

In Scope

• P0: Fix existing security checks to execute real verification (CodeQL, seccomp, CBMC, fail-closed behavior).
• P0: Protect security workflow files with CODEOWNERS and repository rules.
• P0: Pin all third-party GitHub Actions to immutable commit SHAs.
• P0: Verify checksums/signatures for downloaded CI tools.
• P1: Add clang-tidy + Clang Static Analyzer lane.
• P1: Add OSV-Scanner lane.
• P1: Add zizmor lane.
• P1: Add TSan CI lane.
• P1: Add C/C++ fuzzing targets (libFuzzer + ASan/UBSan).
• P1: Add Zig built-in fuzzer lane.
• P2: Add seccomp/Landlock/capability negative tests.
• P2: Add Tickoni-specific policy invariant property tests.
• P2: Add replay determinism security testing.
• P2: Expand CBMC proofs over critical policy/bounds code.
• P3: Generate SBOMs with Syft for release artifacts.
• P3: Scan release SBOMs with Grype.
• P3: Add release binary hardening verification.
• P3: Add OpenSSF Scorecard.
• P4: Add CLR as a non-blocking nightly Zig analysis lane.
• P5: Add story evidence manifest tooling to verify roadmap evidence completeness at build time.
• P5: Add story evidence index generator to scan all story docs and produce a machine-verifiable evidence manifest.
• P5: Add CI lane that fails when any story's declared evidence is missing or mismatched.
• P5: Migrate existing story evidence artifacts from scattered markdown paths into a unified evidence layout under doc/execution/audits/stories/.

Out Of Scope

• Commercial SAST products (Snyk, Coverity, PVS-Studio, SonarQube) — these are optional second-layer products, addressed after the distinct coverage areas above are enforced.
• Semgrep custom rules — useful but lower priority.
• OSS-Fuzz integration — optional beyond CI integration.
• CLR promotion to a blocking gate — remains experimental until Zig 0.16+ compatible and stable.
• Gitleaks PR-range scanning enhancement — improvement to existing check, not a new lane.
• MSan lane — explicitly optional per the security plan.

Conditional Boundary Checklist

Boundary	Status	Notes / linked story
Financial capability and policy	Applies	Property tests enforce policy invariants; stories T13–T14 in P2
Audit records and evidence	Applies	Append-only audit test; CBMC proofs over audit code
Replay and divergence behavior	Applies	Replay determinism testing (P2); replay-specific fuzz targets
Runtime topology, tile ownership, or links	N/A	security tooling does not change topology
Model gateway governance (tkmodl)	N/A	model access rules unchanged; fuzzing covers model response decoding
Tool broker or adapter dispatch (tktool / tkadpt)	N/A	adapter access rules unchanged; fuzzing covers adapter response decoding
Approved execution (tkexec)	N/A	not touched
CaseOps API/UI (tkapi)	N/A	not touched
Storage role: Memory, Analytics, Ledger	N/A	not touched
Metrics, diagnostics, and operations	Applies	S4 (property tests) and S6 (release hardening) change operational security surface
Security and fail-closed behavior	Applies	All stories tighten or add security gates

Story Breakdown

• V3.35.S1: P0 — Fix existing security guarantees: CodeQL, seccomp, CBMC, CODEOWNERS, pin Actions, verify checksums - story
• V3.35.S2: P1 — Add static analysis and runtime safety lanes: clang-tidy, OSV-Scanner, zizmor, TSan - story
• V3.35.S3: P1 — Add fuzzing infrastructure: libFuzzer targets for C/C++ trust boundaries, Zig built-in fuzzer lane - story
• V3.35.S4: P2 — Validate the actual architecture: seccomp/Landlock negative tests, Tickoni property invariant tests, replay determinism testing, expanded CBMC proofs - story
• V3.35.S5: P3 — Secure releases: SBOM generation with Syft, artifact CVE scan with Grype, binary hardening verification, OpenSSF Scorecard - story
• V3.35.S6: P4 — Experimental depth: CLR non-blocking nightly Zig analysis lane, evidence and documentation closure - story
• V3.35.S7: P5 — Story evidence manifest framework: general-purpose build-time verification of roadmap evidence completeness across all epics (V1.x–V3.x), replacing the V2.22.S7 stub and providing reusable infrastructure for all future stories

Epic Acceptance

• All required story issues are done or explicitly deferred with rationale.
• The demo moment succeeds using deterministic local inputs on a clean checkout.
• All 14 CI security lanes produce deterministic pass/fail output.
• CodeQL, CBMC, seccomp, and Gitleaks execute real checks (not no-op wrappers).
• Security workflow files protected with CODEOWNERS and repository rules.
• All third-party GitHub Actions pinned to SHA.
• Relevant documentation artifacts are updated.
• Non-goals and deferred work are visible in the roadmap.
• No Tickoni runtime, policy, audit, replay, adapter, API, or storage behavior changed inadvertently.

Release / Evidence Gate

• What can the user or operator do now that they could not before this epic?
  Run a single just security-check-all command that exercises 14 distinct security layers — source analysis, dependency scanning, CI workflow analysis, runtime safety, fuzzing, formal verification, isolation enforcement, property invariants, SBOM generation, and binary hardening — all with deterministic pass/fail output. The operator doesn't have to trust that security tooling exists in the repo; they run it and see every layer pass or fail in real time.
• What changed from the previous roadmap increment?
  Security tooling moved from aspirational plan to enforced CI gates across 14 layers. The transformation isn't "we added scanners" — it's "every security claim is now backed by a deterministic gate that runs on every commit."
• What is this epic's wow-effect: the visible moment in this epic's demo or workflow that makes Tickoni feel unlike a generic agent harness?
  One command. Fourteen layers. Every layer produces a real result — not a skip or tool-not-found message. The operator sees the full security posture at a glance. In a domain where security is usually a slide deck, Tickoni is a command. That's the difference between a promise and a proof.
• How does this epic progress Tickoni's unique value proposition from doc/strategy/positioning.md: speed, isolation/control, spend governance, policy-gated action, and forensic replay?
  Isolation and forensic replay: seccomp negative tests prove forbidden operations actually fail. Property tests encode financial invariants as code. Replay determinism tests prove consistent security outcomes. CBMC proofs verify bounds and invariants in critical code. Security is no longer a claim — it's a measurable chain. This is what happens when security stops being aspirational and becomes verifiable.
• Which demo command or CaseOps flow closes the epic?
  just security-check-all (all lanes pass locally), then just security-release-check (SBOM, Grype, binary hardening).
• Which account, beneficiary, IBAN, wallet, rail, currency, market, venue, asset class, instrument, notional, amount, exposure, and frequency checks are enforced, if any?
  N/A — this epic adds the tooling that enforces these checks in the runtime, not the checks themselves.
• What happens when the requested action exceeds policy, scope, or evidence?
  The property test lanes detect and report deviations; CI gates block merge until fixed.
• Is execution paper-only, draft-only, sandbox, live, or disabled?
  Build/test only; no live side effects. Security checks are CI-only and local-dev-only.
• Which fixtures, samples, audit records, replay capsules, screenshots, or API examples prove the behavior?
  CI lane outputs, local just security-check-all output, SBOM files, Grype scan results, binary hardening check output.
• Can replay run without external side effects when replay applies?
  Yes — fuzzing and replay tests substitute captured model/adapter outputs and never call external APIs.
• What intentional blocked-flow or divergence example proves fail-closed behavior?
  seccomp negative tests (non-allowlisted syscall -> SIGSYS), property tests (unknown capability -> deny), replay determinism tests (tampered input -> divergence detected).

Dependencies And Decisions

• V2.10.S6 (CI cutover) must ship first — fully-qualified just recipe names are the routing surface for all security lanes.
• V2.10.S1 (contrib/platform.sh) must ship first — security lanes need consistent OS/arch detection.
• S1 (P0) must ship before S2–S6 because it fixes the foundation that other stories build on.
• S3 (fuzzing) and S2 (static analysis) are independent — can ship in any order.
• S4 (architecture validation) depends on S1 (CBMC fixes) and S2 (TSan) because it expands existing tools and adds new tests on top.
• S5 (release hardening) is independent of S2–S4 but should follow S1 so the release surface is clean.
• S6 (experimental) is independent and can ship last — CLR is non-blocking by design.