mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-03 05:07:46 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
36 lines
1.4 KiB
TeX
36 lines
1.4 KiB
TeX
\section{Limitations and Honest Assessment}
|
|
|
|
|
|
\subsection{Path Explosion}
|
|
|
|
Contracts with many branches, loops, or recursive calls generate exponentially many paths.
|
|
Halmos mitigates this with loop bounding but cannot eliminate it. Complex DeFi protocols
|
|
with nested callbacks may exceed practical limits.
|
|
|
|
\subsection{External Calls}
|
|
|
|
Halmos cannot reason about external contracts it has not seen. Cross-contract interactions
|
|
are modeled abstractly: external calls return symbolic values. This means Halmos cannot
|
|
prove properties that depend on the behavior of external contracts.
|
|
|
|
\subsection{Hash Functions}
|
|
|
|
Halmos treats \texttt{keccak256} as an uninterpreted function: it knows that
|
|
\texttt{keccak256(x) = keccak256(x)} (reflexivity) but not that
|
|
\texttt{keccak256(x) != keccak256(y)} when \texttt{x != y} (collision resistance).
|
|
This occasionally produces spurious counterexamples involving hash collisions that
|
|
are practically impossible.
|
|
|
|
\subsection{What Halmos Does Not Replace}
|
|
|
|
Halmos proves properties of Solidity bytecode for all inputs within bounded loop
|
|
iterations. It does not replace:
|
|
\begin{itemize}[nosep]
|
|
\item Manual auditing (business logic errors, economic attacks).
|
|
\item Fuzzing (faster at finding common bugs).
|
|
\item Formal protocol verification (protocol design correctness).
|
|
\item Operational security (key management, deployment procedures).
|
|
\end{itemize}
|
|
|
|
%% ============================================================
|