Files
papers/kai/sections/06-authority.tex

76 lines
3.3 KiB
TeX

\section{Policy is the authority}
\label{sec:authority}
A model answering ``may this command run?'' will sometimes be wrong, and some
of its evidence is written by an adversary: a file the agent read, a page it
fetched. Prompt injection is a property of any model that reads untrusted text,
so the question is what the system does when the model is wrong. The answer
here is structural.
\begin{definition}[Verdicts]
The verdicts are the chain $V = \{\allow, \ask, \deny\}$ ordered
$\allow < \ask < \deny$, with join $a \join b = \max(a, b)$.
\end{definition}
A deterministic policy $\pi$, written by people and reviewed like code, maps a
state to a verdict before any model runs: reading \texttt{\textasciitilde/.ssh}
with network egress is \deny{} by rule; with no rule, \allow{} means only ``no
objection''. A program maps the state to a model verdict $\mu(s)$, and an
enforced program's effective verdict is
\begin{equation}
\varepsilon(s) = \pi(s) \join \mu(s).
\label{eq:join}
\end{equation}
\begin{proposition}[The model only tightens]
\label{prop:tighten}
For every state $s$ and every $\mu(s)$, $\varepsilon(s) \ge \pi(s)$; hence
$\{s : \varepsilon(s) = \allow\} \subseteq \{s : \pi(s) = \allow\}$.
\end{proposition}
\begin{proof}
$\max(a, b) \ge a$, and \allow{} is the least element.
\end{proof}
\begin{corollary}
\label{cor:envelope}
The safety envelope is the policy's. An adversary who controls the state
completely, and so $\mu(s)$, can make an action ask or be refused where the
policy would allow it, and nothing else.
\end{corollary}
\paragraph{Abstention, escalation, modes.}
If the verdict question's answer $p$ has $\kappa_p$ below its threshold,
$\mu(s) = \ask$; otherwise $\arg\max_i p_i$. An escalation is a \op{noul}
that raises the verdict when $p_{\op{true}}$ reaches its threshold (``could
this command send credentials?'' to \deny{} at 0.3,
Appendix~\ref{app:program}); escalations are joins, so
Proposition~\ref{prop:tighten} still holds. In \emph{shadow} $\mu$ is only
recorded, in \emph{advisory} shown, and in both $\varepsilon = \pi$; in
\emph{enforced}, $\varepsilon = \pi \join \mu$. A gate pinned to a
calibration runs in shadow when an input was answered under another
\shipped.
\begin{proposition}[Enforcement costs only friction]
\label{prop:friction}
Over a shadow sample, the states on which enforcing a program would change
the outcome are exactly $F = \{s : \mu(s) > \pi(s)\}$, and on each the change
is to a stricter verdict.
\end{proposition}
\begin{proof}
$\pi(s) \join \mu(s) \ne \pi(s)$ iff $\mu(s) > \pi(s)$, and then the join is
$\mu(s)$.
\end{proof}
The shadow record is thus the complete counterfactual of enforcement: each
state in $F$ is a catch or friction, both counts once people label them, and
promotion asks only whether the catches are worth the friction. No estimate of
the model's miss rate is needed; enforcement cannot make a miss worse than the
policy's own.
\paragraph{Constraints and preferences.}
A routing or context program splits in two. The \emph{constraint} (which
providers may see this state) lives in a lattice with the same rule: policy
sets the floor, the model may only raise it. The \emph{preference} (cheap or
frontier among permitted models) is the model's, defaulting toward quality on
abstention; a wrong preference costs money or quality, never a constraint.