Verifikasi Formal zk-SNARKs: Metode Bukti Memori

Dalam melakukan verifikasi formal terhadap sistem zk-SNARKs, pengolahan subsistem memori adalah tantangan kunci. Berbeda dengan mesin virtual tradisional, zkVM menggunakan tabel eksekusi dan tabel pendukung untuk merepresentasikan status memori, yang memerlukan metode verifikasi khusus.

Sistem memori zkWasm terdiri dari tabel eksekusi dan tabel memori. Tabel eksekusi mencatat proses eksekusi instruksi, sedangkan tabel memori menyimpan semua riwayat akses memori. Untuk menyederhanakan pengembangan, zkWasm menyediakan lapisan abstraksi, melalui dua fungsi alloc_memory_table_lookup_write_cell dan alloc_memory_table_lookup_read_cell untuk mengoperasikan memori.

Dalam proses verifikasi, kami menganggap tabel memori sebagai struktur data yang dapat berubah, dengan membangun pemetaan data alamat melalui fungsi memory_at. Dengan cara ini, kami dapat membuktikan bahwa batasan yang dihasilkan oleh fungsi alloc setara dengan operasi set dan get yang dilakukan pada pemetaan, sehingga menyederhanakan verifikasi instruksi menjadi bentuk yang mirip dengan interpreter non-ZK.

Untuk mencegah penyerang memanipulasi tabel memori, zkWasm menggunakan mekanisme penghitung untuk melacak jumlah entri yang valid. Tabel eksekusi dan tabel memori masing-masing mempertahankan penghitung, dan memastikan konsistensi antara keduanya melalui pembatasan. Ini mengharuskan verifikasi yang lebih tepat, yang memerlukan bukti bahwa setiap instruksi sesuai dengan jumlah entri tabel memori yang benar.

Proses verifikasi dilakukan dengan pendekatan dari atas ke bawah, termasuk tiga langkah:

1. Jumlah entri yang diperkirakan harus dibuat oleh instruksi.
2. Jumlah entri dalam tabel bukti tidak lebih dari yang diharapkan
3. Buktikan melalui induksi bahwa cum_mops dan instructions_mops selalu konsisten dalam tabel.

Metode verifikasi yang rinci ini membantu mengidentifikasi kesalahan potensial, seperti masalah kunci dalam mekanisme penghitungan tabel lompat.

Untuk mencapai verifikasi modular, kami membagi sistem menjadi tiga bagian independen: verifikasi sirkuit instruksi, verifikasi tabel eksekusi, dan implementasi tabel memori. Struktur ini memungkinkan beberapa insinyur untuk bekerja secara paralel, meningkatkan efisiensi verifikasi.

Secara keseluruhan, meskipun zkVM memiliki perbedaan dalam menangani status dinamis, dengan mencocokkan lapisan abstraksi dalam implementasi, pendekatan modular yang mirip dengan verifikasi interpreter tradisional masih dapat diterapkan. Pendekatan ini meminimalkan dampak yang disebabkan oleh perbedaan, sehingga setiap instruksi dapat diverifikasi secara independen berdasarkan antarmuka get-set.