Skip to content

v0.15.0 — Adversarial Depth & Formal Structure

Choose a tag to compare

View all tags
@EslaM-X EslaM-X released this 24 Aug 03:28
· 17 commits to main since this release
v0.15.0
a99fae6
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

PiProof v0.15.0 — Adversarial Depth & Formal Structure

Second external-review hardening release: machinery that finds its own bugs, and documents that make claims checkable. It paid for itself immediately — the fuzzing suite found a real canonicalization bug before any consumer did.

Found & fixed: Canonical Profile v1.1

Raw-key sort + NFC serialization made canonicalization deterministic but not idempotent: canon(parse(c)) !== c for some already-canonical documents, silently breaking isCanonical() on output the protocol itself produced. v1.1 sorts NFC forms so the emitted text IS the sort key — fixed-point by construction. No previously signed payload changes meaning (the collision rule excludes unstable pairs). Interop vector canon-012 pins the amended order; all 15 vectors regenerated byte-exact in Node + Python.

Added

Seeded fuzzing suite (scripts/fuzz.mjs, npm run fuzz) — six campaigns:

  • canonicalization properties (determinism, idempotence, reject-only-CanonicalError) with Node↔Python cross-examination of every anomaly
  • schema fail-closed under random mutation of valid events, __proto__ injection included
  • Unicode NFC equivalence / collision rejection
  • byte-level Node↔Python differential parsing via a persistent stdlib driver (scripts/fuzz-diff-driver.py)
  • K real OS processes racing one nonce → exactly one winner, every round
  • V8 runtime-parser anomalies are classified separately from protocol violations (FUZZ_STRICT=1 makes them fatal; default CI stays deterministic across Node builds)

Layer governance (scripts/check-layers.mjs, normative docs/LAYERS.md) — modules classified L0 primitives → L4 presentation; one mechanical rule (depLayer ≤ myLayer); unclassified files are violations. Enforced in CI. Current state: 23 modules, 64 edges, 0 violations.

Engineering formal model (docs/FORMAL_MODEL.md) — the G1–G9 verification pipeline as an ordered fail-closed state machine; twelve security invariants (INV-01…INV-12) each with enforced-by / verified-by traceability; crash-failure semantics of the claim path; a normative implementer MUST list. A paper model, honestly labeled as one.

Liveness-aware nonce-lock ownership (FileNonceStore) — lockfiles record {pid, host, acquiredAt}; a lock held by a live same-host process is never stolen regardless of age; provably dead owners may be taken after the staleness window; foreign-host/legacy locks keep time-based fallback. Closes the stale-lock-timeout double-entry race. Pinned by 6 new tests including K-process races.

V8 JSON.parse divergence disclosed (SECURITY.md) — under allocation churn Node can mis-parse byte-identical JSON (phantom-key shape differences vs Python's json.loads). Documented as a runtime defect with full impact analysis: PiProof's schema-pinned key sets make it unreachable in every protocol path.

Verification

132/132 tests · layer check 23 modules / 64 edges / 0 violations · 20/20 attacks rejected · 15/15 canonical vectors byte-exact ×2 languages · FUZZ OK (quick + full)

Status

v1.0 remains gated on external security review (issue #2). New deliberately-open evidence rows in MATURITY.md: #13 independent third-party implementation, #14 mechanized verification.

Assets 2
Loading