Pengujian dan Verifikasi Branch-and-Bound yang Efisien untuk zkVM

ZEBRA: Verifikasi Otomatis Zero-Knowledge Virtual Machine melalui Integer Interval Lattice dan Parallel Branch-and-Bound

Hideaki Takahashi; Suman Jana; Junfeng Yang· 2026· DOI 10.48550/arXiv.2609.15020

Masalah inti

Zero-knowledge virtual machine (zkVM) memungkinkan eksekusi terverifikasi program serbaguna dengan menerjemahkan semantik virtual machine menjadi batasan aljabar atas jejak eksekusi. Kebenaran batasan ini sangat kritis: satu batasan yang salah dapat menerima bukti palsu (under-constrained) atau menolak eksekusi yang valid (over-constrained). Pendekatan yang ada tidak memberikan jaminan yang berarti pada skala produksi: fuzzer dan unit test sering melewatkan bug, SMT solver kesulitan dengan ukuran dan sifat nonlinier batasan, dan theorem prover memerlukan upaya manual yang besar. Makalah ini menyajikan ZEBRA, kerangka kerja verifikasi dan deteksi bug yang otomatis penuh. Untuk program dan input tertentu, batasan harus menerima tepat satu jejak eksekusi yang valid—tidak lebih dan tidak kurang. Hal ini mereduksi verifikasi zkVM menjadi masalah kardinalitas himpunan solusi pada ruang jejak kanonik, di mana redundansi seperti null-row padding dan permutasi non-deterministik dihilangkan sebelum penghitungan. Untuk menghitung kardinalitas secara tractable, ZEBRA mengangkat analisis dari witness finite-field ke integer interval lattice, memanfaatkan sifat sparsitas struktural batasan zkVM

ZEBRA dievaluasi pada lima zkVM dunia nyata. Kerangka kerja ini menemukan 11 bug zero-day; 6 di antaranya telah dikonfirmasi secara independen dan 3 telah diperbaiki oleh pengembang. Dibandingkan dengan verifikasi berbasis SMT, ZEBRA 51,5x lebih cepat, memverifikasi 16,5 poin persentase lebih banyak instance, dan verifikasi rentangnya memberikan efisiensi hingga 63x dibandingkan verifikasi input tunggal yang berulang. Sifat sparsitas diukur pada lima zkVM: batasan hanya menggunakan 14,0% dari kapasitas konektivitas teoretisnya secara rata-rata. Sparsitas ini menjadi faktor kunci efisiensi ZEBRA. Pencarian parallel branch-and-bound berskala baik dengan jumlah core, dan propagasi interval mencapai batas yang ketat dengan galat aproksimasi yang terbatas. Tabel 1 merangkum perbandingan kinerja: | Metrik | ZEBRA | Berbasis SMT | |--------|-------|-----------| | Kecepatan | 51,5x lebih cepat | Baseline | | Instance terverifikasi | +16,5 pp | Baseline | | Efisiensi verifikasi rentang | hingga 63x | Baseline | Hasil ini menunjukkan bahwa ZEBRA menyediakan solusi praktis dan efektif untuk verifikasi zkVM pada skala produksi.

Zero-knowledge virtual machine (zkVM) memungkinkan eksekusi terverifikasi program serbaguna dengan menerjemahkan semantik virtual machine menjadi batasan aljabar atas jejak eksekusi. Kebenaran batasan ini sangat kritis: satu batasan yang salah dapat menerima bukti palsu (under-constrained) atau menolak eksekusi yang valid (over-constrained). Pendekatan yang ada tidak memberikan jaminan yang berarti pada skala produksi: fuzzer dan unit test sering melewatkan bug, SMT solver kesulitan dengan ukuran dan sifat nonlinier batasan, dan theorem prover memerlukan upaya manual yang besar.

Makalah ini menyajikan ZEBRA, kerangka kerja verifikasi dan deteksi bug yang otomatis penuh. Untuk program dan input tertentu, batasan harus menerima tepat satu jejak eksekusi yang valid—tidak lebih dan tidak kurang. Hal ini mereduksi verifikasi zkVM menjadi masalah kardinalitas himpunan solusi pada ruang jejak kanonik, di mana redundansi seperti null-row padding dan permutasi non-deterministik dihilangkan sebelum penghitungan. Untuk menghitung kardinalitas secara tractable, ZEBRA mengangkat analisis dari witness finite-field ke integer interval lattice, memanfaatkan sifat sparsitas struktural batasan zkVM: pada 5 zkVM dunia nyata, batasan hanya menggunakan 14,0% dari kapasitas konektivitas teoretisnya secara rata-rata. Sparsitas ini memungkinkan propagasi interval yang ketat dengan galat aproksimasi yang terbatas. ZEBRA melakukan pencarian parallel branch-and-bound yang menghasilkan counter-example konkret atau mensertifikasi tidak adanya pelanggaran dalam wilayah terbatas.

Pendekatan ZEBRA mengatasi keterbatasan metode verifikasi yang ada. Fuzzer dan unit test tidak memadai karena tidak dapat mengeksplorasi ruang batasan secara menyeluruh. SMT solver kesulitan dengan ukuran dan sifat nonlinier batasan zkVM, sering kali timeout atau gagal memverifikasi. Theorem prover memerlukan upaya manual dan keahlian yang besar, sehingga tidak praktis untuk integrasi berkelanjutan. Inovasi kunci ZEBRA adalah reduksi verifikasi zkVM menjadi masalah kardinalitas himpunan solusi pada ruang jejak kanonik, dikombinasikan dengan penggunaan integer interval lattice untuk menghitung kardinalitas secara tractable. Sparsitas batasan zkVM (14,0% pemanfaatan konektivitas) adalah sifat struktural yang dimanfaatkan ZEBRA untuk mencapai propagasi interval yang ketat. Pencarian parallel branch-and-bound memastikan skalabilitas. Penemuan 11 bug zero-day, dengan 6 dikonfirmasi secara independen dan 3 diperbaiki, menyoroti dampak praktis ZEBRA. Percepatan 51,5x dibandingkan verifikasi berbasis SMT dan efisiensi 63x untuk verifikasi rentang membuat ZEBRA cocok untuk verifikasi skala produksi. Pekerjaan selanjutnya dapat memperluas ZEBRA ke sistem batasan lain dan mengoptimalkan lebih lanjut pencarian branch-and-bound. Sebagai kesimpulan, ZEBRA menyediakan kerangka kerja otomatis penuh, efisien, dan efektif untuk memverifikasi zkVM, menjawab kebutuhan kritis dalam keamanan dan kebenaran zero-knowledge proof.

Praktisi dan peneliti ilmu komputer

Membuka konten member…