AI Safety & Kernel-Level Security

Why Formal Methods Matter for AI Safety

Traditional software engineering relies on empirical testing—running code with sample inputs to check for defects. Autonomous agents, however, choose their next action at run time, and no test suite can enumerate every action an agent might propose.

Formal methods replace sampling with proof. VAREK compiles policy into obligations for an SMT decision procedure, which reasons over whole domains symbolically: every proposed action is SATISFIED (provably allowed), UNSATISFIED (provably not allowed) or UNKNOWN (cannot be decided within bounds). UNKNOWN is never coerced into a pass. Since v1.15, every SATISFIED verdict also carries a certificate that a small, independently written checker must accept before the action takes effect.

Verified Before the Agent Starts

Before the agent runs, the Warden's optional plan gate checks the agent's declared action-graph — every step against the policy and, with a flow policy, the data moving along its edges — and a load-time liveness proof certifies that every refusal ends in an automated outcome, so an unattended deployment never waits on a human.

• Cross-action data flow: a secret source cannot reach a forbidden sink, even when each step looks safe on its own.
• Declared intent, checked: plan steps can declare fields and, since v1.21.1, how they open a file (open=read), and the gate decides each step with exactly what it declares. Every call is still decided again at run time.

For pipelines written fresh, the VAREK language (stable at v1.0) is statically typed and LLVM-compiled, so unsafe operations are not expressible in the first place.

Kernel-Level Security with Seccomp

When an AI agent is given tool-use capabilities, it gains the power to interface with the underlying system. If an agent is steered by a prompt-injection exploit, it could read secrets, reach the network or tamper with your environment.

The VAREK Warden holds every policy-relevant system call at the kernel boundary using seccomp-BPF and seccomp user-notify, on a default-deny allowlist, and decides it before it runs:

• Files: each open is resolved once, decided on its canonical path, and the same descriptor is handed to the agent; each lookup is decided the same way and answered by the Warden — no path-traversal, symlink or /proc/self escape, and a denied open has no side effect.
• Network: since v1.21, each outbound connect is decided on the destination the Warden copied once; the Warden dials it itself and hands over the connected socket, so the destination cannot be swapped after the check.
• The agent itself: it runs unprivileged, cannot launch further programs, and is stopped — with everything it started — if the supervisor stops.
• The record: every record is hash-chained; checkpoints can be Ed25519-signed and anchored off the host; the stream exports in the CycloneDX 1.6 format.

Declaring a Policy

A Warden policy is an ordered list of rules. The first match wins, so the deny rules come first, and anything no rule matches is UNKNOWN and refused:

# Example VAREK Warden policy (first match wins)
require warden 1.21
deny  path  suffix .pem
deny  path  glob /**/.env
allow path  /srv/agent/reference/  readonly
allow path  /srv/agent/work/
allow host  10.0.0.12:443

The agent can read its reference data but not modify it, write its work directory, never open a file ending in .pem or named .env anywhere, and connect to one internal service; everything else is refused. (A real policy also grants the agent's runtime libraries, read-only.)