diff --git a/chapters/ch11-honesty-and-axioms.tex b/chapters/ch11-honesty-and-axioms.tex index 7a9dfad..156e940 100644 --- a/chapters/ch11-honesty-and-axioms.tex +++ b/chapters/ch11-honesty-and-axioms.tex @@ -11,6 +11,15 @@ every file compiles. Nothing here is hypothetical --- each failure mode appears in the wild, and the discipline below is the one the companion projects hold themselves to. +\begin{pitfall} +This chapter teaches you to interrogate a \emph{certificate}. It does not teach +you to interrogate the \emph{script that interrogates certificates for you} --- +and that script is software you wrote, verified by nothing. +Chapter~\ref{ch:attestation} is about that second problem, which turned out to +be far harder than everything in this chapter, and is where every failure in the +companion projects has occurred. +\end{pitfall} + \section{The trust ledger} When the kernel accepts \lean{fieldImplementation}, what exactly are you diff --git a/chapters/ch13-attestation-protocol.tex b/chapters/ch13-attestation-protocol.tex new file mode 100644 index 0000000..887d968 --- /dev/null +++ b/chapters/ch13-attestation-protocol.tex @@ -0,0 +1,223 @@ +\chapter{The Attestation Protocol: Who Checks the Checker?} +\label{ch:attestation} + +\section{The second act nobody warns you about} + +Chapter~\ref{ch:honesty} taught you to interrogate a certificate: ask what it +rests on, and refuse to be impressed by a file that merely compiles. That +chapter had a blind spot, and this one exists because a sequence of external +reviewers found it. + +The blind spot is this. \lean{\#print axioms} tells \emph{you}, at \emph{your} +terminal, that a theorem's cone is clean. Then you write a script that runs it +across your project, the script prints \texttt{ALL GREEN}, and you publish that +green light as evidence. Between the kernel's verdict and the reader's belief +sits a piece of software you wrote --- and \emph{that software is not verified +by anything}. + +\begin{bigidea} +Verification is \textbf{two acts}, not one. + +\textbf{Act one --- proof.} The Lean kernel decides whether a term is a valid +derivation of its statement. This is mathematics. It is what everyone pictures +when they hear ``formally verified''. + +\textbf{Act two --- attestation.} Establishing that what the kernel accepted is +what you \emph{claim}, resting only on what you \emph{say} it rests on, about +the artifact you \emph{say} it concerns --- and that a stranger who was not +present and does not trust you can check every part of that for themselves. + +\medskip +\textbf{Lean decides whether a proof is valid. The Attestation Protocol decides +whether anyone else can know that.} A proof without an attestation protocol is +a private conviction, not public evidence. +\end{bigidea} + +The companion projects learned this expensively. In one campaign, eleven +theorems about a hash-based signature verifier were proved in \textbf{two days} +and no reviewer ever disputed one of them. Making the green light over those +same eleven theorems mean something to a determined skeptic took \textbf{eight +rounds of review} and turned up \textbf{eighteen distinct defect classes} --- +none of them in the mathematics, all of them in act two. + +\section{The shape of every failure} + +Here is the finding that makes this chapter teachable. All eighteen defects had +\emph{one shape}: + +\begin{aha} +\textbf{Something load-bearing sat outside the binding.} + +The audit was always \emph{sound} about what it examined. The entire attack +surface was what it did \emph{not} examine. +\end{aha} + +Read the greatest hits and watch the pattern repeat. Each of these was +demonstrated end-to-end against a button that was printing \texttt{ALL GREEN} +at the time: + +\begin{itemize} + \item \textbf{The certificate list was outside.} Delete one row from the list + of audited theorems and that theorem silently leaves the audit. Nothing + noticed. + \item \textbf{Un-listed declarations were outside.} Add + \lean{axiom cheat : ∀ (P : Prop), P} and + \lean{theorem oops : False := cheat _} to a proof file. The audit + checked the theorems on its list; this one was not on the list. + \textbf{The repository proved \lean{False} and the button stayed + green.} + \item \textbf{Non-theorems were outside.} After that was fixed, the same + payload as a \lean{def} rather than a \lean{theorem} passed --- the + enumeration matched only theorems. + \item \textbf{The auditor was outside itself.} After \emph{that} was fixed, + the same payload placed \emph{inside the audit driver} passed, because + the driver was exempt from its own enumeration. + \item \textbf{Statements were outside.} Replace a theorem's statement with a + tautology that happens to have the same axiom cone. Passes. + \item \textbf{Specifications were outside.} This is the subtle one. Each + certificate said ``the extracted loop equals this hand-written + reference fold''. Redefine the fold to \emph{be} the extracted loop. + The certificate now says \emph{the loop equals the loop} --- vacuous --- + and the axiom cone, the statement hash, and the digest are all + \textbf{byte-identical}. + \item \textbf{The policy was outside.} The audit compared each cone against a + list of permitted axioms. That list was not itself covered by the + digest. Add one name to it and every protection re-opens, digest + unchanged. + \item \textbf{The subject was outside.} The proofs were about a generated + model file. Hand-edit the model; every phase still passes. + \item \textbf{The tools were outside.} Stub the compiler-wrapper script and + the button printed \texttt{ALL GREEN} in \textbf{3.6 seconds} over + deliberately destroyed proofs. Flip two characters in the audit + driver's fail-closed guards and every check switched off with the + digest byte-identical. +\end{itemize} + +\begin{pitfall} +Notice what is \emph{not} on that list: a wrong proof, a wrong theorem, a bug in +Lean. The kernel did its job perfectly throughout. Every single failure was in +the apparatus built \emph{around} it --- by the same person who was reporting +the results. +\end{pitfall} + +\section{Completeness of binding} + +Because the failures all have one shape, the property to design for has one +name. It is not soundness --- soundness was never the problem. + +\begin{bigidea} +\textbf{Completeness of binding.} Everything load-bearing is inside the binding: +the statements, the definitions those statements are stated \emph{against}, the +policy that decides what is permitted, the bytes of the artifact being reasoned +about, and the tools doing the checking. +\end{bigidea} + +Four rules follow, and each one is the generalisation of a defect above. + +\subsection{Derive the population; never keep a list} + +A hand-maintained list of ``things that must be checked'' is one more thing that +can fall out of sync --- and did, twice. Derive membership instead: + +\begin{itemize} + \item from the \emph{environment}: every declaration in these modules, obtained + by walking the environment, not by naming them; + \item from the \emph{filesystem}: every \lean{.lean} file under the generated + directory must appear in the hash map, so a new file fails closed; + \item from the \emph{type system}: the transitive closure of constants a + statement mentions, so a new reference definition cannot appear + unnoticed; + \item from a \emph{file attribute}: every executable file in the verification + directory must be pinned --- so adding a script fails until you pin it. +\end{itemize} + +\subsection{Fail closed on absence} + +\begin{pitfall} +The most common bug in an audit script: \emph{nothing found} and \emph{nothing +wrong} share a code path. + +A missing report, an empty cone, a truncated line, a renamed theorem, an absent +map key --- each of these must be a build failure. In the campaign above, +fail-open-on-absence was both the \emph{first} defect found and the +\emph{last}. +\end{pitfall} + +\subsection{Exact, not subset} + +Checking that a cone contains nothing forbidden is not enough. A certificate can +lie by resting on \emph{less} than you declared as well as more --- if your +theorem quietly stopped depending on the hash function, something is very wrong, +and a subset check will smile at you. Require set \emph{equality}. + +\subsection{A stranger must be able to re-derive it} + +The final rule is the one that separates evidence from assertion. Publish a +digest a reader can recompute; commit the input that digest is taken over, so a +mismatch can be \emph{diffed} rather than merely reported; and record who ran +the check, on what machine, at which commit. + +\section{The meta-defect: assertions that pass for the wrong reason} + +There is a second lesson, about \emph{tests} rather than about products, and it +is humbling enough to state plainly. Across the same eight rounds, \textbf{eight +separate assertions were found to be checking nothing} --- including two inside +fixes written to repair that very problem. + +The purest specimen. A script transformed a data file by dropping one field, and +carried this line: + +\begin{lstlisting}[language=Python] +kept = {k: v for k, v in record.items() if k not in DROP} +assert set(kept) == set(record) - DROP # can never fail +\end{lstlisting} + +\lean{kept} was built by the comprehension on the line above. The assertion is a +tautology. The first attempt to repair it compared \lean{kept[k]} against +\lean{record[k]} --- tautological for exactly the same reason. + +\begin{aha} +\textbf{No check inside a transformer can detect a corrupted input, because the +transformer is what defines the output from that input.} + +Faithfulness there is a property a \emph{reviewer reads}, not something the code +can test about itself. What can actually fail --- and therefore what must carry +the weight --- is the pin on the input, the presence and count guards, and an +independent re-derivation. +\end{aha} + +\begin{tryit} +Take any test you have written that guards an important property. Now +\textbf{break the thing it guards} and run it. + +If it does not go red --- or goes red with a message about something else --- +you have a decoration, not a test. Do this for every guard you own. In the +campaign described here, that exercise would have caught eight defects, and the +people who eventually caught them were strangers. +\end{tryit} + +\section{What this means for you} + +You will not build an eighteen-attack self-test for a homework exercise, and you +should not. What you should take away is a habit of mind and a vocabulary. + +\begin{checkpoint} +When you next read the words ``formally verified'', ask two questions instead of +one. + +\textbf{Act one:} what statement did a kernel accept, and what does it rest on? +(Chapter~\ref{ch:honesty} taught you this.) + +\textbf{Act two:} what binds that statement to the artifact I care about, who +checked, what did the checker \emph{not} look at, and can I re-derive any of it +myself? + +If a project cannot answer the second set, it has done act one and called it +finished --- which is exactly the mistake these chapters were rewritten to +prevent. +\end{checkpoint} + +And when it is your own project: invite someone to attack the button, early. +Every one of the eighteen defects was found by a reviewer trying to break it. +\emph{None} was found by the author reviewing their own work --- and the author +looked, repeatedly, with the same care they had used to write the proofs. diff --git a/main.tex b/main.tex index a2dce53..4cc0ecf 100644 --- a/main.tex +++ b/main.tex @@ -151,6 +151,7 @@ For self-study or a seminar, the book paces naturally as a semester: \input{chapters/ch10-verifying-a-field} \input{chapters/ch11-honesty-and-axioms} \input{chapters/ch12-the-pyramid} +\input{chapters/ch13-attestation-protocol} \appendix \input{chapters/appendix-toolkit}