Breakout Session: ZK Protocol Security Analysis & Proofs of Correctness

Summary by Michele Orrù

Summary by Vivek Arte:


How important are sanity checks?

  • check for unused variables
  • check for inconsistencies (between spec and code)
  • prove security in GGM? (more for pairing based SNARKs)

How hard is it to build automated proofs for these analyses?

  • CryptoVerif exists
  • but we can manage with something simpler for these types of proofs?
  • maybe just via information flow, etc?

for proofs, have multiple people check it independently (and from scratch)! - would help avoid simple errors

Think from the point of view of a regulator?

  • even things related to composability?
  • what NIST did for PQC
  • defined different security levels - IND-CCA bits of security : level 1,3,5
  • the assumptions used don’t make any difference - the people have to put forward how they meet these levels
  • have a competition - more people will look closely at the papers then.

proVerif has a GGM analyzer but it doesn’t satisfy the win condition needed for SNARKs?

  • is it something to improve? Who maintains the code?

composability issues??

how do you incentivize people to find bugs? bug bounties don’t work.

  • maybe something like a stackoverflow/wiki to explain papers?
  • something like complexityzoo?

have dual implementations? as a fallback if the less tested portion fails?

Hydra? - 3 different ways, reject if they don’t match up?

come up with a checklist for regulators and implementers?

go from what could go wrong to prescriptive guidelines for what should be done.