Lie to Me: Menemukan Bug di Toolchain ZK DSL dengan Injeksi Witness Adversarial

Toolchain bahasa khusus domain zero-knowledge (ZK DSL) mengompilasi program menjadi sistem kendala dan menghasilkan witness untuk pembuktian kriptografis. Syarat kebenaran utamanya adalah **soundness**: kendala yang diberlakukan harus setidaknya sekuat semantik program sumber. Jika bug toolchain melemahkan kendala, prover dapat menghasilkan bukti untuk eksekusi yang tidak valid. Bug soundness semacam ini terkenal sulit dideteksi karena tidak terlihat oleh pengujian eksekusi valid: setiap eksekusi valid tetap berperilaku benar, sehingga uji diferensial dan regresi pada input valid tetap lulus.

Makalah ini memperkenalkan **Liezz**, kerangka pengujian yang menghasilkan program ZK DSL dan mengungkap bug soundness melalui *injeksi witness adversarial*. Wawasan kuncinya adalah toolchain yang benar harus menolak setiap witness yang tidak berkorespondensi dengan eksekusi valid. Liezz membangun witness tidak valid tersebut secara konstruktif dan memeriksa apakah toolchain menerimanya. Penerimaan berarti bug soundness.

Secara formal, untuk program deterministik $P$ dan dua penetapan input publik $x_1,x_2$ dengan output berbeda $y_1\ne y_2$, Liezz menyambung witness satu eksekusi dengan

Liezz diterapkan pada empat toolchain ZK DSL: **Circom, Corset, Gnark, dan Noir**. Evaluasi melaporkan **13 bug**, dengan **tujuh berdampak pada soundness**. Beberapa bug ini hanya dapat dijangkau melalui panggilan pustaka standar yang dihasilkan, yang menunjukkan nilai pembangkitan panggilan pustaka berparameter.

Hasil komparatif utamanya adalah, dengan anggaran pengujian yang sama, baseline eksekusi valid **tidak** mengungkap satu pun kegagalan soundness yang diungkap oleh witness tersuntik yang diterima. Dengan kata lain, injeksi witness adversarial menjangkau kegagalan yang sepenuhnya luput dari pengujian eksekusi valid. Hal ini konsisten dengan motivasi teoretisnya: bug soundness membiarkan semua eksekusi valid tetap benar, sehingga tidak terlihat oleh tes yang hanya menjalankan eksekusi valid.

Angka yang dilaporkan dapat diringkas sebagai:

| Metrik | Nilai |
|---|---|
| Toolchain yang didukung | 4 (Circom, Corset, Gnark, Noir) |
| Bug yang ditemukan | 13 |
| Bug berdampak soundness | 7 |
| Kegagalan soundness yang ditemukan baseline eksekusi valid | 0 |

Temuan bahwa beberapa bug memerlukan panggilan pustaka standar yang dihasilkan penting bagi praktisi: gadget pustaka mer