Dalam rangkaian blog tentang verifikasi formal tingkat lanjut atas bukti tanpa pengetahuan, kami telah membahas cara memverifikasi instruksi ZK dan analisis mendalam terhadap dua kerentanan ZK. Seperti yang ditunjukkan dalam laporan publik dan basis kode, dengan memverifikasi secara formal setiap instruksi zkWasm, kami menemukan dan memperbaiki setiap kerentanan, memungkinkan kami memverifikasi sepenuhnya keamanan teknis dan kebenaran seluruh sirkuit zkWasm.
Meskipun kami telah menunjukkan proses verifikasi instruksi zkWasm dan memperkenalkan konsep awal proyek terkait, pembaca yang akrab dengan verifikasi formal mungkin lebih tertarik untuk memahami verifikasi zkVM dengan sistem ZK lain yang lebih kecil, atau jenis VM bytecode lainnya pada. Pada artikel ini, kita akan membahas secara mendalam beberapa poin teknis yang ditemui saat memvalidasi subsistem memori zkWasm. Memori adalah bagian paling unik dari zkVM, dan penanganannya sangat penting untuk semua verifikasi zkVM lainnya.
Verifikasi formal: mesin virtual (VM) versus mesin virtual ZK (zkVM)
Tujuan utama kami adalah memverifikasi kebenaran zkWasm, yang mirip dengan teorema kebenaran penerjemah bytecode biasa (VM, seperti penerjemah EVM yang digunakan oleh node Ethereum). Artinya, setiap langkah eksekusi penerjemah berhubungan dengan langkah hukum berdasarkan semantik operasional bahasa tersebut. Seperti yang ditunjukkan pada gambar di bawah, jika status struktur data penafsir bytecode saat ini adalah SL, dan status ini ditandai sebagai status SH dalam spesifikasi tingkat tinggi mesin Wasm, maka saat juru bahasa melangkah ke status SL', di sana harus merupakan SH' negara bagian tingkat tinggi yang sah, dan spesifikasi Wasm menetapkan bahwa SH harus melangkah ke SH'.
Demikian pula, zkVM memiliki teorema kebenaran serupa: setiap baris baru dalam tabel eksekusi zkWasm berhubungan dengan langkah hukum berdasarkan semantik operasional bahasa. Seperti yang ditunjukkan pada gambar di bawah, jika status baris struktur data saat ini dalam tabel eksekusi adalah SR, dan status ini dinyatakan sebagai status SH dalam spesifikasi tingkat tinggi mesin Wasm, maka status baris berikutnya dari tabel eksekusi SR' harus sesuai dengan keadaan tingkat tinggi SH' , dan spesifikasi Wasm menetapkan bahwa SH harus melangkah ke SH'.
Dapat dilihat bahwa spesifikasi status tingkat tinggi dan langkah-langkah Wasm konsisten baik di VM atau zkVM, sehingga dapat memanfaatkan pengalaman verifikasi sebelumnya dari penerjemah atau kompiler bahasa pemrograman. Yang istimewa dari verifikasi zkVM adalah jenis struktur data yang membentuk status sistem tingkat rendah.
Pertama, seperti yang kami nyatakan di postingan blog sebelumnya, pembuktian zk pada dasarnya adalah operasi bilangan bulat modulo bilangan prima besar, sedangkan spesifikasi Wasm dan juru bahasa normal menangani bilangan bulat 32-bit atau 64-bit. Sebagian besar implementasi zkVM melibatkan hal ini, jadi pemrosesan terkait juga perlu dilakukan selama verifikasi. Namun, ini adalah masalah "lokal": setiap baris kode menjadi lebih kompleks karena operasi aritmatika yang perlu ditangani, namun keseluruhan struktur kode dan pembuktiannya tidak berubah.
Perbedaan besar lainnya adalah cara penanganan struktur data berukuran dinamis. Dalam penerjemah bytecode biasa, memori, tumpukan data, dan tumpukan panggilan semuanya diimplementasikan sebagai struktur data yang dapat diubah. Demikian pula, spesifikasi Wasm mewakili memori sebagai tipe data dengan metode get/set. Misalnya, interpreter EVM Geth memiliki tipe data `Memory`, yang diimplementasikan sebagai array byte yang mewakili memori fisik dan ditulis dan dibaca melalui metode `Set 32` dan `GetPtr`. Untuk mengimplementasikan instruksi penyimpanan memori, Geth memanggil `Set 32` untuk memodifikasi memori fisik.
func opMstore(pc *uint 64, penerjemah *EVMInterpreter, cakupan *ScopeContext) ([]byte, kesalahan) {
// nilai pop dari tumpukan
mStart, nilai := lingkup.Tumpukan.pop(), lingkup.Tumpukan.pop()
lingkup.Memori.Set 32(mStart.Uint 64(), val)
kembali nihil, nihil
}
Dalam pembuktian kebenaran penerjemah di atas, kami membuktikan bahwa status tingkat tinggi dan status tingkat rendahnya cocok satu sama lain setelah memberikan nilai ke memori konkret di penerjemah dan memori abstrak di spesifikasi.
Namun, dengan zkVM, situasinya menjadi lebih rumit.
tabel memori zkWasm dan lapisan abstraksi memori
Di zkVM, terdapat kolom pada tabel eksekusi untuk data berukuran tetap (mirip dengan register di CPU), namun tidak dapat digunakan untuk menangani struktur data berukuran dinamis, yang diimplementasikan dengan mencari tabel tambahan. Tabel eksekusi zkWasm memiliki kolom EID, yang nilainya 1, 2, 3..., dan memiliki dua tabel tambahan, tabel memori dan tabel lompat, yang masing-masing digunakan untuk merepresentasikan data memori dan tumpukan panggilan.
Berikut ini contoh cara penerapan program penarikan:
int saldo, jumlah;
batal main() {
keseimbangan = 100;
jumlah = 10;
saldo -= jumlah; // tarik
}
Isi dan struktur tabel eksekusi cukup sederhana. Ini memiliki 6 langkah eksekusi (EID 1 hingga 6), setiap langkah memiliki baris yang mencantumkan opcode (opcode) dan, jika instruksinya adalah membaca atau menulis memori, alamat dan datanya:
Setiap baris dalam tabel memori berisi alamat, data, EID awal dan EID akhir. EID awal adalah EID dari langkah eksekusi yang menulis data ini ke alamat ini, dan EID akhir adalah EID dari langkah eksekusi berikutnya yang akan menulis alamat ini. (Ini juga berisi hitungan, yang akan kita bahas secara rinci nanti.) Untuk rangkaian instruksi pembacaan memori Wasm, ia menggunakan batasan pencarian untuk memastikan bahwa ada entri yang sesuai dalam tabel sehingga EID dari instruksi baca ada di tabel. berkisar dari awal hingga akhir Di dalam. (Demikian pula, setiap baris tabel lompat berhubungan dengan bingkai tumpukan panggilan, dan setiap baris diberi label dengan EID dari langkah instruksi panggilan yang membuatnya.)
Sistem memori ini sangat berbeda dari penerjemah VM biasa: tabel memori bukanlah memori yang dapat diubah yang diperbarui secara bertahap, namun berisi riwayat semua akses memori sepanjang jejak eksekusi. Untuk menyederhanakan pekerjaan programmer, zkWasm menyediakan lapisan abstraksi, diimplementasikan melalui dua fungsi entri yang mudah digunakan. Mereka adalah:
alokasikan_memori_tabel_pencarian_tulis_sel
Dan
Alloc_memory_table_lookup_read_cell
Parameternya adalah sebagai berikut:
Misalnya, kode yang mengimplementasikan instruksi penyimpanan memori di zkWasm berisi panggilan ke fungsi 'write alloc':
biarkan memory_table_lookup_heap_write1 = pengalokasi
.alokasi_tabel_memori_lookup_tulis_sel_dengan_nilai(
"simpan tulis res 1",
pembangun_kendala,
idul fitri,
pindahkan |____| konstanta_dari!(LocationType::Heap sebagai u 64),
pindahkan |meta| load_block_index.expr(meta), // alamat
pindahkan |____| konstanta_dari!( 0), // adalah 32-bit
pindahkan |____| constant_from!( 1), // (selalu) diaktifkan
{ ...
biarkan store_value_dalam_heap1 = memory_table_lookup_heap_write1.nilai_sel;
Fungsi `alloc` bertanggung jawab untuk menangani batasan pencarian antar tabel dan batasan aritmatika yang menghubungkan `idul fitri` saat ini dengan entri tabel memori. Dari sini, pemrogram dapat memperlakukan tabel ini sebagai memori biasa, dan nilai `store_value_in_heap1` telah ditetapkan ke alamat `load_block_index` setelah kode dieksekusi.
Demikian pula, instruksi pembacaan memori diimplementasikan menggunakan fungsi `read_alloc`. Dalam contoh urutan eksekusi di atas, terdapat batasan baca untuk setiap instruksi beban dan batasan tulis untuk setiap instruksi penyimpanan, dan setiap batasan dipenuhi oleh entri dalam tabel memori.
mtable_lookup_write(baris 1.eid, baris 1.alamat_toko, baris 1.nilai_toko)
⇐ (baris 1.eid= 1 ∧ baris 1.alamat_toko=saldo ∧ baris 1.nilai_toko= 100 ∧ ...)
mtable_lookup_write(baris 2.eid, baris 2.alamat_toko, baris 2.nilai_toko)
⇐ (baris 2.eid= 2 ∧ baris 2.alamat_toko=jumlah ∧ baris 2.nilai_toko= 10 ∧ ...)
mtable_lookup_read(baris 3.eid, baris 3.load_addr, baris 3.load_value)
⇐ ( 2
mtable_lookup_read(baris 4.eid, baris 4.load_addr, baris 4.load_value)
⇐ ( 1
mtable_lookup_write(baris 6.eid, baris 6.alamat_toko, baris 6.nilai_toko)
⇐ (baris 6.eid= 6 ∧ baris 6.alamat_toko=saldo ∧ baris 6.nilai_toko= 90 ∧ ...)
Struktur verifikasi formal harus sesuai dengan abstraksi yang digunakan dalam perangkat lunak yang diverifikasi, sehingga pembuktiannya dapat mengikuti logika yang sama dengan kode. Untuk zkWasm, ini berarti kita perlu memverifikasi rangkaian tabel memori dan fungsi "mengalokasikan sel baca/tulis" sebagai modul, yang berinteraksi seperti memori variabel. Dengan adanya antarmuka seperti itu, verifikasi setiap rangkaian instruksi dapat dilakukan dengan cara yang mirip dengan penerjemah biasa, sedangkan kompleksitas ZK tambahan dikemas dalam modul subsistem memori.
Dalam verifikasi, kami menerapkan gagasan bahwa "tabel memori sebenarnya dapat dianggap sebagai struktur data yang bisa berubah". Artinya, tulis fungsi `memory_at type`, yang memindai tabel memori sepenuhnya dan membuat pemetaan data alamat yang sesuai. (Rentang nilai variabel `type` di sini adalah tiga tipe data memori Wasm yang berbeda: heap, tumpukan data, dan variabel global.) Kemudian, kami membuktikan bahwa batasan memori yang dihasilkan oleh fungsi alokasi setara dengan menggunakan set dan get fungsi. Perubahan data dilakukan oleh pemetaan data alamat yang sesuai. Kita dapat membuktikan:
Untuk setiap Idul Fitri, jika kendala berikut ini berlaku
memory_table_lookup_read_cell eid jenis offset nilai
Tetapi
dapatkan (memory_at eid type) offset = Beberapa nilai
Dan, jika kendala berikut ini berlaku
tabel_memori_lookup_tulis_sel eid jenis offset nilai
Tetapi
memory_at (eid+ 1) tipe = set (tipe memory_at eid) nilai offset
Setelah ini, verifikasi setiap instruksi dapat didasarkan pada operasi get dan set pada peta data alamat, mirip dengan penerjemah bytecode non-ZK.
mekanisme penghitungan penulisan memori zkWasm
Namun, uraian sederhana di atas tidak mengungkapkan seluruh isi tabel memori dan tabel lompat. Di bawah kerangka zkVM, tabel ini dapat dimanipulasi oleh penyerang, yang dapat dengan mudah memanipulasi instruksi pemuatan memori dan mengembalikan nilai arbitrer dengan memasukkan sederet data.
Mengambil program penarikan sebagai contoh, penyerang memiliki kesempatan untuk memasukkan data palsu ke dalam saldo akun dengan melakukan operasi penulisan memori $110 sebelum operasi penarikan. Proses ini dapat dicapai dengan menambahkan baris data ke tabel memori dan mengubah nilai sel yang ada di tabel memori dan tabel eksekusi. Ini akan menghasilkan penarikan "gratis" karena saldo akun akan tetap $100 setelah operasi.
Untuk memastikan bahwa tabel memori (dan tabel lompat) hanya berisi entri valid yang dihasilkan oleh instruksi penulisan memori (dan panggilan dan pengembalian) yang benar-benar dijalankan, zkWasm menggunakan mekanisme penghitungan khusus untuk memantau jumlah entri. Secara khusus, tabel memori memiliki kolom khusus yang mencatat jumlah total entri yang ditulis ke memori. Pada saat yang sama, tabel eksekusi juga berisi penghitung untuk menghitung jumlah operasi penulisan memori yang diharapkan untuk setiap instruksi. Pastikan kedua penghitungan tersebut konsisten dengan menetapkan batasan kesetaraan. Logika metode ini sangat intuitif: setiap kali operasi penulisan dilakukan di memori, operasi tersebut akan dihitung satu kali, dan harus ada catatan yang sesuai di tabel memori. Oleh karena itu, penyerang tidak dapat memasukkan entri tambahan apa pun ke dalam tabel memori.
Pernyataan logis di atas agak kabur, dan dalam proses pembuktian mekanis, perlu dibuat lebih tepat. Pertama, kita perlu merevisi pernyataan lemma penulisan memori yang disebutkan di atas. Kami mendefinisikan fungsi `mops_at eid type` untuk menghitung entri tabel memori dengan `eid` dan `type` tertentu (sebagian besar instruksi akan membuat 0 atau 1 entri pada eid ). Pernyataan teorema lengkap memiliki prasyarat tambahan yang menyatakan bahwa tidak ada entri tabel memori palsu:
Jika kendala berikut ini berlaku
(memori_tabel_lookup_tulis_sel eid jenis offset nilai)
Dan batasan baru berikut ini ditetapkan
(jenis mops_at eid) = 1
Tetapi
(memory_at(eid+ 1) jenis) = tetapkan nilai offset (memory_at eid jenis)
Hal ini memerlukan verifikasi kami yang lebih tepat dibandingkan kasus sebelumnya. Hanya berasal dari batasan kesetaraan bahwa jumlah total entri tabel memori sama dengan jumlah total penulisan memori dalam eksekusi tidaklah cukup untuk menyelesaikan verifikasi. Untuk membuktikan kebenaran suatu instruksi, kita perlu mengetahui bahwa setiap instruksi berhubungan dengan jumlah entri tabel memori yang benar. Misalnya, kita perlu mengesampingkan apakah penyerang dapat menghilangkan entri tabel memori untuk instruksi dalam urutan eksekusi dan membuat entri tabel memori baru yang berbahaya untuk instruksi lain yang tidak terkait.
Untuk membuktikan hal ini, kami menggunakan pendekatan top-down untuk membatasi jumlah entri tabel memori yang sesuai dengan instruksi tertentu, yang melibatkan tiga langkah. Pertama, kami memperkirakan jumlah entri yang harus dibuat untuk instruksi dalam urutan eksekusi berdasarkan jenis instruksi. Kami menyebut jumlah penulisan yang diharapkan dari langkah ke-i hingga akhir eksekusi `instructions_mops i`, dan jumlah entri yang sesuai dalam tabel memori dari instruksi ke-i hingga akhir eksekusi `cum_mops (eid i) `. Dengan menganalisis batasan pencarian setiap instruksi, kita dapat membuktikan bahwa instruksi tersebut menghasilkan entri yang tidak lebih sedikit dari yang diharapkan, yang mengarah pada kesimpulan bahwa setiap segmen dari [i... numRows] yang dilacak menghasilkan entri yang tidak kurang dari yang diharapkan:
Lemma cum_mops_bound': untuk semua n i,
0 ≤ saya ->
i + Z.dari_nat n = etabel_numRow ->
MTable.cum_mops (nilai_etable eid_sel i) (max_eid+ 1) ≥ instructions_mops' i n.
Kedua, jika Anda dapat menunjukkan bahwa tabel tidak memiliki entri lebih banyak dari yang diharapkan, maka tabel tersebut memiliki jumlah entri yang tepat, dan itu sudah jelas.
Lemma cum_mops_equal' : untuk semua n i,
0 ≤ saya ->
i + Z.dari_nat n = etabel_numRow ->
MTable.cum_mops (nilai_etable sel_eid i) (max_eid+ 1) ≤ instruksi_mops' i n ->
MTable.cum_mops (nilai_etable eid_sel i) (max_eid+ 1) = instruksi_mops' i n.
Sekarang lanjutkan ke langkah ketiga. Teorema kebenaran kami menyatakan bahwa untuk n apa pun, cum_mops dan instruction_mops selalu konsisten dari baris n hingga akhir tabel:
Lemma cum_mops_equal : untuk semua n,
0 <= Z.dari_nat n < etable_numRow ->
MTable.cum_mops (nilai_etabel eid_sel (Z.dari_nat n)) (max_eid+ 1) = instruksi_mops (Z.dari_nat n)
Verifikasi diselesaikan dengan merangkum n. Baris pertama dalam tabel adalah batasan kesetaraan zkWasm, yang menunjukkan bahwa jumlah total entri dalam tabel memori sudah benar, yaitu cum_mops 0 = instruction_mops 0 . Untuk baris berikut, hipotesis induktif memberitahu kita:
cum_mops n = instruksi_pel lantai n
dan kami berharap dapat membuktikannya
cum_mops (n+ 1) = instruksi_mops (n+ 1)
Perhatikan di sini
cum_mops n = mop_at n + cum_mops (n+ 1)
Dan
instruksi_pel n = instruksi_pel n + instruksi_pel (n+ 1)
Oleh karena itu, kita bisa mendapatkannya
mops_at n + cum_mops (n+ 1) = instruksi_mops n + instruksi_mops (n+ 1)
Sebelumnya, kami telah menunjukkan bahwa setiap instruksi akan menghasilkan jumlah entri yang tidak kurang dari yang diharapkan, misalnya.
mops_at n ≥ instruksi_mops n.
Jadi bisa disimpulkan
cum_mops (n+ 1) ≤ instruksi_mops (n+ 1)
Di sini kita perlu menerapkan lemma kedua di atas.
(Dengan menggunakan lemma serupa untuk memverifikasi tabel lompat, dapat dibuktikan bahwa setiap instruksi panggilan dapat menghasilkan entri tabel lompat secara akurat, sehingga teknik pembuktian ini dapat diterapkan secara umum. Namun, kami masih memerlukan verifikasi lebih lanjut untuk membuktikan bahwa pengembalian tersebut Benar. instruksi. Eid yang dikembalikan berbeda dari eid instruksi pemanggil yang membuat bingkai panggilan, jadi kita juga memerlukan properti invarian tambahan untuk menyatakan bahwa nilai eid bertambah dalam satu arah selama urutan eksekusi.)
Mendeskripsikan proses pembuktian secara mendetail merupakan ciri khas verifikasi formal dan merupakan alasan mengapa memverifikasi bagian kode tertentu sering kali membutuhkan waktu lebih lama daripada menulisnya. Tapi apakah itu sepadan? Hal ini bermanfaat dalam kasus ini karena kami menemukan bug kritis dalam mekanisme penghitungan tabel lompat selama pembuktian. Bug ini telah dijelaskan secara rinci dalam artikel sebelumnya - secara ringkas, versi kode yang lebih lama memperhitungkan instruksi panggilan dan pengembalian, dan penyerang dapat membuat lompatan palsu dengan menambahkan instruksi pengembalian tambahan ke urutan eksekusi Entri tabel memberikan ruang . Meskipun mekanisme penghitungan yang salah dapat memenuhi intuisi bahwa setiap panggilan dan instruksi kembali dihitung, masalah muncul ketika kita mencoba untuk menyempurnakan intuisi ini menjadi pernyataan teorema yang lebih tepat.
Jadikan proses pembuktian bersifat modular
Dari pembahasan di atas terlihat adanya ketergantungan melingkar antara pembuktian rangkaian setiap instruksi dan pembuktian kolom hitungan pada tabel eksekusi. Untuk membuktikan kebenaran rangkaian instruksi, kita perlu mempertimbangkan penulisan memori di dalamnya; yaitu, kita perlu mengetahui jumlah entri tabel memori pada EID tertentu, dan kita perlu membuktikan bahwa operasi penulisan memori diperhitungkan. tabel eksekusi sudah benar; dan ini juga perlu dibuktikan bahwa setiap instruksi melakukan setidaknya jumlah minimum penulisan memori.
Selain itu, ada faktor lain yang perlu dipertimbangkan: Proyek zkWasm cukup besar, sehingga pekerjaan verifikasi perlu dimodulasi agar beberapa teknisi verifikasi dapat membagi pekerjaan. Oleh karena itu, perhatian khusus perlu diberikan pada kompleksitasnya ketika mendekonstruksi pembuktian mekanisme penghitungan. Misalnya, untuk instruksi LocalGet, dua teorema adalah sebagai berikut:
Teorema opcode_mops_correct_local_get : untuk semua i,
0 <= i ->
nilai_etabel sel_eid i > 0 ->
opcode_mops_correct LocalGet i.
Teorema LocalGetOp_correct : untuk semua i st y xs,
0 <= i ->
nilai_etable diaktifkan_sel i = 1 ->
pel lantai_di_benar i ->
nilai_tabel (ops_cell LocalGet) i = 1 ->
negara_rel i st ->
tumpukan wasm_st = xs ->
(nilai_tabel_offset_sel i) > 1 ->
nth_error xs (Z.to_nat (nilai_tabel_offset_sel i - 1)) = Beberapa y ->
state_rel (i+ 1) (perbarui_tumpukan (incr_iid st) (y:: xs)).
Pernyataan teorema pertama
opcode_mops_benar LocalGet saya
Ketika diperluas, ini berarti bahwa instruksi tersebut membuat setidaknya satu entri tabel memori pada baris i (angka 1 ditentukan dalam spesifikasi opcode LocalGet dari zkWasm).
Teorema kedua adalah teorema kebenaran lengkap dari instruksi yang dikutip
mops_at_correct saya
Sebagai hipotesis, ini berarti bahwa instruksi tersebut menciptakan tepat satu entri tabel memori.
Seorang insinyur verifikasi dapat membuktikan kedua teorema ini secara independen dan kemudian menggabungkannya dengan bukti tentang tabel eksekusi untuk membuktikan kebenaran seluruh sistem. Perlu dicatat bahwa semua pembuktian untuk instruksi individual dapat dilakukan pada tingkat batasan baca/tulis tanpa mengetahui implementasi spesifik dari tabel memori. Oleh karena itu, proyek ini dibagi menjadi tiga bagian yang dapat ditangani secara mandiri.
Meringkaskan
Memverifikasi sirkuit zkVM baris demi baris pada dasarnya tidak berbeda dengan memverifikasi aplikasi ZK di bidang lain, karena keduanya memerlukan alasan serupa tentang batasan aritmatika. Dari perspektif tingkat tinggi, verifikasi zkVM memerlukan banyak metode verifikasi formal yang sama dengan yang digunakan dalam penerjemah dan kompiler bahasa pemrograman. Perbedaan utama di sini adalah status mesin virtual berukuran dinamis. Namun, dampak dari perbedaan ini dapat diminimalkan dengan menyusun struktur verifikasi secara hati-hati agar sesuai dengan lapisan abstraksi yang digunakan dalam implementasi, sehingga setiap instruksi dapat diimplementasikan sebagai modul independen berdasarkan antarmuka get-set seperti pada penerjemah kimia biasa verifikasi.
