ci: Zig FFI gate (pinned 0.13.0) + obli-pkg verification hardening - #109
Conversation
The FFI (ffi/zig/, 5 files) had zero CI coverage — it rotted silently until PR #56 fixed 6 compile errors found by hand. This adds a zig-ffi job compile-checking every FFI source. Zig comes from the official tarball with a hardcoded sha256 (verified against ziglang.org/download/index.json) rather than a third-party setup action, keeping the workflow fully SHA-pinned. 0.13.0 is the verified toolchain: 0.14+ renamed callconv(.C) and rejects these sources. Full-link gate (zig build against system liboqs/libsodium) deferred until a liboqs container image is wired in — see #62. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The payload derivation shipped earlier is real and fail-closed, but four defects around it could still verify garbage or degrade trust: - readKeyOrDefault zero-padded short/truncated key files to the algorithm's key length. Now readKey: the file must be exactly the expected length (no shorter, no trailing bytes) or verification refuses (fail-closed). - extractSignatureOrDefault base64-decoded into fixed undefined buffers; a short decode left an uninitialised tail that was passed at full-buffer length to OQS_SIG_verify — non-deterministic verification input. Now extractSignature: the decoded length must equal the algorithm's signature length exactly. - Parser asymmetry: extraction found "SIGNATURE:" anywhere via indexOf while deriveSignedPayload strips only line-starting envelopes — a mid-line marker could be consumed as a signature yet survive in the signed payload. Both sides now share line-start semantics (indexOfLineStart). - HOME fell back to "/tmp" (a world-writable keyring root) and the subsequent allocator.free(home) was an invalid free of the static literal on that path. Missing HOME now refuses to verify. Verified: zig ast-check + a full semantic compile (zig build-obj -lc) under the pinned Zig 0.13.0 both pass. The signer + end-to-end sign/verify vectors remain follow-on work (#60, rescoped). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedAdds a pinned Zig 0.13.0 AST-check CI gate for the FFI layer and hardens obli-pkg signature verification by closing four fail-open gaps. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 6 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
|
|
…#111) Closes #68. Advances #63 (owner action below) and #79 (skeleton only; stays open). ## What - **CONTRIBUTING**: the `.md` was un-instantiated template rot — opened mid-code-fence, raw `{{MAIN_BRANCH}}` token, a repository tree with five nonexistent directories, ended mid-block. Real content rewritten into `CONTRIBUTING.adoc` (actual tree, `docs/TOOLCHAIN.adoc` + `.tool-versions` toolchain, proof-gate discipline); `.md` deleted; README link updated. - **GOVERNANCE / MAINTAINERS**: inverse situation — the `.adoc` twins are the rich repo-specific docs; the generic stubs (`GOVERNANCE.md`, bare `MAINTAINERS`) deleted. - **#79 skeleton**: `docs/learning-paths/README.adoc` seeds the end-user/developer/maintainer outline. ## Owner action — `.claude/CLAUDE.md` replacement (#63) The file is agent-edit-blocked (self-modification guardrail). Please replace its contents with the text below, which fixes: the six `.scm` references (now `.machine_readable/6a2/*.a2ml`), the phantom `guix.scm`/`deno.json` claims, and the foreign language-policy table (AffineScript/Deno/Tauri — a different project's stack). ```markdown ## Machine-Readable Artefacts Structured project metadata lives in `.machine_readable/6a2/` (A2ML format): - `STATE.a2ml` - Current project state and progress - `META.a2ml` - Architecture decisions and development practices - `ECOSYSTEM.a2ml` - Position in the ecosystem and related projects - `AGENTIC.a2ml` - AI agent interaction patterns - `NEUROSYM.a2ml` - Neurosymbolic integration config - `PLAYBOOK.a2ml` - Operational runbook - `0-AI-MANIFEST.a2ml` - Manifest Contractiles live in `.machine_readable/contractiles/`. --- # CLAUDE.md - AI Assistant Instructions ## This Repo's Stack (all pinned in .tool-versions) | Language/Tool | Use Case | |---------------|----------| | **OCaml 5.1.1 + dune** | The Oblíbený compiler (lib/, bin/, test/) | | **Idris2 0.7.0** | ABI proof layer (src/abi/, oblibeny-abi.ipkg) | | **Zig 0.13** | Crypto FFI + obli-pkg (ffi/zig/); 0.14+ breaks callconv(.C) | | **just** | Task runner — all operations go through the justfile | | **Bash/POSIX shell** | Scripts, kept minimal | | **Guile Scheme** | Root spec files (ANCHOR*.scm, SPEC*.scm, AUTHORITY*.scm) | Do not introduce Node/npm/TypeScript/Python/Go — this repo has no JS/Python surface and the estate bans them as replacements-available. ## The Proof Gate (non-negotiable) - CI (`ci.yml`) builds the OCaml language, runs the conformance suite, type-checks (= proves) the Idris2 ABI layer, compile-checks the Zig FFI, and rejects soundness escape hatches (`believe_me`, `postulate`, `assert_total`, `partial`, `idris_crash`, holes) in `src/abi/Crypto.idr` and `src/abi/Packages`. - Local mirror: `just ci` + `just proofs`. Never weaken a proof to make a change pass. ## Packaging - Containers: `Containerfile.bootstrap` / `Containerfile.minimal` / `Containerfile.liboqs` (podman-first). - `flake.nix` is legacy (estate ruling: Guix-only; a `guix.scm` migration is an open follow-up). ## Security Requirements - No MD5/SHA1 for security (use SHA256+) - HTTPS only (no HTTP URLs) - No hardcoded secrets - SHA-pinned dependencies (actions included) - SPDX license headers on all files ``` Suggested follow-up issue rather than folding in here: *"packaging: replace flake.nix with guix.scm"* (Nix-retired estate ruling). **Note**: `CONTRIBUTING.adoc` links `docs/TOOLCHAIN.adoc`, which lands in PR #108 — merge that first (they're ordered #108 → #109 → #110 → this). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Closes #62. Advances #60 (rescope comment to follow on the issue).
Commit 1 — Zig FFI CI gate
ci.ymlgains azig-ffijob: official Zig 0.13.0 tarball with hardcoded SHA-256 (d45312e61ebcc48032b77bc4cf7fd6915c11fa16e4aad116b66c9468211230ea, verified against ziglang.org/download/index.json) — no third-party setup action, so the workflow stays fully SHA-pinned — thenzig ast-checkover all FFI sources. Link-strategy decision (#62): a fullzig buildlink gate needs system liboqs/libsodium (build.zighardcodes/usr/localpaths); deferred until a liboqs container image (the keptContainerfile.liboqsfrom the container-consolidation PR) is wired in.Commit 2 — obli-pkg.zig verification hardening
Issue #60's original premise (mock payload stub) is partially outdated — payload derivation is already real and fail-closed. This commit closes the four remaining fail-open gaps:
readKeyOrDefaultsilently zero-filled short key files → nowreadKey, exact-length or refuse.undefinedbuffer tails passed full-length toOQS_SIG_verify→ decoded length must exactly match the algorithm's signature size.SIGNATURE:mid-line while payload derivation only stripped line-starting envelopes → both now shareindexOfLineStart./tmpHOME fallback (world-writable keyring root) + invalidfreeof the static literal → missing HOME refuses to verify.Deferred (issue #60 stays open, rescoped): the signer itself and end-to-end sign→verify test vectors — nothing in the repo produces
SIGNATURE:blocks yet, so the verify path can currently only fail closed.Verified
zig ast-checkon all 4 FFI sources: passzig build-obj -lc): exit 0🤖 Generated with Claude Code