\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.