Skip to main content

Security

Verum's type system and verification pipeline eliminate entire classes of vulnerabilities. This guide surveys the tools and the residual risks.

What this guide recommends, and what this build runs

The recommendations below are the right ones to design against. Three of them cannot be executed by this build, and a security guide that does not say so is worse than none — a reader follows it and ships code that stops at the first call.

Checked, both tiers:

Recommended hereState in this build
ML-DSA signatures, ML-KEM-768 exchange❌ verum.pq.* has no implementation — traps on both tiers
X25519 key exchange❌ verum.x25519.scalar_mult likewise; generate_* also needs the missing CSPRNG
HKDF, HMAC, SHA-2⚠️ correct under the interpreter, fault under AOT (A147)
AES-128 / AES-256 block cipher✅ verified against the FIPS-197 vectors at both tiers
ChaCha20, Poly1305, the AEADs⚠️ correct under the interpreter, fault under AOT

So the AEAD advice stands in design and, today, runs only under verum run. Check security/overview before planning against any row here — it carries the per-primitive measurement and is updated as the defects close.

What Verum prevents by construction​

ClassMechanism
Use-after-freeCBGR generation checks
Double-freeCBGR tracks the current generation
Null dereferenceNo null; Maybe<T> forces handling
Buffer overflowBounds-checked indexing; refinement types proving in-range
Integer overflowExplicit checked_* / saturating_* / wrapping_* APIs
Uninitialised-memory readMaybeUninit<T> + escape check
Type confusionNominal types; explicit conversions
Data racesSend / Sync enforce thread-safety at compile time
SQL/HTML/shell injectionTagged literals (sql#, html#, sh#) auto-escape
Deserialisation mismatchTyped @derive(Deserialize) with refinements
Unvalidated user inputRefinement types force validation at boundaries

What still requires discipline​

  • Cryptographic correctness — use the vetted stdlib crypto primitives under core.security: aead for authenticated encryption, ecc for X25519, pq for ML-KEM / ML-DSA, kdf for HKDF. Don't roll your own primitives — picking the wrong mode or truncating tags catastrophically weakens security.
  • Constant-time code — the compiler doesn't guarantee side- channel resistance by default. The stdlib crypto primitives are constant-time by construction, and core.subtle.constant_time_eq is mandatory for any secret-byte comparison. Don't branch on secret bytes in your own code.
  • Supply-chain trust — see the trust model for cog signatures and advisories.
  • Resource exhaustion — DoS via memory, open FDs, task queues. Use bounded channels, semaphores, nursery limits.
  • Business-logic bugs — verification proves what you wrote; if the spec is wrong, the proof doesn't help. Pair verified code with good tests.

Practical checklist​

Inputs​

  • All external inputs parsed via typed Deserialize with refinement types or, for arbitrary shapes, Data + explicit validation.
  • Regex in tagged form (rx#"...") — compile-time-checked.
  • SQL in tagged form (sql#"...") — injection-safe.
  • Shell commands via Command.new(...).arg(...) — never string- concatenate.
  • HTML output via html#"""...""" — escape-by-default.

Authentication / authorisation​

  • Sensitive operations require using [Auth] — no global auth.

  • Use capability-restricted types: Database with [Read] for views that must not write.

  • security.labels supplies runtime classification tags and explicit comparisons. Apply the result of a label comparison in your application policy; wrapping a value in Labeled<T> does not automatically restrict where it can flow.

  • Workload identity (K8s / multi-cluster / multi-cloud) — security.spiffe gives you SPIFFE-ID-based mTLS with automatic rotation.

Secrets​

  • Keep secrets out of logs and public responses. Runtime Labeled<T> tags do not make the logger refuse sensitive data.
  • For types holding key material, implement Drop to zero the buffer before release — see security.util.zeroise (stable wrapper planned; use the verum.mem.zeroise intrinsic until then).
  • Pull secrets from a dedicated store, not env vars: HashiCorp Vault, AWS Secrets Manager, or GCP Secret Manager via security.secrets.
  • Environment variables over on-disk plaintext; container secrets over env vars where a store is not available.

Crypto​

  • Authenticated encryption — use the AEAD layer: AES-128/256-GCM or ChaCha20-Poly1305. Never raw AES / raw ChaCha20 — those lack authentication.
  • Signatures — ML-DSA (post-quantum) for new work; Ed25519 (planned P1) when it lands; ECDSA-P256 (planned P1) for legacy interop.
  • Key exchange — X25519 paired with ML-KEM-768 for PQ-hybrid is the TLS 1.3 / QUIC default.
  • KDFs — HKDF-SHA-256 / -SHA-384 / -SHA-512 for key derivation from high-entropy IKM. Argon2id for password hashing (different module, planned).
  • MACs — HMAC-SHA-256 is the right default for cookie signing / token MACs. Always verify tags with constant_time_eq, never ==.
  • Never unsafe-cast between [Byte; N] and other types without zeroisation first.

Network​

  • TLS 1.3 only. Verum's pure-Verum TLS stack at core.net.tls13 is 1.3-only by design; there is no tls12_fallback flag. Clients detect RFC 8446 §4.1.3 downgrade sentinels ("DOWNGRD\x01" / "DOWNGRD\x00") in ServerHello.random and abort with ProtocolVersion.
  • Load the system trust store explicitly: ClientOptions.with_system_trust() (H3) or QuicClientOptions.with_system_trust() — both wrap TrustStore.system() with a deterministic fallback to an empty store on macOS / Windows backends that fail.
  • Certificate pinning: construct a TrustStore from your pinned DER chains via TrustStore.from_der(&[...]) and pass it as opts.trust.
  • Hostname verification — on by default (opts.verify_hostname = true) via RFC 6125 §6.4 SAN matching. CN fallback is not supported (deprecated).
  • QUIC is anti-amplification limited to 3× received bytes (§21.1) before path validation completes; no configuration required — the limit is enforced in path.vr and verified by V7.
  • Rate-limit inbound: Semaphore for concurrent connections, leaky bucket for per-IP throughput.

Concurrency​

  • Use nursery with on_error: cancel_all to bound task trees.
  • Bounded channels (bounded(N)) to limit queue depth.
  • Avoid mutable shared state; prefer message-passing.
  • @verify(static) catches Send / Sync violations at compile time.

FFI​

  • Every extern "C" block comes with a boundary contract (requires, ensures, memory_effects, thread_safe, errors_via, @ownership).
  • Input pointers: validate non-null, bound-check length.
  • Output pointers: zero before return if returning on error.
  • Strings crossing the boundary: Text.from_utf8 — returns Result<Text, Utf8Error>, so invalid input is a value you handle.

Verification​

  • Safety-critical code: @verify(thorough).
  • Security-critical lemmas: @verify(certified) with a proof term.
  • @verify(certified) in CI for any module touching crypto, auth, or raw memory.

Auditing​

verum audit                      # scan deps against advisory DB
verum analyze --context          # capability context surface per function
verum analyze --escape           # reference-tier distribution
verum analyze --refinement       # refinement / verification coverage
verum analyze --all              # everything in one pass
verum smt-stats                  # solver-routing stats from the last build

Reporting vulnerabilities​

Security issues in Verum itself: email security@verum-lang.org with a PoC. The team follows a 90-day coordinated-disclosure policy.

See also​