mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +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.
32 lines
1.6 KiB
TeX
32 lines
1.6 KiB
TeX
\section{The Invariant: Machine-Checkable Security Claims}
|
|
|
|
\label{sec:invariant}
|
|
|
|
\begin{invariant}[Machine-checkable security]
|
|
Every security property of the Lux Network either:
|
|
\begin{enumerate}[leftmargin=2em]
|
|
\item Has a machine-checkable proof (formal verification in Coq, Lean, or TLA+), or
|
|
\item Has an automated test suite that verifies the property against known test
|
|
vectors, or
|
|
\item Is explicitly listed as an unverified assumption with a justification for
|
|
why it is believed to hold.
|
|
\end{enumerate}
|
|
There is no fourth category. ``We believe it is secure'' without one of the above
|
|
annotations is not a valid security claim.
|
|
\end{invariant}
|
|
|
|
This invariant is not aspirational---it is a \emph{process requirement}. Every
|
|
protocol change must be accompanied by an update to one of the three categories.
|
|
New cryptographic primitives require either a proof reference or NIST KAT validation.
|
|
New consensus rules require either a formal proof or a TLA+ model. New implementations
|
|
require either formal verification or an automated test suite with coverage metrics.
|
|
|
|
The purpose of this invariant is not to achieve 100\% formal verification (which is
|
|
impractical for a large system). The purpose is to eliminate the category of
|
|
``security claims that nobody has checked.'' Every claim is checked by a machine, a
|
|
proof system, or a test suite---or it is explicitly marked as unchecked.
|
|
|
|
%% ========================================================================
|
|
%% 10. RELATED WORK
|
|
%% ========================================================================
|