# 安全模型

> 证明确立什么、依赖哪些假设、验证者必须自己持有什么、可靠性依赖哪些代码，以及 1.0.0 版的限制。

## 证明确立什么

一份通过验证的证明确立的是：具有给定身份的程序，在其映像上从入口 pc 启动，输入窗口中存放该公开输入，并带有某份由证明者选择的证明者提示（advice），逐条指令执行直至以给定状态调用 `EXIT`，且已写出给定的公开输出（journal）。对证明者提示不作任何断言。没有任何东西被隐藏。

## 假设

| 假设 | 在何处起作用 |
| --- | --- |
| Mercury 与 KZG 在代数群模型中、q-DLOG 假设下的知识可靠性 | 每一次承诺打开 |
| 在 Fiat–Shamir 中把 Poseidon2 视为随机预言机 | 每个挑战，包括基础证明和递归中的挑战 |
| Groth16 自身的假设 | 判定器，即通往合约的最后一步 |
| PSE 的 perpetual powers of tau 有一位诚实的贡献者 | 每个承诺所依据的 SRS |
| 判定器第二阶段仪式的每一轮都有一位诚实的贡献者 | 判定器的密钥 |

BN254 提供约 100 位的安全性。每一层协议的统计误差，从求和校验（sumcheck）和批量打开，到内存论证与查找（lookup）论证，都远低于此：一个电路的整个 GKR 过程低于 `2^14/|Fr|`，每个查找通道低于 `2^−190`，每个 Mercury 实例低于 `2^−220`。

## 验证者必须自己持有的值

两个值，都要取自证明者无法控制的渠道：

- **程序身份。** 如果对照的是证明者提供的身份，证明只能说明有某个程序运行过。
- **仪式的 SRS 摘要。** 不论密钥自身的点给出什么摘要，密钥都会按这个摘要加载，所以基于已知 `τ` 构建的密钥，只有通过这项比对才会被拒绝。

验证密钥本身可以来自任何人。加载它时会根据其自身内容重新计算程序身份和 SRS 摘要，并要求其中的电路与验证者的注册表一致：程序身份绑定程序，注册表绑定电路。`verifier` 命令行工具只比较程序身份，SRS 摘要则取自密钥；`host::verify` 两者都不比较，并且把检查陈述中的输入、公开输出和退出状态的工作也留给调用方。

## 受信任的代码

可靠性只取决于验证者。它依赖于 `constants`、`field`、`curve`、`transcript`、`poly`、`sumcheck`、`pcs-verify`、`pcs`、`gkr-verify`、`verifier-core`、`verifier`，以及 `constraints`，因为电路是陈述的一部分，缺失一个门就是可靠性漏洞。从 ELF 计算程序身份还要信任 `loader`、`isa` 和 `program`。上链的最后一步又加入了递归程序、`groth16`、判定器的电路和合约。

证明者、模拟器、执行轨迹构建器，以及宿主程序（host）SDK 中负责证明的一半，都是**不受信任的**。证明者不做任何校验；错误的输入只会让诚实的证明者得到一份无法通过验证的证明，而作弊的证明者本来就不会运行这些代码。

## 不是常数时间的，也不是零知识的

代码中没有任何部分是常数时间的：约简、幂运算、点加和标量阶梯都会根据操作数分支。这在这里无害，因为没有任何证明是零知识的，证明过程不保有任何秘密。代码处理的唯一秘密，是判定器仪式贡献者的因子，它经过的是同一个非常数时间的阶梯；请在你自己控制的机器上进行贡献。

## v1.0.0 的限制

| 限制 | 说明 |
| --- | --- |
| 不是零知识的 | Mercury、GKR 和判定器中都没有盲化 |
| 证明者提示不受绑定 | 客户程序（guest）要将它与证明所绑定的某样东西进行核对 |
| 公开值 | 输入和公开输出各至多 16,380 字节 |
| `sc.w` 总是成功 | 这是与 RV32IMAC 语义唯一的偏差；没有保留（reservation）状态 |
| 陷入（trap）不可证明 | 未对齐的访问、对映射内存之外的访问、`ebreak`，或者 pc 处没有指令，都会使执行终止，且不产生证明 |
| 代码是静态的 | 指令流就是加载时解码的映像；可执行代码中只要有一个无法解码的字，程序就会被拒绝 |
| 代码大小 | `.text` 须在解码表的覆盖范围之内，`2^22` 时为 7.94 MiB；映像默认不超过 4 MiB |
| 执行长度 | `2^36 − 1` 个周期 |
| 委托集合是固定的 | 基础格式中有六种；一个委托证明其函数的一步，把各步组合起来（包括校验曲线点）是调用代码的责任 |
| 证明者内存 | 由同时处理中的分片决定：实测区块的峰值为 174 GiB |
| 区块见证 | 无状态校验器的输入来自外部的见证生成方 |
| 判定器的密钥 | 每种根的形状一个，其可信程度取决于它的仪式；开发用密钥是可伪造的 |
| 链上成本 | 实测区块约 3.6M gas |

## 下一个版本将改变什么

上面涉及 BN254 的每一个假设，从 q-DLOG、配对到 Groth16，都会被一台足够大的量子计算机攻破。[v2.0.0 的演进方向](https://apogee.gweb3networks.com/docs/quantum-leap)是一个可靠性改为建立在格问题之上的证明核心。

从审计者的视角，逐个 crate、逐个论证地审视同一个模型：[审计指南](https://apogee.gweb3networks.com/docs/auditors)、[可靠性地图](https://apogee.gweb3networks.com/docs/auditors/soundness-map)。