Summary by Michele Orrù
Summary by Vivek Arte:
NOTES:
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.