Security

This page describes MIND's memory checks, tested deterministic workloads, and evidence verification. Deployment assurance also depends on the selected compiler path, runtime, and application.

Memory Safety

MIND uses scope-bounded regions and generation-checked references. RFC 0010 tracks the implemented checks and remaining phases; this is not a claim that every native path implements Rust's ownership and borrowing guarantees.

  • Region escape checks — reject references that escape a supported region boundary.
  • Generation-checked references — check reference validity at supported dereference operations.
  • Explicit unsafe boundaries — raw pointers and C FFI require the checks and caller obligations of the selected ABI.
  • Implementation coverage — see RFC 0010; concurrency safety and arbitrary native-program coverage require their own acceptance checks.

Deterministic Execution

The strict arithmetic profile preserves the defined operation order. Cross-substrate CI checks the committed workloads on x86_64 AVX2 and ARM64 NEON:

  • Integer and Q16.16 fixed-point — committed fixture outputs match their reference hashes on both CPU substrates.
  • Strict floating point — the scalar f64 chain, length-4093 f32 dot product, and 64×64 f32 matrix-vector fixture have exact matching output hashes. The f64 reference was verified on ARM on 2026-07-05; the two f32 references on 2026-07-14.
  • Operation order — the admitted strict kernels preserve their specified accumulation order and separate multiply/add operations.
  • Replay inputs — pin inputs, seeds, and external observations when checking deterministic replay.
  • Reproducible builds — compare same-target artifacts under fixed source, toolchain, flags, dependencies, and build inputs. Cross-ISA output identity compares the computation's results, not native instruction bytes.

Those three floating-point fixtures do not establish identity for every input, arbitrary vector reduction, transcendental function, or GPU workload. General floating-point and GPU coverage remains outside the shipped cross-substrate claim. See Determinism for the full tier breakdown.

Audit Trail Support

For regulated industries, MIND provides features to support audit and compliance:

  • Full execution traces available in debug mode
  • Immutable IR representations for model versioning
  • Cryptographic hashing of compiled artifacts
  • Integration points for external logging systems

Compile-time Evidence Chains (RFC 0016)

mindc emits an evidence-chain epilogue on compiled IR, including a tamper-evident trace_hash. Opt-in signing requires both ML-DSA-87 and SLH-DSA-SHAKE-256s; both build features are off by default.mindc verify --signer-pubkeychecks an operator-supplied trusted-key allowlist and rejects an unknown signer. A signature authenticates the signed claim; independent reproduction or a supported proof is still needed to establish the computation's correctness. Published release keys and signed-reproduction CI remain operational work. The evidence fields include:

  • evidence_chain.determinism — class (e.g. byte-identical-q16)
  • evidence_chain.substrate — target (x86_avx2, arm64_neon, cuda_sm89, …)
  • evidence_chain.toolchain — compiler + flags identity
  • evidence_chain.trace_hashSHA-256 of the canonical mic@3 binary IR (RFC 0016 GAP-1, re-anchored 2026-05-31)
  • evidence_chain.parent — optional pointer to the parent compilation

The chain rides on a MAP epilogue (RFC 0014) attached to either canonical IR serialisation —mic@1 text or mic@3 binary (RFC 0021) — and survives the load → execute → re-emit cycle. See ir-stability.md for the normative carrier contract.

Cryptographic Primitives (Pure MIND)

The standard library includes a crypto / TLS / HTTP primitive stack written entirely in MIND and verified against RFC and NIST known-answer tests:

  • Symmetric & hashing — AES-128-GCM, SHA-256, HKDF, Keccak / SHA-3 + SHAKE (FIPS 202)
  • Public-key — X25519, RSA-PSS-SHA256 verify, ECDSA-P256 verify, ML-KEM-768 (FIPS 203 post-quantum KEM)
  • Certificates — X.509 parsing and signature verification
  • TLS 1.3 — key schedule, record layer, Finished MAC, handshake crypto (RFC 8448 replay-verified)
  • HTTP/2 — HPACK header compression (RFC 7541) and binary framing (RFC 9113)

Honest scope: this is a verified primitive library, not a working TLS client or server yet — there is no socket-driven handshake state machine or certificate-chain path validation, and HPACK is decode-only. The primitives are correctness-first, not speed-optimized.

Threat Model

The MIND security model assumes:

  • Source code and compiler are trusted
  • Runtime environment provides standard OS protections
  • Input data may be adversarial (tensor bounds are checked)
  • Side-channel attacks are out of scope for the base runtime

Sandboxing (Planned)

Future versions will support optional sandboxing for untrusted model execution:

// Planned syntax
@sandbox(memory_limit: 1GB, time_limit: 10s)
fn untrusted_inference(input: Tensor<f32, N, M>) -> Tensor<f32, N, K> {
    // ...
}

Learn More

See the full security specification at mind-spec/security.md.