verifying-crypto-with-lean/chapters/ch13-attestation-protocol.tex

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