diff --git a/chapters/ch01-why-verify.tex b/chapters/ch01-why-verify.tex index 9ee062a..db202a2 100644 --- a/chapters/ch01-why-verify.tex +++ b/chapters/ch01-why-verify.tex @@ -3,12 +3,23 @@ \section{A story about one carry bit} -In 2014, researchers examining widely deployed elliptic-curve code found -arithmetic bugs of a very particular species: the code was correct on -\emph{almost every} input. Not most inputs --- almost all of them, in a -precise sense. One famous example, a carry-propagation flaw in an -implementation of curve25519 arithmetic, produced a wrong answer with -probability on the order of $2^{-64}$ per random input. +Here is the entire bug that this book exists because of: + +\begin{lstlisting} + h[4] += carry; // propagate the top limb's overflow +- // (missing: one more conditional subtraction of p) ++ if (h[4] >= LIMB_CAP) h[4] -= LIMB_CAP, h[0] += 19; +\end{lstlisting} + +\noindent One missing line. A field-arithmetic routine that forgets a single +final carry is correct on \emph{almost every} input --- not most, almost +\emph{all} of them, in a precise sense --- and silently wrong on the rare +ones where that last carry would have fired. Bugs of exactly this species +were found in deployed elliptic-curve code and became the motivating +disaster behind a whole line of verification research (the Fiat-Cryptography +project, Erbsen et al., IEEE S\&P 2019 --- a direct ancestor of the work this +book teaches). A representative one produced a wrong answer with probability +on the order of $2^{-64}$ per random input. Pause on that number. If you tested this function a billion times per second, around the clock, you should expect to wait \emph{centuries} before a random @@ -24,41 +35,18 @@ than the square of the number of atoms in the observable universe. Testing samples a raindrop from that ocean. \end{pitfall} -\begin{worked}{feel what $2^{-64}$ means, with the real numbers} -Claims about astronomical improbability deserve to be checked by hand, so -check this one. A failure probability of $2^{-64}$ per random input means -you expect one hit per $2^{64}$ trials. First, get $2^{64}$ into scientific -notation the way you always can: $\log_{10} 2 \approx 0.30103$, so -\[ -\log_{10} 2^{64} = 64 \times 0.30103 \approx 19.27 -\qquad\Longrightarrow\qquad -2^{64} \approx 1.8 \times 10^{19}. -\] -At $10^9$ tests per second, the expected waiting time is -\[ -\frac{1.8 \times 10^{19}}{10^{9}} = 1.8 \times 10^{10} \text{ seconds}. -\] -A year is $\approx 3.15 \times 10^{7}$ seconds (a number worth memorizing: -``$\pi \times 10^7$ seconds per year'' is accidentally almost exact), so -\[ -\frac{1.8 \times 10^{10}}{3.15 \times 10^{7}} \approx 580 \text{ years}. -\] -So: a test farm hammering this function a \emph{billion} times per second, -started when Copernicus published, would be expected to see the bug for the -first time about now. And this is the \emph{optimistic} case where failing -inputs are hit by uniform sampling --- for carry bugs they are typically -\emph{correlated}, clustered in corners uniform sampling underweights. - -Now the input space itself. A single \lean{FieldElement} is 255 bits; a -pair is 510 bits, and -\[ -\log_{10} 2^{510} = 510 \times 0.30103 \approx 153.5 -\qquad\Longrightarrow\qquad -2^{510} \approx 10^{153}. -\] -For comparison, the number of atoms in the observable universe is around -$10^{80}$. Testing all pairs is not ``hard''; it is not a thing that -happens in this universe. +\begin{worked}{feel what $2^{-64}$ means} +One hit per $2^{64}$ trials, and $2^{64} \approx 1.8 \times 10^{19}$. At a +billion tests a second that is $1.8 \times 10^{10}$ seconds to expect a +single failure --- about \textbf{580 years}. So a test farm hammering this +function a \emph{billion} times per second, started when Copernicus +published, would be expected to see the bug for the first time about now. +And that is the \emph{optimistic} case: carry bugs cluster in exactly the +corners uniform sampling underweights, so in practice you wait longer than +the calendar of the universe. (The one-line $\log_{10}$ derivation behind +``580 years,'' and the far more hopeless arithmetic for the full 510-bit +space of input \emph{pairs}, are Exercise~1.1 --- worth doing, because the +number that falls out has more digits than the universe has atoms.) \end{worked} Why does cryptographic code have bugs of exactly this shape? Because of how it @@ -102,10 +90,12 @@ headroom count, and the headroom count is where the bodies were buried. \end{worked} And in cryptography, ``rare wrong answer'' does not mean ``rare small -glitch.'' Wrong field arithmetic can leak private keys: several published -attacks turn a single faulty group operation into full key recovery. The -stakes are not a corrupted pixel; they are every signature your machine has -ever made. +glitch.'' Wrong field arithmetic can leak the private key itself: published +attacks in the ``invalid-curve'' and fault-injection families turn a +\emph{single} faulty group operation into full key recovery --- the attacker +feeds inputs engineered to land in the buggy corner, and reads the secret +off the wrong answers. The stakes are not a corrupted pixel; they are every +signature your machine has ever made, and every one it ever will. \section{There is another way} @@ -122,8 +112,10 @@ Every input, forever, or the proof does not check. The tool that checks such arguments is called a \emph{proof assistant}. This book uses \textbf{Lean~4}, a modern proof assistant that is also a -full-fledged programming language. Others you may have heard of: Rocq -(formerly Coq), Isabelle/HOL, Agda. The ideas transfer; the syntax differs. +full-fledged programming language.\footnote{You may have heard of Rocq +(formerly Coq), Isabelle/HOL, or Agda. The ideas in this book transfer to +all of them; only the syntax differs. We pick Lean~4 for reasons that will +be concrete by the end of this chapter.} A proof assistant is built around a small, paranoid core called the \emph{kernel}. Everything you will learn in this book --- clever tactics, @@ -171,21 +163,30 @@ one abstraction level and rests on the layer beneath it: \end{tikzpicture} \end{center} -By the end of this book you will be able to read --- and extend --- the real -proofs at every layer of this pyramid. The journey looks like this: +\begin{tryit} +Before you read another word, go and touch the thing this book is about. Open +\textbf{\code{ltl.zkdefi.org}} on any device. You are looking at a public, +append-only log of machine-checked proofs --- 19 entries, each one a claim of +the form ``this exact version of this software was verified, resting on +exactly these assumptions.'' Entries 13--16 are the four Ed25519 libraries +whose pyramid you see above. Entry~18 is the first \emph{post-quantum} entry +in the log. You cannot read the proofs yet --- that is what the next twelve +chapters are for --- but you can already see that they are real, public, and +checkable by a stranger with a stock laptop. That stranger is who you are +becoming. +\end{tryit} -\begin{itemize}[leftmargin=1.4em] -\item \textbf{Chapters 2--5} teach Lean itself, from \code{\#eval 1+1} to - proofs by induction and the automation that dispatches arithmetic goals. -\item \textbf{Chapters 6--7} build the mathematics: modular arithmetic, finite - fields, and how to convince a paranoid kernel that a 77-digit number is - prime. -\item \textbf{Chapters 8--9} cross the bridge from Rust to Lean: how real - code is translated into a form we can reason about, and the single most - important idea in the whole enterprise --- the \emph{denotation function}. -\item \textbf{Chapters 10--12} assemble the pyramid: field correctness, the - ethics of axioms and honest boundaries, and the layers above. -\end{itemize} +By the end of this book you will be able to read --- and extend --- the real +proofs at every layer of this pyramid. To make that concrete, here is what +you will personally be able to \emph{do}, and roughly when: by Chapter~7 you +will have handed a paranoid kernel a certificate that a 77-digit number is +prime, and watched it agree; by Chapter~9 you will read real Rust translated +into Lean and understand the one idea (the \emph{denotation function}) that +makes the translation trustworthy; by Chapter~12 you will stand on the apex +and read the signature-verification theorem for the actual code in your SSH +client. The chapters between here and there earn each of those, in order --- +Lean itself first, then the mathematics, then the bridge from real code, then +the climb. \begin{bigidea} \textbf{The ratchet rule of this book.} Every load-bearing idea is worked @@ -239,20 +240,24 @@ Learning to smell those is as important as learning to write proofs at all. \section{Why Lean, and why now} Twenty years ago, verifying real cryptographic C or Rust code was a heroic, -multi-year effort. Three things changed: +multi-year effort. Three things changed --- and each one is an advantage +\emph{you} inherit the moment you start: \begin{enumerate}[leftmargin=1.6em] -\item \textbf{Proof assistants matured.} Lean~4 is fast, pleasant, and comes - with \emph{Mathlib}, a library of over a million lines of formalized - mathematics --- finite fields and elliptic-curve ingredients included, so we - do not start from bare axioms. -\item \textbf{Translation pipelines appeared.} Tools like \emph{Charon} and - \emph{Aeneas} mechanically translate real Rust code into Lean definitions, - so the thing we verify is derived from the code that ships, not a - hand-transcribed approximation (Chapter~\ref{ch:rust}). -\item \textbf{Automation got serious.} Decision procedures like \lean{omega} - (linear integer arithmetic) and \lean{decide} discharge the boring 90\% of - goals, leaving humans the interesting 10\%. +\item \textbf{You start on a million lines of proved mathematics.} Lean~4 + ships with \emph{Mathlib} --- finite fields, elliptic curves, number theory, + already formalized and checked. You do not build the tower from bare axioms; + you walk onto a finished floor and add one room. +\item \textbf{You verify the code that ships, not a story about it.} Tools + called \emph{Charon} and \emph{Aeneas} mechanically translate real Rust into + Lean, so what you reason about is \emph{derived} from the deployed source + rather than hand-copied by someone who might have copied it wrong + (Chapter~\ref{ch:rust}). This is the difference between verifying software + and verifying an essay about software. +\item \textbf{The machine does the boring 90\%.} Decision procedures like + \lean{omega} and \lean{decide} dispatch the routine arithmetic goals on + their own, so your attention goes to the 10\% that is actually interesting + --- the part where the real idea lives. \end{enumerate} None of this made verification \emph{easy}. It made verification diff --git a/chapters/ch07-primality-certificates.tex b/chapters/ch07-primality-certificates.tex index e5d84f3..1deaddf 100644 --- a/chapters/ch07-primality-certificates.tex +++ b/chapters/ch07-primality-certificates.tex @@ -52,8 +52,13 @@ Concretely for our hero: $p - 1 = 2^{255} - 20$ factors as \[ p - 1 \;=\; 2^{2} \cdot 3 \cdot 65147 \cdot Q, \] -where $Q$ is a 71-digit prime with its own (short) certificate, and -$65147$ recurses one more level: $65146 = 2 \cdot 32573$ with $32573$ +where $Q$ is the 71-digit prime +\[ +Q = 740582127325613583022312264370627886761\allowbreak 66966415465897661863160754340907, +\] +printed here in full --- no hidden digits, this is the exact value in the +repository's \code{P25519.lean} --- carrying its own (short) certificate, +and $65147$ recurses one more level: $65146 = 2 \cdot 32573$ with $32573$ prime. The full certificate for $p$ is a small tree of witnesses and factorizations --- a few hundred bytes of data standing behind a 77-digit claim: diff --git a/main.pdf b/main.pdf index 599a1ed..c8520d8 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.tex b/main.tex index 4cc0ecf..c9ed2e2 100644 --- a/main.tex +++ b/main.tex @@ -28,8 +28,11 @@ no prior formal-verification or Lean experience assumed.\par} \vspace{0.8cm} {\color{ink2}\rule{\linewidth}{0.6pt}} \vspace{0.3cm} -{\small\color{paper} Companion to the \code{*-ed25519-verified} and \code{pasta-pallas-verified} -proof projects. \\ Every code snippet in this book runs. Every claim it makes about a proof, a proof assistant has checked.\par} +{\small\color{paper} Companion to a public transparency log of machine-checked +proofs --- \textbf{\code{ltl.zkdefi.org}}, 19 entries and counting, one of them +post-quantum. Open it on your phone now; by the last chapter you will be able +to verify every entry yourself. \\ Every code snippet in this book runs. Every +claim it makes about a proof, a proof assistant has checked.\par} \end{titlepage} \restoregeometry \pagecolor{paper}\color{ink} @@ -39,6 +42,13 @@ proof projects. \\ Every code snippet in this book runs. Every claim it makes ab \markboth{How to read this book}{} \addcontentsline{toc}{chapter}{How to read this book} +There is a public web page --- \code{ltl.zkdefi.org} --- that lists nineteen +pieces of software, each stamped with a machine-checked proof that it does what +it claims. One of those stamps was earned two days before the writer of that +proof could make anyone else believe it; another survived quantum-resistant +cryptography. This book is the road from not understanding a single word on that +page to being able to verify every entry on it yourself, and to add your own. + You are about to learn one of the most powerful ideas in computer science: how to make a computer \emph{prove} that a program is correct --- not test it on a few inputs and hope, but establish, with the certainty of mathematics, that it