papers/lux-omnichain-yield/sections/10-formal-security-properties.tex

\section{Formal Security Properties}
\label{sec:security}
% ============================================================

We state and prove the key security invariants of the yield system. The implementation includes 54 security tests: unit tests for all share accounting edge cases, fuzz tests (256 runs per property) for conversion function robustness, and invariant tests (128K calls) verifying that share price monotonicity and collateralization bounds hold under arbitrary operation sequences.

\begin{property}[Conservation]\label{prop:conservation}
For every yield-bearing bridge token $yT$:
\begin{equation}
  S(t) \cdot p(t) \leq B(t) + \epsilon_{\text{rounding}}
\end{equation}
where $\epsilon_{\text{rounding}} \leq S(t)$ wei (at most 1 wei per outstanding share due to floor rounding).
\end{property}

\begin{proof}
By construction, deposits mint $\lfloor a / p(t) \rfloor$ shares for $a$ assets deposited, so the share value never exceeds the deposit. Withdrawals burn shares before releasing assets. Yield increases $B(t)$ without increasing $S(t)$ (shares are only minted for deposits and fee extraction). Fee shares are minted against yield already in $B(t)$. The rounding bound follows from the floor operation in Equation~(\ref{eq:toShares}).
\end{proof}

\begin{property}[Undercollateralization Detection]
If $B(t) < \theta_{\min} \cdot S(t) \cdot p(t_{k-1})$, the bridge pauses within $\Delta + \delta_{\text{confirm}}$.
\end{property}

\begin{proof}
Direct from Theorem~\ref{thm:pause}.
\end{proof}

\begin{property}[No Share Price Manipulation]
An external actor cannot decrease $p(t)$ through deposit, withdrawal, or harvest operations.
\end{property}

\begin{proof}
\textit{Deposit}: increases $B$ by $a$ and $S$ by $a/p(t)$, leaving $p$ unchanged.
\textit{Withdrawal}: decreases $B$ by $s \cdot p(t)$ and $S$ by $s$, leaving $p$ unchanged.
\textit{Harvest}: increases $B$ by harvested yield, does not change $S$, so $p$ increases.
\textit{Fee extraction}: mints shares against existing yield in $B$, yielding $p' > p$ (Section~\ref{sec:fees}).
No operation decreases $p$.
\end{proof}

\begin{property}[Exit Guarantee]
Users holding yield-bearing bridge tokens can redeem for underlying assets within the MPC liveness bound (7 days worst case under signer rotation) regardless of bridge pause state.
\end{property}

\begin{proof}
The \texttt{burnForWithdrawal} function is never disabled, even in \texttt{PAUSED} state. Only minting is disabled on pause. The MPC set signs withdrawal releases as long as $t$-of-$n$ signers are operational. Under signer rotation (7-day timelock), the current signer set remains active until the rotation completes.
\end{proof}

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