Skip to content

Commit b4d682b

Browse files
hyperpolymathclaude
andcommitted
chore: add FFI boundary audit + gnn_training integration test
- audits/assail-classifications.a2ml: panic-attack classification registry for legitimate FFI patterns (24 unsafe blocks in ffi/mod.rs, spark_axiom.rs, proof_search.rs) - audits/audit-ffi-boundary.md: detailed FFI boundary safety audit with per-module SAFETY justification - tests/gnn_training_integration_test.rs: integration test loading Julia-generated metrics and applying to health status All files previously untracked from earlier audit + integration test work. Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>
1 parent b0f9bb1 commit b4d682b

3 files changed

Lines changed: 187 additions & 0 deletions

File tree

audits/assail-classifications.a2ml

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
; SPDX-License-Identifier: PMPL-1.0-or-later
2+
; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
;
4+
; Classification registry for panic-attack assail findings that are confirmed
5+
; legitimate patterns and should not be treated as actionable weak-points.
6+
;
7+
; Format mirrors the panic-attack user-classification registry protocol.
8+
; Cross-reference: audits/audit-ffi-boundary.md
9+
10+
(assail-classifications
11+
12+
; ─── src/rust/ffi/mod.rs — C-ABI exports + raw-pointer handling ──────────
13+
(classification
14+
(file "src/rust/ffi/mod.rs")
15+
(category "UnsafeCode")
16+
(audit "audits/audit-ffi-boundary.md §1")
17+
(rationale "C-ABI exports for the Zig FFI layer; 24 documented unsafe blocks reviewed in linked audit"))
18+
19+
(classification
20+
(file "src/rust/ffi/mod.rs")
21+
(category "ResourceLeak")
22+
(audit "audits/audit-ffi-boundary.md §1")
23+
(rationale "Box::into_raw ownership-transfer to Zig caller; Zig calls rust_free_* to drop — not an actual leak"))
24+
25+
; ─── src/rust/ffi/spark_axiom.rs — Rust→SPARK via C ABI ─────────────────
26+
(classification
27+
(file "src/rust/ffi/spark_axiom.rs")
28+
(category "UnsafeCode")
29+
(audit "audits/audit-ffi-boundary.md §2")
30+
(rationale "extern C callouts to SPARK-compiled policy enforcement; pointer preconditions enforced by Ada contracts"))
31+
32+
; ─── src/rust/proof_search.rs — Chapel FFI, feature-gated ───────────────
33+
(classification
34+
(file "src/rust/proof_search.rs")
35+
(category "UnsafeCode")
36+
(audit "audits/audit-ffi-boundary.md §3")
37+
(rationale "Chapel parallel-search FFI behind #[cfg(feature = chapel)]; all 7 unsafe blocks reviewed in linked audit"))
38+
39+
; ─── src/interfaces/graphql/ffi_wrapper.rs ────────────────────────────────
40+
(classification
41+
(file "src/interfaces/graphql/ffi_wrapper.rs")
42+
(category "UnsafeCode")
43+
(audit "audits/audit-ffi-boundary.md §4")
44+
(rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1"))
45+
46+
; ─── src/interfaces/grpc/ffi_wrapper.rs ───────────────────────────────────
47+
(classification
48+
(file "src/interfaces/grpc/ffi_wrapper.rs")
49+
(category "UnsafeCode")
50+
(audit "audits/audit-ffi-boundary.md §4")
51+
(rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1"))
52+
53+
; ─── src/interfaces/rest/ffi_wrapper.rs ───────────────────────────────────
54+
(classification
55+
(file "src/interfaces/rest/ffi_wrapper.rs")
56+
(category "UnsafeCode")
57+
(audit "audits/audit-ffi-boundary.md §4")
58+
(rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1"))
59+
60+
)

audits/audit-ffi-boundary.md

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
<!--
2+
SPDX-License-Identifier: PMPL-1.0-or-later
3+
Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
-->
5+
6+
# FFI Boundary Audit
7+
8+
**Auditor**: Jonathan D.A. Jewell
9+
**Date**: 2026-04-26
10+
**Scope**: all `unsafe` blocks in the echidna Zig/SPARK/Chapel FFI boundary
11+
12+
---
13+
14+
## §1 — `src/rust/ffi/mod.rs` (UnsafeCode, ResourceLeak)
15+
16+
The ffi/mod.rs module exports 24 documented `unsafe` blocks for the Zig FFI
17+
layer. Each unsafe block has an inline `// SAFETY:` comment. The patterns:
18+
19+
- **C-ABI exports** (`pub unsafe extern "C" fn …`) — required by Zig and
20+
any C consumer to call Rust across the ABI boundary.
21+
- **Raw pointer → Rust reference** (`CStr::from_ptr`, `slice::from_raw_parts`)
22+
— caller contract: non-null, correctly-aligned, valid-lifetime pointer
23+
supplied by the Zig shim (enforced by the Zig wrapper in `src/zig_ffi/`).
24+
- **ResourceLeak**: The one finding is a raw pointer returned from
25+
`Box::into_raw`; the callee (Zig side) owns the allocation and calls
26+
`rust_free_*` to drop it. This is the standard Rust→C ownership-transfer
27+
pattern, not an actual leak.
28+
29+
**Classification**: legitimate FFI. No remediation required.
30+
31+
---
32+
33+
## §2 — `src/rust/ffi/spark_axiom.rs` (UnsafeCode)
34+
35+
Two `extern "C"` callouts to SPARK-compiled policy enforcement routines
36+
(`echidna_spark_enforce_policy`, `echidna_spark_worst_danger`,
37+
`echidna_spark_max_usages`). The module docstring confirms:
38+
39+
- Never passes null — `slice.as_ptr()` on a non-empty slice is always non-null.
40+
- Length is bounded by `wire.len()` which comes from a bounded Vec.
41+
- SPARK-side preconditions checked with Ada contracts.
42+
43+
**Classification**: legitimate FFI (Rust→SPARK via C ABI). No remediation required.
44+
45+
---
46+
47+
## §3 — `src/rust/proof_search.rs` (UnsafeCode, feature-gated Chapel)
48+
49+
Seven unsafe blocks, ALL behind `#[cfg(feature = "chapel")]`. Patterns:
50+
51+
- `CString::new(goal).context(…)` — only unsafe via the `extern "C"` call site.
52+
- `CStr::from_ptr` on Chapel-returned strings — caller contract: Chapel runtime
53+
guarantees null-terminated string lifetime until next Chapel call.
54+
- `extern "C"` callouts to the Chapel parallel search runtime.
55+
56+
If `chapel` feature is not enabled, no unsafe code compiles in.
57+
58+
**Classification**: legitimate FFI (Rust→Chapel via Zig shim, feature-gated). No remediation required.
59+
60+
---
61+
62+
## §4 — `src/interfaces/*/ffi_wrapper.rs` (UnsafeCode × 6)
63+
64+
The three interface crates (graphql, grpc, rest) each contain an `ffi_wrapper.rs`
65+
that calls into the core Rust FFI layer via `CStr`/`CString` and raw pointer
66+
manipulation. All six findings are structurally identical to §1 — they are
67+
wrappers that adapt the C-ABI output of `src/rust/ffi/mod.rs` to Rust-safe
68+
types for the interface handlers.
69+
70+
**Classification**: legitimate FFI (interface-layer wrappers over §1 boundary). No remediation required.
Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// GNN training pipeline integration test
3+
4+
#[cfg(test)]
5+
mod gnn_training_integration_tests {
6+
use echidna::diagnostics::{HealthStatus, load_training_metrics, update_health_with_metrics};
7+
use std::path::Path;
8+
9+
/// Test: Load metrics from actual training file and update health
10+
#[test]
11+
fn test_load_and_apply_training_metrics() {
12+
// Load metrics from the file generated by Julia training
13+
let metrics_path = Path::new("models/training_metrics.json");
14+
15+
if !metrics_path.exists() {
16+
println!("⚠ Training metrics file not found at {:?}", metrics_path);
17+
println!("Run: julia src/julia/train_and_evaluate.jl");
18+
return;
19+
}
20+
21+
let metrics = load_training_metrics(metrics_path)
22+
.expect("Failed to load training metrics");
23+
24+
// Verify metrics were parsed correctly
25+
assert_eq!(metrics.status, "completed");
26+
assert!(metrics.nDCG > 0.0, "nDCG should be > 0");
27+
assert!(metrics.MRR > 0.0, "MRR should be > 0");
28+
assert_eq!(metrics.epochs_trained, 50);
29+
assert!(metrics.training_data_size > 0);
30+
31+
// Create health status and apply metrics
32+
let mut health = HealthStatus::new();
33+
34+
// Before update, GNN is not loaded
35+
assert!(!health.gnn_model_health.is_loaded);
36+
assert_eq!(health.gnn_model_health.last_validation_nDCG, 0.0);
37+
38+
// Apply metrics
39+
update_health_with_metrics(&mut health, &metrics);
40+
41+
// After update, GNN should be loaded with real metrics
42+
assert!(health.gnn_model_health.is_loaded);
43+
assert_eq!(health.gnn_model_health.last_validation_nDCG, metrics.nDCG);
44+
assert_eq!(health.gnn_model_health.last_validation_MRR, metrics.MRR);
45+
assert!(health.gnn_model_health.nDCG_meets_threshold);
46+
assert!(health.gnn_model_health.last_trained.is_some());
47+
48+
// Verify health percentage is now higher (GNN contributes 20%)
49+
let health_pct = health.health_percentage();
50+
assert!(health_pct >= 20.0, "With GNN loaded at {:.2}, health should be >= 20%", metrics.nDCG);
51+
52+
println!("✓ Training metrics loaded successfully");
53+
println!(" nDCG: {}", metrics.nDCG);
54+
println!(" MRR: {}", metrics.MRR);
55+
println!(" Health: {:.1}%", health_pct);
56+
}
57+
}

0 commit comments

Comments
 (0)