diff --git a/paper/ltl.pdf b/paper/ltl.pdf index dcb96fc..3287348 100644 Binary files a/paper/ltl.pdf and b/paper/ltl.pdf differ diff --git a/paper/ltl.tex b/paper/ltl.tex index 7bfe8d8..a3d44c2 100644 --- a/paper/ltl.tex +++ b/paper/ltl.tex @@ -97,8 +97,9 @@ $E : -x^2+y^2 = 1+d\,x^2y^2$ over $\mathbb{F}_p$, \Bigl(\tfrac{x_1y_2+x_2y_1}{1+d\,x_1x_2y_1y_2},\; \tfrac{y_1y_2+x_1x_2}{1-d\,x_1x_2y_1y_2}\Bigr), \end{equation*} -including the completeness fact that makes it branch-free ($d$ is a -non-square, so the denominators never vanish~\cite{bernsteinlange}). +including the completeness fact that makes it branch-free ($a=-1$ is a +square and $d$ a non-square in $\mathbb{F}_p$, so the denominators never +vanish~\cite{bernsteinlange}). At the apex, writing $\code{accept}(A,m,R,s)$ for ``the extracted verifier returns \code{ok}'', with $k$ the scalar produced by the hash oracle $H(R,A,m)$ and no properties assumed of $H$, the byte-level tier @@ -287,7 +288,7 @@ Operator/consumer tooling and a twelve-lecture course: underlying proof corpora are in the \code{saymrwulf/*-ed25519-verified} repositories; every claim in this paper is re-checkable from these artifacts.} with eight leaves: one attestation per fork from each of two -full replay runs ($\approx$64 Lean files and $\approx$1{,}800\,s per +full replay runs (58--64 Lean files and $\approx$1{,}800\,s per fork, under hard memory caps and core pinning). In the second run all four forks reported 16/16 certificates proven with boundary-exact cones, pinned to exact commits. The first run is deliberately still in the log: its audit step @@ -328,9 +329,11 @@ lemma file) are byte-identical across all four; extraction-facing proof scripts diverge sharply where the forks' code or the extractor's naming differs (e.g., 215 changed lines for the byte-parser proofs on the two forks whose extraction produces a closure-based loader; 121 lines for -the signature-glue proofs on the same-crate fork; zero lines between -structurally identical forks). Per-target verification, in other words, -is doing measurable work exactly where the targets actually differ. +the signature-glue proofs on the same-crate fork; 27 lines---all +annotation---between the two structurally closest forks, documenting the +one fork's \code{black\_box} optimization barrier). Per-target +verification, in other words, is doing measurable work exactly where the +targets actually differ. \section{Related work} \label{sec:related} diff --git a/provider/src/pacta_provider/web.py b/provider/src/pacta_provider/web.py index fd9c388..0c134ec 100644 --- a/provider/src/pacta_provider/web.py +++ b/provider/src/pacta_provider/web.py @@ -54,6 +54,20 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf self.send_header("Content-Length", str(len(paper_pdf))) self.end_headers() self.wfile.write(paper_pdf) + elif route == "/log-public-key": + # TOFU mitigation depends on the key being published in two + # independent locations; this is the site's copy (the mirror + # carries the other). Serving only a fingerprint would not do. + key_path = Path(log.log_dir) / "provider.ed25519.pub" + if not key_path.is_file(): + self._send(404, {"error": "log public key not present in this log directory"}) + return + body = key_path.read_bytes() + self.send_response(200) + self.send_header("Content-Type", "text/plain; charset=utf-8") + self.send_header("Content-Length", str(len(body))) + self.end_headers() + self.wfile.write(body) elif route == "/healthz": self._send(200, {"ok": True, "tree_size": len(log.entries())}) elif route == f"/{API_VERSION}/metadata": @@ -124,6 +138,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf "endpoints": [ f"{base}/docs", f"{base}/paper", + f"{base}/log-public-key", f"{base}/healthz", f"{base}/{API_VERSION}/metadata", f"{base}/{API_VERSION}/sth", diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index c4867ed..fc0e8a7 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -164,9 +164,9 @@ library, plus optionally the whole mirror. Nothing else.

#ArtifactWhat it isWhere 1provider.ed25519.pub The trust anchor. The provider's public key — the only thing you -take on trust, once. Compare the copy here with the copy in the GitHub mirror; they +take on trust, once. Fetch it from BOTH independent locations and compare; the copies must be identical. -mirror +this site · mirror 2<library>.attestation.json The claim. Which repo, which exact git commit, which theorems, which observed axiom cones, what machine protection — signed by the provider. diff --git a/tests/test_web_and_witness.py b/tests/test_web_and_witness.py index 96d74ab..f3281bf 100644 --- a/tests/test_web_and_witness.py +++ b/tests/test_web_and_witness.py @@ -59,6 +59,12 @@ def test_web_endpoints_and_online_proof_roundtrip(tmp_path): with urllib.request.urlopen(base + "/paper", timeout=10) as r: assert r.headers["Content-Type"] == "application/pdf" assert r.read(5) == b"%PDF-" + # the site's copy of the trust anchor (TOFU: two independent locations) + import shutil + + shutil.copy2(tmp_path / "k.pub", tmp_path / "log" / "provider.ed25519.pub") + with urllib.request.urlopen(base + "/log-public-key", timeout=10) as r: + assert r.read() == (tmp_path / "k.pub").read_bytes() finally: server.shutdown()