papers/hanzo-formal-verification/sections/03-agent-framework-verification.tex

\section{Agent Framework Verification}

\label{sec:agents}
% ============================================================================

The Hanzo Agent SDK~\cite{hanzoagentsdk} enables AI agents to perform
actions with delegated credentials. Three properties are critical:

\subsection{Safe Delegation}

An agent must never acquire permissions beyond what its delegator possesses.

\begin{definition}[Permission Lattice]
Permissions form a bounded lattice $(\mathcal{P}, \sqsubseteq, \sqcup, \sqcap,
\bot, \top)$ where $p_1 \sqsubseteq p_2$ means ``$p_1$ is a subset of $p_2$.''
The lattice operations:
\begin{itemize}[leftmargin=1.1em]
    \item $\sqcup$ (join): Union of permissions.
    \item $\sqcap$ (meet): Intersection of permissions.
    \item $\bot$: No permissions.
    \item $\top$: All permissions (root only).
\end{itemize}
\end{definition}

\begin{theorem}[Safe Delegation]
\label{thm:safe-delegation}
For any delegation chain $u \to a_1 \to \cdots \to a_k$ where $u$ is a user
with permissions $p_u$ and each $a_i$ delegates to $a_{i+1}$ with constraint
$c_i$:
\begin{equation}
p_{a_k} \sqsubseteq p_{a_{k-1}} \sqsubseteq \cdots \sqsubseteq p_{a_1}
\sqsubseteq p_u.
\end{equation}
That is, permissions monotonically decrease along any delegation chain.
\end{theorem}

The Lean 4 proof proceeds by induction on the chain length $k$, with the base
case ($k=1$) following from the delegation rule $p_{a_1} = p_u \sqcap c_1
\sqsubseteq p_u$.

\subsection{Credential Chain Validity}

\begin{theorem}[Chain Validity]
A credential chain is valid if and only if:
\begin{enumerate}[leftmargin=1.4em]
    \item The root certificate is signed by the platform root key.
    \item Each intermediate certificate is signed by its parent.
    \item Each certificate's permissions are $\sqsubseteq$ its parent's.
    \item No certificate has expired.
    \item No certificate has been revoked.
\end{enumerate}
The verification algorithm terminates in $O(k)$ time for chain length $k$ and
returns $\texttt{true}$ if and only if all five conditions hold.
\end{theorem}

\subsection{Bug Found: Permission Escalation via Revocation Race}

Formalization revealed a race condition: if a parent credential is revoked
while a child agent is mid-operation, the agent could complete the operation
with permissions derived from a now-revoked credential. The fix adds a
real-time revocation check at operation execution time, not just at credential
presentation time.

% ============================================================================