Skip to content

Commit 0140014

Browse files
audit(security): audited assail-classifications for the 3 legitimate FFI/unsafe residuals (P5) (#51)
## Summary Closes **G18** (P5): records Axiom's inherent, reviewed FFI/`unsafe` boundary as **audited‑legitimate residuals** in the panic‑attack user‑classification registry — the honest alternative to blanket suppression or a permanently‑red gate. ## What's classified (only the 3 genuine FFI/unsafe boundaries) | File | Category | Why it's sound | |---|---|---| | `crypto/src/lib.rs` | UnsafeCode | The `extern "C"` cdylib surface. Thin shim over vetted `openssl` + `pqcrypto-dilithium`; `// SAFETY:` on every block; caller‑allocates ABI; no hand‑rolled crypto. | | `src/verification/signing.jl` | UnsafeFFI | Julia `ccall`/`Libdl` into that cdylib. Optional shim; runtime ABI self‑check; per‑call length validation. | | `src/backends/zig_ffi.jl` | UnsafeFFI | Julia `ccall`/`Libdl` into the Zig compute backend. Availability‑checked before any dispatch; memory‑safety logic lives Zig‑side. | - **`audits/audit-ffi-unsafe.adoc`** — the per‑boundary rationale (the cited audit). - **`audits/assail-classifications.a2ml`** — the registry, which lives **separately from the code under scan** so a newly‑added `unsafe` block cannot self‑suppress (the suppression only holds while the audit is kept current). **Nothing else is suppressed.** All ProofDrift / InputBoundary / MutationGap findings are left **visible and un‑suppressed** — they're tracked as ordinary findings, not audited residuals. ## Verification (ground‑truthed, not self‑graded) Re‑ran `panic-attack assail` after adding the registry: - Exactly the **three** classified findings flip to `suppressed=true`; the `# SPDX` header did not break the S‑expression parse. - The other visible findings are unchanged; **0 critical** (the `static-analysis-gate` stays green on merit, now with the FFI boundary honestly audited rather than noisy). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1 --- _Generated by [Claude Code](https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent eae2272 commit 0140014

2 files changed

Lines changed: 91 additions & 0 deletions

File tree

audits/assail-classifications.a2ml

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Audited legitimate residuals for `panic-attack assail`.
3+
# Companion audit (rationale + review): audits/audit-ffi-unsafe.adoc
4+
# Per the user-classification protocol this registry lives separately from the
5+
# code under scan, so a newly-added unsafe block cannot self-suppress — the
6+
# suppression only holds while the cited audit is kept current.
7+
(assail-classifications
8+
(classification
9+
(file "crypto/src/lib.rs")
10+
(category "UnsafeCode")
11+
(audit "audits/audit-ffi-unsafe.adoc §1")
12+
(rationale "C-ABI cdylib: extern-C raw-pointer surface requires unsafe; each block has a // SAFETY comment; thin shim over vetted openssl + pqcrypto-dilithium, no hand-rolled crypto"))
13+
(classification
14+
(file "src/verification/signing.jl")
15+
(category "UnsafeFFI")
16+
(audit "audits/audit-ffi-unsafe.adoc §2")
17+
(rationale "Julia ccall/Libdl into the audited axiom_crypto cdylib; optional shim with a runtime ABI self-check; buffer lengths validated against ABI constants before every ccall"))
18+
(classification
19+
(file "src/backends/zig_ffi.jl")
20+
(category "UnsafeFFI")
21+
(audit "audits/audit-ffi-unsafe.adoc §3")
22+
(rationale "Julia ccall/Libdl into the Zig compute backend; availability checked before dispatch; memory-safety-critical logic lives Zig-side")))

audits/audit-ffi-unsafe.adoc

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
= Audit — Axiom.jl FFI / unsafe boundary
3+
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
:revdate: 2026-07-01
5+
6+
Records why the three FFI / `unsafe` residuals that `panic-attack assail`
7+
reports for Axiom.jl are *legitimate, reviewed* boundaries rather than defects.
8+
This is the companion document cited by `audits/assail-classifications.a2ml`.
9+
Per the panic-attack user-classification protocol the classification registry
10+
lives in a *separate* file from the code under scan, so adding a new `unsafe`
11+
block cannot silently self-suppress — a suppression is only honoured while this
12+
audit is kept current in the same review.
13+
14+
None of these boundaries hand-rolls cryptography or safety logic; each is the
15+
minimal, necessary seam between Julia and a vetted native library.
16+
17+
== §1 — `crypto/src/lib.rs` (category: UnsafeCode)
18+
19+
`axiom_crypto` is a thin C-ABI shim (`cdylib`) exposing hybrid Ed448 +
20+
Dilithium5 certificate signing to Julia. A stable C ABI necessarily uses
21+
`extern "C"` + `#[no_mangle]` functions taking raw pointers, which Rust
22+
requires to be dereferenced inside `unsafe` — the UnsafeCode finding is this
23+
expected surface, not a soundness hole. Sound because:
24+
25+
* *No hand-rolled crypto.* Ed448 → system libcrypto (OpenSSL 3.x) via the vetted
26+
`openssl` crate; Dilithium5 → the vetted `pqcrypto-dilithium` crate (PQClean
27+
reference implementation). The crate implements no primitive of its own.
28+
* *Every `unsafe` block carries a `// SAFETY:` comment* stating the precondition
29+
it relies on (non-null pointer; caller-allocated buffer of the ABI-declared
30+
length).
31+
* *Caller-allocates-buffer + written-length ABI* — no allocate-and-return /
32+
free-fn pairs, so there is no cross-language ownership to leak or double-free.
33+
* *Length-checked entry points* — each function validates slice lengths against
34+
the exported `axiom_crypto_*_len()` constants and returns a negative status
35+
code (never UB) on a bad length or null pointer.
36+
37+
== §2 — `src/verification/signing.jl` (category: UnsafeFFI)
38+
39+
Loads the `axiom_crypto` cdylib via `Libdl.dlopen` and calls it via `ccall` —
40+
Julia's only foreign-call mechanism, inherently flagged UnsafeFFI. Sound
41+
because:
42+
43+
* The shim is *optional*: if the cdylib is unbuilt, `crypto_shim_available()`
44+
returns `false` and every signing entry point throws a clear, documented error
45+
rather than calling through a null handle.
46+
* A runtime ABI self-check (`_validate_crypto_abi!`) confirms the library's
47+
reported key/signature lengths match the Julia-side constants before any
48+
cryptographic `ccall` (this check caught a real length mismatch in
49+
development).
50+
* Every sign/verify call validates buffer lengths against the ABI constants
51+
before the `ccall`, so no out-of-bounds pointer crosses the boundary.
52+
53+
== §3 — `src/backends/zig_ffi.jl` (category: UnsafeFFI)
54+
55+
Loads the Zig compute backend (`libaxiom_zig`) via `Libdl.dlopen` and dispatches
56+
kernels via `ccall`. Sound because:
57+
58+
* `init_zig_backend` checks the library file exists and wraps `dlopen` in
59+
`try`/`catch`, setting an availability flag; the `@zig_call` macro refuses to
60+
dispatch (`error(...)`) unless `zig_available()` is true, so no call is made
61+
through a null handle.
62+
* The memory-safety-critical compute logic lives on the *Zig* side (a
63+
memory-safe systems language); Julia holds only the thin dispatch seam.
64+
65+
== Scope
66+
67+
Covers ONLY the three boundaries above. All other `assail` findings (ProofDrift,
68+
InputBoundary, MutationGap) are deliberately left *visible and un-suppressed* —
69+
tracked as ordinary findings, not audited-legitimate residuals.

0 commit comments

Comments
 (0)