# Modèle de sécurité

> Ce qu’établit une preuve, ce qu’elle suppose, ce qu’un vérificateur doit détenir lui-même, le code sur lequel repose la solidité, et les limites de la version 1.0.0.

## Ce qu’établit une preuve

Une preuve dont la vérification réussit établit que le programme d’une identité donnée, lancé à son pc d’entrée sur son image, avec l’entrée publique dans sa fenêtre d’entrée et des données auxiliaires (*advice*) choisies par le prouveur, s’exécute instruction par instruction jusqu’à `EXIT` avec un statut donné, après avoir écrit un journal donné. Rien n’est affirmé au sujet des données auxiliaires. Rien n’est caché.

## Hypothèses

| Hypothèse | Où elle intervient |
| --- | --- |
| La solidité de connaissance (*knowledge soundness*) de Mercury et de KZG dans le modèle du groupe algébrique sous q-DLOG | chaque ouverture d’engagement |
| Poseidon2 comme oracle aléatoire pour Fiat–Shamir | chaque défi, dans la preuve de base et dans la récursion |
| Les hypothèses propres à Groth16 | le décideur, la dernière étape vers le contrat |
| Un contributeur honnête aux puissances de tau perpétuelles de PSE | la SRS sur laquelle repose chaque engagement |
| Un contributeur honnête par tour de la cérémonie de phase 2 du décideur | la clé du décideur |

BN254 offre environ 100 bits de sécurité. L’erreur statistique de chaque couche du protocole, des sumchecks et de l’ouverture groupée jusqu’aux arguments de mémoire et de lookup, est très en deçà : moins de `2^14/|Fr|` pour toute la passe GKR d’un circuit, moins de `2^−190` pour chaque canal de lookup, moins de `2^−220` pour chaque instance de Mercury.

## Ce qu’un vérificateur doit détenir lui-même

Deux valeurs, obtenues par un canal que le prouveur ne contrôle pas :

- **L’identité du programme.** Face à une identité fournie par le prouveur, une preuve montre seulement qu’un programme quelconque s’est exécuté.
- **Le condensé SRS de la cérémonie.** Une clé se charge sous le condensé que donnent ses propres points, quel qu’il soit : une clé construite sur un `τ` connu n’est donc refusée que par cette comparaison.

La clé de vérification elle-même peut provenir de n’importe qui. Son chargement recalcule l’identité et le condensé SRS à partir de son propre contenu et exige que ses circuits soient ceux du registre du vérificateur : l’identité lie le programme, le registre lie les circuits. L’outil en ligne de commande `verifier` ne compare que l’identité, et prend le condensé SRS dans la clé; `host::verify` ne compare ni l’un ni l’autre, et laisse aussi à son appelant le soin de vérifier l’entrée, le journal et le statut de sortie de l’énoncé.

## Code de confiance

La solidité relève du seul vérificateur. Elle repose sur `constants`, `field`, `curve`, `transcript`, `poly`, `sumcheck`, `pcs-verify`, `pcs`, `gkr-verify`, `verifier-core`, `verifier`, et `constraints`, car les circuits font partie de l’énoncé et une porte manquante est un défaut de solidité. Le calcul d’une identité à partir d’un ELF fait aussi confiance à `loader`, `isa` et `program`. La dernière étape vers la chaîne ajoute les programmes de récursion, `groth16`, le circuit du décideur et le contrat.

Le prouveur, l’émulateur, les constructeurs de trace et la moitié du SDK hôte consacrée à la preuve ne bénéficient d’**aucune confiance**. Le prouveur ne valide rien; une entrée erronée coûte à un prouveur honnête une preuve qui échoue, et un prouveur malhonnête n’exécute de toute façon rien de ce code.

## Ni temps constant, ni divulgation nulle de connaissance

Rien dans le code n’est à temps constant : les réductions, les exponentiations, les additions de points et les échelles scalaires bifurquent selon leurs opérandes. C’est sans conséquence ici, car aucune preuve n’est à divulgation nulle de connaissance : la génération de preuves ne garde donc rien de secret. Le seul secret que manipule le code est le facteur d’un contributeur à la cérémonie du décideur, qui passe par la même échelle à temps variable; effectuez les contributions sur une machine que vous contrôlez.

## Limites de la v1.0.0

| Limite | Détail |
| --- | --- |
| Pas de divulgation nulle de connaissance | aucun aveuglement dans Mercury, dans GKR ni dans le décideur |
| Données auxiliaires non liées | un programme invité les vérifie par rapport à quelque chose qu’une preuve lie |
| Valeurs publiques | au plus 16 380 octets chacun pour l’entrée et le journal |
| `sc.w` réussit toujours | le seul écart par rapport à la sémantique de RV32IMAC; il n’y a pas d’état de réservation |
| Les déroutements (*traps*) ne sont pas prouvables | un accès non aligné, un accès hors de la mémoire projetée, `ebreak` ou un pc sans instruction termine l’exécution sans preuve |
| Le code est statique | le flux d’instructions est l’image décodée au chargement; un seul mot indécodable dans le code exécutable entraîne le refus du programme |
| Taille du code | `.text` dans la portée d’une table décodée, soit 7,94 MiB à `2^22`; l’image dans la limite de 4 MiB par défaut |
| Longueur d’exécution | `2^36 − 1` cycles |
| Les délégations forment un ensemble fixe | six au format de base; une délégation prouve une étape de sa fonction, et la composition des étapes, dont la validation des points de courbe, relève du code appelant |
| Mémoire du prouveur | déterminée par les shards en cours de traitement : le bloc mesuré a culminé à 174 GiB |
| Témoins de bloc | le validateur sans état reçoit son entrée d’un producteur de témoins externe |
| La clé du décideur | une par forme de racine, et digne de confiance seulement dans la mesure où sa cérémonie l’est; la clé de développement est falsifiable |
| Coût sur la chaîne | environ 3,6 M gas pour le bloc mesuré |

## Ce que change la prochaine version

Chacune des hypothèses ci-dessus qui fait intervenir BN254, de q-DLOG et du couplage jusqu’à Groth16, tombe face à un ordinateur quantique suffisamment grand. La [trajectoire de la v2.0.0](https://apogee.gweb3networks.com/docs/quantum-leap) est un cœur de preuve dont la solidité repose plutôt sur des problèmes de réseaux.

Pour la vue d’un auditeur sur le même modèle, crate par crate et argument par argument : [Guide d’audit](https://apogee.gweb3networks.com/docs/auditors), [Carte de solidité](https://apogee.gweb3networks.com/docs/auditors/soundness-map).