mirror of
https://github.com/hanzoai/papers.git
synced 2026-10-29 07:34:31 +00:00
55 lines
2.0 KiB
TeX
55 lines
2.0 KiB
TeX
\section{KMS Secrets Verification}
|
|
|
|
\label{sec:kms}
|
|
% ============================================================================
|
|
|
|
Hanzo KMS~\cite{hanzokms} manages 12,000+ secrets with envelope encryption.
|
|
|
|
\subsection{Envelope Encryption Correctness}
|
|
|
|
\begin{definition}[Envelope Encryption]
|
|
A secret $s$ is encrypted as $\texttt{Enc}_{KEK}(\texttt{DEK}) \|
|
|
\texttt{Enc}_{DEK}(s)$ where DEK is a per-secret data encryption key and
|
|
KEK is the master key encryption key.
|
|
\end{definition}
|
|
|
|
\begin{theorem}[Encryption Correctness]
|
|
For any secret $s$ and keys $(KEK, DEK)$:
|
|
\begin{equation}
|
|
\texttt{Dec}_{DEK}(\texttt{Enc}_{DEK}(s)) = s,
|
|
\end{equation}
|
|
and
|
|
\begin{equation}
|
|
\texttt{Dec}_{KEK}(\texttt{Enc}_{KEK}(DEK)) = DEK.
|
|
\end{equation}
|
|
Composition: the full decrypt-unwrap pipeline recovers $s$ exactly.
|
|
\end{theorem}
|
|
|
|
\subsection{Key Rotation Safety}
|
|
|
|
\begin{theorem}[Rotation Safety]
|
|
During key rotation from $KEK_{\text{old}}$ to $KEK_{\text{new}}$:
|
|
\begin{enumerate}[leftmargin=1.4em]
|
|
\item No secret $s$ is ever stored in plaintext (the DEK is always
|
|
encrypted under at least one KEK).
|
|
\item No secret is inaccessible (either $KEK_{\text{old}}$ or
|
|
$KEK_{\text{new}}$ can decrypt the DEK at every point during rotation).
|
|
\item After rotation completes, $KEK_{\text{old}}$ can be safely destroyed
|
|
without losing access to any secret.
|
|
\end{enumerate}
|
|
\end{theorem}
|
|
|
|
The proof models rotation as a state machine with five states (idle, re-wrap
|
|
started, re-wrap in progress, re-wrap completed, old key destroyed) and proves
|
|
that the safety invariant holds at every state transition.
|
|
|
|
\subsection{Bug Found: Partial Rotation Failure}
|
|
|
|
Formalization revealed that if the re-wrap process fails mid-way (e.g.,
|
|
database connection lost), some secrets remain wrapped under the old KEK while
|
|
others are wrapped under the new KEK. If the old KEK is then destroyed
|
|
(automated cleanup), the un-re-wrapped secrets become inaccessible. The fix
|
|
adds a rotation completion check before old key destruction.
|
|
|
|
% ============================================================================
|