Proposal: Halo2 Soundness Bug Examples

[teddav]

General Grant Proposal

• Project: Halo2 Soundness Bug Examples #5

Project Overview 📄

Overview

Write examples of Halo2 circuits presenting soundness bugs.
The goal is to educate users on recognizing and understanding Halo2 circuit bugs.

Team 👥

A one man team :)

• Name: David
• Telegram: teddav
• Discord: teddav

Team's experience

• Audited Summa (through yAcademy) (cc Alex Jin Enrico)
• Merged a (tiny) PR on Halo2 feat: MockProver cell override halo2#352
• And found a bug in the library:
  • Possible bug in Lookup-any API halo2#335
  • https://github.com/teddav/poc-underconstrained-halo2
• Created an easy to use Halo2 template repo: https://github.com/teddav/halo2-starter

Development Roadmap 🔩

Overview

• Total Estimated Duration: 6 weeks
• Total Estimated Working Hours: XXX hr
• Full-time equivalent (FTE): 0.5
• Expected Start Date: July 24th 2024
• Expected End Date: September 4th 2024

For each vulnerability, the process will be:

• explain the high level vulnerability: causes and consequences (real world examples)
• write the vulnerable circuit
• show the exploit
• fix it

Milestone 1: High level overview + underconstrained

• Estimated Duration: 2 weeks
• FTE: 0.5
• Estimated delivery date: August 7th 2024

• Start with a blogpost
  • Halo2 global explainer
  • explanation of soundness
  • high level overview of circuit vulnerabilities
• Write examples of the most common vulnerability: underconstrained circuits

Milestone 2: Circuits, circuits, circuits...

• Estimated Duration: 2 weeks
• FTE: 0.5
• Estimated delivery date: August 21st 2024

1. Write more vulnerable circuits:
   see https://github.com/0xPARC/zk-bug-tracker#common-vulnerabilities-header

• more underconstrained:
  • "Nondeterministic Circuits"
  • “Assigned but not Constrained”
• overflow/underflow

2. Research other kind of vulnerabilities

Milestone 3: Tools + finish

• Estimated Duration: 2 weeks
• FTE: 0.5
• Estimated delivery date: September 4th 2024

1. Setup automated tools
   Which automated tools exist? How to use them to detect circuit vulnerabilities?
   These tools could be a great help to new developers (and more advanced as well)
2. Write final blogpost

[miha-stopar]

Looks cool!