vcl-ut #25 P5c (step 5): recompute-PCC wasm32 entry (fail-closed; isolated unsafe boundary)#32
Merged
Conversation
…lated unsafe boundary) The recompute-PCC tier's executable artefact. Under the locked two-tier design (VERIFICATION-STANCE.adoc): the consumer is shipped this wasm module + the wire bytes of a (Statement, OctadSchema) + the producer's claimed level, RE-RUNS the certified decision here, and compares. Guarantee = corpus proof (checkLevelNSound, once) + conformance pin (P5c-4) — NOT the wasm's type system. New crate src/interface/recompute-wasm (standalone workspace; only dep = the in-repo forbid-unsafe vcltotal-parse via internal path-dep): - src/lib.rs — `vcl_recompute(stmt_ptr,len,schema_ptr,len) -> i64` (+ `vcl_alloc`/`vcl_dealloc` for the host to stage bytes). Fail-closed: any WireError, null ptr, or unmet level → -1; the only non-negative result is a genuinely recomputed certified level. - The ONLY unsafe in the whole recompute path is one audited, documented host/guest memory-ABI block (slice::from_raw_parts) — which IS the declared trust boundary. All decode/decision logic stays in the #![forbid(unsafe_code)] vcltotal-parse crate. User decision (recorded): separate crate + isolated documented unsafe, not wasm-bindgen, not exported-buffer. - Builds to real wasm: `cargo build --release --target wasm32-unknown-unknown` → 50KB vcltotal_recompute_wasm.wasm. `panic = "abort"` (no unwinding runtime; a by-construction unreachable panic traps, never UB). - Host tests green (garbage/null fail-closed; well-formed → 0); clippy -D warnings clean; fmt clean. Mechanism findings (disclosed, not faked — estate doctrine): - plain wasm32-unknown-unknown is SUFFICIENT for the recompute argument: nothing structured crosses the boundary needing type-preservation (opaque bytes in, i64 out, decoder+decider run INSIDE). AffineScript dependent/affine typing was load-bearing only for the REJECTED proof-term-transport tier. - affinescriptiser is NOT used here, for two independent reasons, documented in AFFINESCRIPTISER-NA.adoc: (1) it structurally requires >=1 [[resources]] and this entry is a pure resource-free verdict function — faking a resource to satisfy the tool would be the exact cargo-culting the verification-honesty doctrine forbids; (2) its own wasm backend is Phase-2-pending (verified). The wasm verdict is identical to the conformance-pinned native verdict by construction (deterministic cargo build of the same pinned, pure, total source). Adds README.adoc + AFFINESCRIPTISER-NA.adoc; .gitignore excludes /target (no build artefact committed). The fail-closed C/Zig C-ABI shim (Phase 3d) stays the attestation FALLBACK tier; the two-tier wiring + stance flip + ADR are P5c-6. Refs #25. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,198 @@ | |||
| // SPDX-License-Identifier: PMPL-1.0-or-later | |||
| @@ -0,0 +1,198 @@ | |||
| // SPDX-License-Identifier: PMPL-1.0-or-later | |||
| @@ -0,0 +1,198 @@ | |||
| // SPDX-License-Identifier: PMPL-1.0-or-later | |||
🔍 Hypatia Security ScanFindings: 25 issues detected
View findings[
{
"reason": "Issue in quality.yml",
"type": "missing_workflow",
"file": "quality.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in security-policy.yml",
"type": "missing_workflow",
"file": "security-policy.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Action actions/upload-artifact@v4 needs attention",
"type": "unpinned_action",
"file": "release.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action actions/download-artifact@v4 needs attention",
"type": "unpinned_action",
"file": "release.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "codeql.yml lists `language: javascript-typescript` but the repo has no source files in any CodeQL-scannable language. The analyze job will exit 'no source files' on every run. Switch the matrix to `actions` (which scans workflow files — every repo has those).",
"type": "codeql_language_matrix_mismatch",
"file": "codeql.yml",
"action": "switch_codeql_matrix_to_actions",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "assert_smaller bypasses termination checker (1 occurrences, CWE-704)",
"type": "assert_smaller",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Checker.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "believe_me undermines formal verification (2 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Decide.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "believe_me undermines formal verification (3 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Composition.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
"type": "assert_total",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Composition.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
P5c (step 5) — recompute-PCC
wasm32entry (fail-closed; isolatedunsafeboundary)The recompute-PCC tier's executable artefact. Per the locked
two-tier design (
VERIFICATION-STANCE.adoc): the consumer is shippedthis wasm module + the wire bytes of a
(Statement, OctadSchema)+ theproducer's claimed level, re-runs the certified decision here, and
compares. The guarantee is the corpus proof (
checkLevelNSound, once)New crate
src/interface/recompute-wasmStandalone workspace; only dependency is the in-repo
#![forbid(unsafe_code)]vcltotal-parse(internal path-dep).vcl_recompute(stmt_ptr,len,schema_ptr,len) -> i64(+vcl_alloc/vcl_deallocfor host byte-staging). Fail-closed: anyWireError, null pointer, or unmet level →-1; the onlynon-negative result is a genuinely recomputed certified level.
unsafein the whole recompute path is one audited,documented host/guest memory-ABI block — which is the declared
trust boundary. All decode/decision logic stays in the forbid-unsafe
crate. (Per your call: separate crate + isolated documented unsafe.)
cargo build --release --target wasm32-unknown-unknown→ 50 KBvcltotal_recompute_wasm.wasm.panic = "abort".-D warningsclean; fmt clean..gitignoreexcludes/target.Mechanism findings (disclosed, not faked — estate doctrine)
wasm32-unknown-unknownis sufficient for the recomputeargument: nothing structured crosses the boundary needing
type-preservation (opaque bytes in,
i64out, decoder+decider runinside). AffineScript dependent/affine typing was load-bearing only
for the rejected proof-term-transport tier.
(full rationale in
AFFINESCRIPTISER-NA.adoc): it structurallyrequires ≥1
[[resources]]and this entry is a pure resource-freeverdict function — fabricating a resource to satisfy the tool would
be exactly the cargo-culting the verification-honesty doctrine
forbids; and its own wasm backend is Phase-2-pending (verified). The
wasm verdict is identical to the conformance-pinned native verdict
by construction (deterministic
cargo buildof the same pinned,pure, total source).
Verified locally
cargo test3/3 (fail-closed garbage/null; well-formed→0) ·cargo clippy --all-targets -- -D warningsclean ·cargo fmt --checkclean·
cargo build --release --target wasm32-unknown-unknown→.wasmproduced.
Scope boundary
The fail-closed C/Zig C-ABI shim (Phase 3d) stays the attestation
fallback tier — unchanged here. The two-tier wiring narrative + the
OWED→RESOLVEDstance flip + ADRdocs/decisions/0002-ffi-attestation-trust-boundary.adocare P5c-6(the authoritative-doc change; deliberately a separate, reviewable
unit).
Refs #25.
🤖 Generated with Claude Code