ZKP15.2 Formal Methods in ZK (Part I)

ZKP学习笔记

ZK-Learning MOOC课程笔记

Circuits Workflow
- Source Code: Witness Generation and Constraints
- Witness Generation and Constraints should (generally) be equivalent!
What is Equivalence
- Every input-output of P must satisfy C
- Every (x,y) which satisfies C must be an input-out pair of P
Equivalence Violations
- Underconstrained Bugs: Verifier can accept bad inputs/ outputs
A Taxonomy of ZK Bugs
Unconstrained Signals
- Corresponds to signals whose constraints always evaluate to true, accepting everything
- Example: Underconstrained Output
  - Error: for (var i = 0; i< n, i++)
  - No constrains over the last element of output
  - Attacker can pass in any value for out 2
Unsafe Component Usage
- Sub-circuits often assume constraints are placed on inputs and outputs
- Corresponds to cases where the use of a sub-circuit does not follow
- Example: Under-Constrained Sub-Circuit Output
  - Missing constraint lt.out === 0
  - Without the missing constraint, attackers can withdraw more funds than they have
Constraint/Computation Discrepancy
- Not all computation can be directly expressed as a constraint
- Corresponds to constraints that do not capture a computation’s semantics
- Example: No Zero Inverse
  - Accepts arbitrary out when a and b are 0!
Circuit Dependence Graphs (CDG)
- Goal: Identify discrepancies between computation and constraints
- Data dependence <–
- Constrain ===
- CDG Example