# Sicherheitsmodell

> Was ein Beweis begründet, was er voraussetzt, was ein Verifier selbst besitzen muss, auf welchem Code die Soundness beruht und die Grenzen von Version 1.0.0.

## Was ein Beweis begründet

Ein Beweis, der die Verifikation besteht, begründet, dass das Programm einer gegebenen Identität, gestartet an seinem Einsprung-pc auf seinem Image, mit der öffentlichen Eingabe in seinem Eingabefenster und irgendwelchen vom Prover gewählten Hilfsdaten (Advice), Befehl für Befehl bis zu `EXIT` mit einem gegebenen Status ausgeführt wird und dabei ein gegebenes Journal geschrieben hat. Über die Hilfsdaten wird nichts behauptet. Nichts wird verborgen.

## Annahmen

| Annahme | Wo sie eingeht |
| --- | --- |
| Knowledge Soundness von Mercury und KZG im algebraischen Gruppenmodell unter q-DLOG | jede Öffnung eines Commitments |
| Poseidon2 als Random Oracle für Fiat–Shamir | jede Challenge, im Basisbeweis und in der Rekursion |
| Die eigenen Annahmen von Groth16 | der Decider, der letzte Schritt zum Contract |
| Ein ehrlicher Beitragender zu den Perpetual Powers of Tau der PSE | der SRS, auf dem jedes Commitment beruht |
| Ein ehrlicher Beitragender pro Runde der Phase-2-Zeremonie des Deciders | der Schlüssel des Deciders |

BN254 bietet etwa 100 Bit Sicherheit. Der statistische Fehler jeder Protokollschicht, von den Sumchecks und der gebündelten Öffnung bis zu den Speicher- und Lookup-Argumenten, liegt weit darunter: unter `2^14/|Fr|` für den gesamten GKR-Durchlauf eines Schaltkreises, unter `2^−190` für jeden Lookup-Kanal, unter `2^−220` für jede Mercury-Instanz.

## Was ein Verifier selbst besitzen muss

Zwei Werte, bezogen über einen Kanal, den der Prover nicht kontrolliert:

- **Die Programmidentität.** Gegenüber einer vom Prover gelieferten Identität zeigt ein Beweis nur, dass irgendein Programm gelaufen ist.
- **Der SRS-Digest der Zeremonie.** Ein Schlüssel wird unter jedem Digest geladen, den seine eigenen Punkte ergeben; ein Schlüssel, der über einem bekannten `τ` gebaut wurde, wird also nur durch diesen Vergleich zurückgewiesen.

Der Verifikationsschlüssel selbst darf von beliebiger Seite stammen. Beim Laden werden die Identität und der SRS-Digest aus seinem eigenen Inhalt neu berechnet, und seine Schaltkreise werden mit der Registry des Verifiers abgeglichen: Die Identität bindet das Programm, die Registry bindet die Schaltkreise. Das Kommandozeilenwerkzeug `verifier` vergleicht nur die Identität und entnimmt den SRS-Digest dem Schlüssel; `host::verify` vergleicht keines von beiden und überlässt es seinem Aufrufer, auch Eingabe, Journal und Exit-Status der Aussage zu prüfen.

## Vertrauenswürdiger Code

Die Soundness liegt allein beim Verifier. Sie beruht auf `constants`, `field`, `curve`, `transcript`, `poly`, `sumcheck`, `pcs-verify`, `pcs`, `gkr-verify`, `verifier-core`, `verifier` und `constraints`, weil die Schaltkreise Teil der Aussage sind und ein fehlendes Gate ein Soundness-Fehler ist. Das Berechnen einer Identität aus einem ELF vertraut außerdem `loader`, `isa` und `program`. Der letzte Schritt zur Chain fügt die Rekursionsprogramme, `groth16`, den Schaltkreis des Deciders und den Contract hinzu.

Dem Prover, dem Emulator, den Trace-Buildern und der beweisenden Hälfte des Host-SDK wird **nicht vertraut**. Der Prover validiert nichts; eine falsche Eingabe führt bei einem ehrlichen Prover zu einem Beweis, der fehlschlägt, und ein betrügerischer Prover führt diesen Code ohnehin nicht aus.

## Nicht in konstanter Zeit, nicht zero-knowledge

Nichts im Code läuft in konstanter Zeit: Reduktionen, Exponentiationen, Punktadditionen und Skalarleitern verzweigen abhängig von ihren Operanden. Das ist hier unschädlich, weil kein Beweis zero-knowledge ist und das Beweisen somit nichts geheim hält. Das einzige Geheimnis, mit dem der Code umgeht, ist der Faktor eines Beitragenden zur Zeremonie des Deciders, und er durchläuft dieselbe Leiter mit variabler Laufzeit; führen Sie Beiträge auf einer Maschine aus, die Sie kontrollieren.

## Grenzen von v1.0.0

| Grenze | Einzelheiten |
| --- | --- |
| Nicht zero-knowledge | keine Verblindung in Mercury, GKR oder dem Decider |
| Hilfsdaten sind ungebunden | ein Gastprogramm (Guest) prüft sie gegen etwas, das ein Beweis bindet |
| Öffentliche Werte | höchstens je 16.380 Byte Eingabe und Journal |
| `sc.w` gelingt immer | die einzige Abweichung von der Semantik von RV32IMAC; es gibt keinen Reservierungszustand |
| Traps sind nicht beweisbar | ein nicht ausgerichteter Zugriff, ein Zugriff außerhalb des gemappten Speichers, `ebreak` oder ein pc ohne Befehl beendet eine Ausführung ohne Beweis |
| Code ist statisch | der Befehlsstrom ist das beim Laden dekodierte Image; ein einziges nicht dekodierbares Wort im ausführbaren Code führt zur Zurückweisung des Programms |
| Codegröße | `.text` innerhalb der Reichweite einer dekodierten Tabelle, 7,94 MiB bei `2^22`; das Image standardmäßig innerhalb von 4 MiB |
| Ausführungslänge | `2^36 − 1` Zyklen |
| Delegationen bilden eine feste Menge | sechs im Basisformat; eine Delegation beweist einen Schritt ihrer Funktion, und das Zusammensetzen der Schritte, darunter die Validierung von Kurvenpunkten, ist Sache des aufrufenden Codes |
| Speicher des Provers | bestimmt durch die gleichzeitig bearbeiteten Shards: Der gemessene Block erreichte eine Spitze von 174 GiB |
| Block-Witnesses | der zustandslose Validator bezieht seine Eingabe von einem externen Witness-Erzeuger |
| Der Schlüssel des Deciders | einer pro Wurzelform und nur so vertrauenswürdig wie seine Zeremonie; der Entwicklungsschlüssel ist fälschbar |
| On-Chain-Kosten | etwa 3,6 Mio. gas für den gemessenen Block |

## Wohin die nächste Version das verschiebt

Jede der obigen Annahmen, die BN254 betrifft, von q-DLOG und dem Pairing bis zu Groth16, hält einem hinreichend großen Quantencomputer nicht stand. Die [Flugbahn zu v2.0.0](https://apogee.gweb3networks.com/docs/quantum-leap) führt zu einem Beweiskern, dessen Soundness stattdessen auf Gitterproblemen beruht.

Die Sicht eines Auditors auf dasselbe Modell, Crate für Crate und Argument für Argument: [Audit-Leitfaden](https://apogee.gweb3networks.com/docs/auditors), [Soundness-Karte](https://apogee.gweb3networks.com/docs/auditors/soundness-map).