Assurance
What Pollis checks about its own code, and what those checks found.
The artifacts page covers the transparency log and the commands that check a download.
1 · Independent rebuild of every release
After each release, a workflow rebuilds the Linux AppImage payload from the public source at that tag, on a clean runner, and asserts that the hash it gets is the hash already recorded in the public transparency log. It uses no Pollis secrets, so anyone can fork it and run the same check, and it trusts one pinned ML-DSA-44 key.
The verdict used to live only in a job log and a CI artifact that expires after 90 days. This is the durable record.
Loading rebuild verdicts…
It covers the Linux AppImage payload only. The .deb, .rpm,
macOS and Windows builds have published-bytes-match and build provenance, but nothing re-derives them
from source yet.
Reproduction needs the published build recipe as well as the source, because one build-time value is compiled in. Without the recipe a third party can still prove log inclusion, but not bit-for-bit reproduction.
Three releases were never checked. The rebuild runs only when the release workflow succeeds, so v1.9.0, v1.9.1 and v1.10.0 have no verdict. They are in the table, marked as unchecked.
Some historical red runs were not real failures. Before commit
564353ae (16 August 2026) the workflow could report "did not reproduce" for a release
not yet published to the log: the check exited cleanly over an empty artifact set, so the wait loop
stopped at once and compared the rebuild against nothing. v1.9.4 and v1.9.5 failed this way; both
reproduce byte-identically. The red runs stay in the table.
v1.9.3 reproduces. Its 13 August rebuild did not, and went unexplained. The same
check re-run on 17 August (same tag, same source) landed on the CI machine image the release had used
and produced a payload byte-identical to the one in the log
(07bccca8…,
run 32036282718).
Why the August run differed. An AppImage is not purely a function of our source: the
bundler copies system libraries from the build machine into the bundle. GitHub rebuilds the image
behind its ubuntu-22.04 label every few weeks and rolls it out gradually, so the release
build and its rebuild, 36 minutes apart, ran on different images and seven bundled libraries
(Kerberos, SQLite, systemd, udev) differed. The only change in code built from Pollis source was the
order of a list of content hashes in the executable, which a compile-time dependency emits in
filesystem order and which carries no meaning.
The August run stays in the table, still red, because it could not make the comparison it reported
on. The workflow now compares the machine image the release recorded with its own and reports one of
did not reproduce, build environment drifted or no recorded recipe. All
three fail, since an inconclusive rebuild is not a pass; only the first is a claim about the shipped
binary. The write-up, with the byte evidence, is in
docs/reproducible-builds-residuals.md.
2 · Machine-checked correctness
Pollis promises that messages work: delivery to every current member, decryption, offline and online cycles, reconnects. Where that promise can break is in a few small, pure decision functions: when a delivery cursor may advance, when a commit may be accepted at an epoch, when old data may be deleted. Those are checked by machine.
TLA+ — the design
TLC checks two specifications on every relevant pull request, enumerating every reachable state of each model.
| Spec | Checks | Model bound | States | Result |
|---|---|---|---|---|
CommitLog |
OnePerEpoch, Gapless, OpeningClosesTheHead,
NoForeignAdopt, LineageMonotone
|
3 clients, max 2 commits, max epoch 3 | 72,228 distinct depth 13 |
all hold |
Delivery |
NoLossForCurrentMember, CursorMonotone,
AcceptedLossesOnly, CursorLeqClock
|
2 devices, max 3 messages, max epoch 2 | 130,484 distinct depth 19 |
all hold |
A passing check means nothing if the invariant can no longer fail, so three deliberately broken
variants run alongside and each must produce a counterexample.
Dropping the commit-log head guard violates OnePerEpoch; dropping the migration
compare-and-swap violates OpeningClosesTheHead; guarding retention on the
fastest member rather than the slowest violates NoLossForCurrentMember. If any of
those ever passes cleanly, the gate fails.
Kani — the actual Rust
TLA+ checks the design, not the shipped code. 35 Kani harnesses (19 proofs, 16 teeth) run bounded model checking over the real Rust functions: the delivery watermark, the rejoin gate that keeps a revoked device out of the tree, own-commit canonicalization, gap detection, the Delivery Service's head arithmetic, and the retention floor. Each proof is paired with a mutant that Kani must refute, such as an off-by-one in the watermark, a fail-open rejoin gate, or a retention floor that adds slack instead of subtracting it.
Every run publishes a summary and a downloadable artifact: TLA+ runs · Kani runs · design doc · the specs themselves.
Both are bounded. TLC checks a small model (three clients, a few epochs) and Kani checks small input domains. A bug that only appears at larger scale is outside both. Exhaustive over a small space is stronger than sampling a large one, but it is not a proof about the running system.
They cover the decision functions, not the program. The proofs range over pure functions extracted for the purpose. Database calls, the network, the MLS library and the UI are covered by ordinary tests and a nightly fuzzing soak, not by proofs.
One invariant has no machine-checked proof: that the test schema equals the production schema. A mechanical equality check enforces it instead, as the design doc notes.
3 · Supply chain
Pollis's Rust lockfile resolves to 1,094 crates. Two gates run on every pull request
and every push to main, both against pinned tool versions
(cargo-deny 0.19.9, cargo-vet 0.10.2) so the gate itself does not drift.
cargo-deny — advisories, licences, sources
-
Advisories. Any RustSec advisory against the graph fails the build unless it has an
exemption naming its
RUSTSEC-id with a written reason; there is no blanket suppression. There are 29 exemptions. Twenty-one are unmaintained-crate notices with no vulnerability (ten are the GTK3 bindings Tauri's WebKit backend requires; no GTK4 Tauri backend exists). Eight are real vulnerabilities with no reachable fix, listed below. - Licences. An allow-list of 17 identifiers, each one actually present in the graph. MPL-2.0 is permitted with the reasoning written down (file-level copyleft, no reach across a module boundary).
-
Sources.
crates.ioonly, plus exactly one git dependency: anopenmlscommit, needed for the post-quantum MLS ciphersuite that no published release carries yet. The revision is pinned inCargo.toml, so it cannot follow upstreammain.
| Advisory | Crate | Why it is exempt |
|---|---|---|
RUSTSEC-2023-0071 | rsa |
No upstream fix. Transitive via LiveKit's JWT library; the decryption-timing oracle is not reachable on the signing path we use. |
RUSTSEC-2026-0049RUSTSEC-2026-0098RUSTSEC-2026-0099RUSTSEC-2026-0104 |
rustls-webpki 0.101 / 0.102 |
Certificate-validation issues fixed only on the 0.103 line, which our own direct TLS already uses. The old lines are pinned by LiveKit and libSQL upstream; waiting on their rustls bump. |
RUSTSEC-2026-0258 | h2 0.3 |
Empty-DATA-frame denial of service, fixed only on the 0.4 line with no 0.3 backport. Reachable only as libSQL's outbound client to Turso, never on the Delivery Service's inbound listener, which is hyper 1.9 and does not use it. |
RUSTSEC-2026-0194RUSTSEC-2026-0195 |
quick-xml |
Every vulnerable instance is build-time code generation or dev-only. No runtime path parses untrusted XML. |
cargo-vet — review provenance
cargo-vet records who has reviewed each crate version. Pollis imports 517 audits from six
organisations that publish theirs: Mozilla (206), Google (117), Bytecode Alliance (84), ISRG (52), Zcash
(42) and Embark (16). Another 35 crates are trusted by publisher identity. The rest sit in an exemption
baseline.
Pollis has audited no crates itself. supply-chain/audits.toml is empty.
867 exemption entries cover 725 crates, essentially the dependency graph as it stood when the gate was
switched on. The gate is a ratchet: no new or bumped crate gets in without a reviewable change to that
file. It does not mean every dependency has been reviewed.
Existing duplicate versions are allow-listed, and wildcards only warn. A large native tree carries transitive duplicates we do not control. The ones present today sit in a generated skip list; a new duplicate fails the check. Wildcard version requirements are logged but do not block.
There is no scheduled re-scan, and no bot updates Rust or JavaScript dependencies
(Dependabot bumps GitHub Actions pins only). Advisories are checked on pull requests and pushes to
main, so a new advisory against an unchanged dependency waits for the next such run.
Neither gate covers JavaScript or vendored C/C++. The renderer's pnpm
tree is in the per-release SBOM but not vetted, and C and C++ compiled in build scripts (notably the
WebRTC crates) is in neither.
Read the policy directly:
deny.toml ·
supply-chain/ ·
gate runs.
4 · Signing keys, custody and rotation
Every claim on the artifacts page reduces to one pinned
ML-DSA-44 key, key id 6cbd4b2aed5c4bf1. This section covers who holds it, what happens if
it is stolen, and its history.
| Key | Signs | Custody |
|---|---|---|
| Transparency-log signing key ML-DSA-44 |
Signed tree heads for all three logs | A GitHub Actions secret, backed up in a secrets manager |
| Offline root key ML-DSA-44 |
Nothing but key-set statements: "these keys may sign these logs, until this date" | Offline. Not in CI, the secrets manager or the repository |
| Release code-signing | macOS (Apple Developer ID) and Windows (Azure Trusted Signing) installers | GitHub Actions secrets |
| Sigstore identity | cosign signatures and SLSA provenance | No held key: a short-lived certificate bound to the release workflow's OIDC identity |
The key has been rotated once. In August 2026 the log signing key was replaced with fresh material and all three trees were republished from source data under new domain-separation contexts. The previous key had been derived from the same 32-byte seed as its Ed25519 predecessor, so the earlier post-quantum migration had changed the format but not the secret. A rehearsal against production, with the old key still installed, caught two bugs that would each have made the rotation a silent no-op. The result was verified from a machine that had not performed the rotation.
A compromised signing key does not need a new build. Clients pin a key set authorised by the offline root, so the response is to sign and publish a new key set without the compromised key; no client update is needed. The runbook drops a compromised key outright rather than giving it a short expiry, since an attacker who can delay a client's fetch keeps the key alive that long. It also says to act on suspicion, without waiting for proof.
GitHub Actions is inside the publishing trust boundary, as the whitepaper states. The log signing key is an Actions secret and the trees are built and signed in CI, so a compromise there could sign a tree. The post-publish self-audit and the equivocation tripwire detect that afterwards; they cannot prevent it. The same holds for the release-signing keys. Pollis operates the only log, which is why the verifier is released: a third party can audit without asking us for anything.
The rotation had no overlap window. The custody design calls for at least 90 days with both keys pinned; the actual rotation skipped it. An auditor holding cached pre-rotation tree heads sees the change as equivocation and has to re-pin from the announcement.
Root compromise has no in-band recovery. If the offline root is lost or stolen, the fix does require a client release: mint a new root, ship a build pinning both, wait out the overlap, then publish under the new root alone.
The pinned key is copied by hand into the Rust core, the verifier, this website, two
workflows, the key-set statement and several documents. A stale deployed copy once showed every visitor
a false tamper alarm. CI now checks that the copies agree on every pull request
(scripts/check-pinned-log-key.py), and a separate workflow checks that the deployed site
pins the same key, but nothing stops the copies being edited by hand in the first place.
Compromise runbook · Custody & rotation design · The signed key set.
5 · Security reviews
Pollis has had two full adversarial security reviews, both by teams of AI agents working read-only in parallel, each required to cite the source line behind every finding. That is not the same as a paid human audit firm. Findings and fixes are published in full.
| Review | Scope | Findings | Status |
|---|---|---|---|
| September 2026, first commit 521b551 |
Static review of the client, Delivery Service and release pipeline, plus an OWASP ZAP run (~47,000 requests) against a locally built Delivery Service | 9 High, 13 Medium, 1 Low | all fixed #1091, #1102, #1113 |
| 18 September 2026, second v1.13.0, commit 62db0805 |
Six parallel audits across the MLS client, Delivery Service authorization, enrollment and key material, and the supply chain, plus two documentation-versus-code sweeps | 2 Critical, 5 High, 8 Medium, 4 Low | fixed #1161 |
Every fixed finding ships with a regression test confirmed to fail against the pre-fix code. Two of the second review's findings were addressed differently from the audit's suggestion, with the reasoning on #1161. One, two identity columns (who reacted with which emoji, who pinned a message) stored in the clear, is an accepted exposure rather than a fixed defect: no document claims they are protected, and whether to seal them is an open product decision. The repository-settings finding (no required checks, unprotected release tags) was closed separately on #1101.
Both reviews were mostly static. Live testing of TLS configuration, signed-request replay, adversarial two-client MLS behaviour, updater tampering and the voice SFU has been scoped but not run by an independent human tester. An independent human audit is welcome, and the whitepaper is written for that reader.
6 · Operations
Live service status, running version and daily uptime are published at status.pollis.com. What happens if the one person operating Pollis stops, and how to tell a stalled transparency log from a withheld one, is on if the operator stops. Legal demands for user data and the warrant canary are on legal requests.
Reporting a vulnerability
Report privately through a
GitHub security advisory, not a public issue. The machine-readable
policy is at /.well-known/security.txt and the
terms are in the
disclosure policy.
Pollis is source-available, not open source: PolyForm Noncommercial 1.0.0. You may read, build, audit and modify it for noncommercial purposes; commercial use needs a separate licence. Auditing the code and publishing what you find is permitted.