papers/hanzo-formal-verification/sections/04-api-gateway-verification.tex

\section{API Gateway Verification}

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

The Hanzo Gateway~\cite{hanzogateway} routes all API requests. We verify three
properties.

\subsection{Routing Correctness}

\begin{definition}[Route Table]
A route table $\mathcal{T}: \texttt{Path} \times \texttt{Method} \to
\texttt{Backend}$ maps (path, HTTP method) pairs to backend services.
Routes have priorities; the highest-priority matching route is selected.
\end{definition}

\begin{theorem}[Route Determinism]
For any request $(p, m)$, the routing function $\texttt{route}(\mathcal{T},
p, m)$ returns exactly one backend service or $\texttt{404}$. No request
matches two routes with equal priority (this is enforced as a well-formedness
condition on $\mathcal{T}$).
\end{theorem}

\subsection{Rate Limiter Fairness}

\begin{definition}[Token Bucket]
A token bucket $B = (r, b, t)$ has refill rate $r$ tokens per second, burst
capacity $b$, and current tokens $t$. A request consuming $c$ tokens is
admitted if $t \geq c$.
\end{definition}

\begin{theorem}[Rate Limiter Fairness]
For two organizations with identical rate limit configurations $(r, b)$, the
maximum difference in admitted requests over any time window $[0, T]$ is
bounded by the burst capacity $b$:
\begin{equation}
|A_1(T) - A_2(T)| \leq b.
\end{equation}
\end{theorem}

\subsection{Authentication Chain Soundness}

\begin{theorem}[Auth Soundness]
If the gateway admits a request with org claim $o$, then:
\begin{enumerate}[leftmargin=1.4em]
    \item A valid JWT exists, signed by the IAM signing key.
    \item The JWT has not expired.
    \item The org $o$ in the JWT matches the org injected into downstream
    headers.
    \item All downstream data queries are scoped to org $o$.
\end{enumerate}
No combination of request headers can cause the gateway to inject an org
different from the one in the validated JWT.
\end{theorem}

\subsection{Bug Found: Path Traversal in Route Matching}

Formalization revealed that URL-encoded path separators (\texttt{\%2F}) were
not normalized before route matching, allowing requests to bypass path-based
access controls. The fix adds URL normalization as the first step in the
routing pipeline.

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