Pengesahan Formal Lanjutan Bukti Sifar Pengetahuan: Cara Mengesahkan Arahan ZK

Untuk memahami dengan mendalam cara teknologi pengesahan formal digunakan pada zkVM (mesin maya berpengetahuan sifar), artikel ini akan memfokuskan pada pengesahan satu arahan. Untuk situasi keseluruhan pengesahan rasmi lanjutan ZKP (bukti sifar pengetahuan), sila rujuk artikel "Pengesahan Formal Lanjutan bagi Rantaian Sekat Bukti Sifar Pengetahuan" yang kami terbitkan pada masa yang sama.

Apakah pengesahan arahan ZK?

zkVM (mesin maya berpengetahuan sifar) mampu mencipta objek kalis pendek sebagai bukti bahawa program tertentu boleh dijalankan pada input tertentu dan ditamatkan dengan jayanya. Dalam medan Web3.0, aplikasi zkVM membolehkan daya pemprosesan yang tinggi kerana nod L1 hanya perlu mengesahkan bukti ringkas peralihan kontrak pintar daripada keadaan input kepada keadaan output dan pelaksanaan kod kontrak sebenar boleh diselesaikan di luar rantaian.

Prover zkVM akan mula-mula menjalankan program untuk menjana rekod pelaksanaan setiap langkah, dan kemudian menukar data rekod pelaksanaan kepada satu set jadual berangka (proses ini dipanggil "aritmetik"). Nombor ini mesti memenuhi satu set kekangan (iaitu, litar), yang merangkumi persamaan sambungan antara sel jadual tertentu, pemalar tetap, kekangan carian pangkalan data antara jadual dan kekangan yang perlu dipenuhi antara setiap pasangan baris jadual bersebelahan persamaan (aka "gerbang"). Pengesahan dalam rantaian boleh mengesahkan bahawa memang terdapat jadual yang memenuhi semua kekangan, sambil memastikan bahawa nombor tertentu dalam jadual tidak akan dilihat.

Pelaksanaan setiap arahan VM menghadapi banyak kekangan sedemikian Di sini kami merujuk set kekangan arahan VM ini sebagai "arahan ZK". Di bawah ialah contoh kekangan arahan beban memori zkWasm yang ditulis dalam Rust.

ZK Pengesahan arahan secara rasmi dilakukan dengan melakukan penaakulan formal pada kod ini, yang pertama-tama kami terjemahkan ke dalam bahasa formal.

Walaupun hanya satu kekangan yang mengandungi ralat, penyerang mungkin menyerahkan bukti ZK yang berniat jahat. Jadual data yang sepadan dengan bukti berniat jahat tidak sepadan dengan operasi undang-undang kontrak pintar. Tidak seperti rantaian bukan ZK seperti Ethereum, yang mempunyai banyak nod yang menjalankan pelaksanaan EVM (Mesin Maya Ethereum) yang berbeza, menjadikannya tidak mungkin pepijat yang sama akan berlaku di tempat yang sama pada masa yang sama, rantaian zkVM hanya mempunyai satu pelaksanaan VM tunggal . Dari perspektif ini sahaja, rantaian ZK lebih rapuh daripada sistem Web3.0 tradisional.

Apa yang lebih teruk ialah tidak seperti rantaian bukan ZK, memandangkan butiran pengiraan transaksi zkVM tidak diserahkan dan disimpan pada rantaian, selepas serangan berlaku, bukan sahaja sangat sukar untuk menemui butiran khusus serangan itu, tetapi juga untuk mengenal pasti serangan itu juga boleh menjadi sangat mencabar dengan sendirinya.

Sistem zkVM memerlukan pemeriksaan yang sangat ketat Malangnya, ketepatan litar zkVM sukar untuk dijamin.

Mengapa sukar untuk mengesahkan arahan ZK?

VM (Mesin Maya) ialah salah satu bahagian paling kompleks dalam seni bina sistem Web3.0. Fungsi berkuasa kontrak pintar adalah teras menyokong keupayaan Web3.0 Kuasa mereka datang daripada VM asas, yang kedua-duanya fleksibel dan kompleks: untuk menyelesaikan tugas pengkomputeran dan penyimpanan umum, VM ini mesti dapat menyokong banyak arahan. dan negeri. Sebagai contoh, pelaksanaan geth EVM memerlukan lebih daripada 7,500 baris kod bahasa Go. Begitu juga, litar ZK yang mengekang pelaksanaan arahan ini adalah sama besar dan kompleks. Seperti dalam projek zkWasm, pelaksanaan litar ZK memerlukan lebih daripada 6000 baris kod Rust.

zkWasm seni bina litar

Berbanding dengan litar ZK khusus yang digunakan dalam sistem ZK yang direka untuk aplikasi tertentu (seperti pembayaran persendirian), litar zkVM adalah lebih besar saiznya: bilangannya mungkin satu peraturan mengikat. atau dua susunan magnitud lebih besar, dan jadual aritmetik mungkin termasuk ratusan lajur yang mengandungi berjuta-juta sel berangka.

Apakah maksud pengesahan arahan ZK?

Di sini kami ingin mengesahkan ketepatan arahan XOR dalam zkWasm. Secara teknikalnya, jadual pelaksanaan zkWasm sepadan dengan urutan pelaksanaan Wasm VM yang sah. Jadi dari perspektif makro, perkara yang ingin kami sahkan ialah setiap kali arahan ini dilaksanakan, keadaan zkVM undang-undang baharu akan sentiasa dijana: setiap baris dalam jadual sepadan dengan keadaan undang-undang VM dan baris berikut akan sentiasa Ia dijana dengan melaksanakan arahan VM yang sepadan. Rajah di bawah menunjukkan teorem formal untuk ketepatan arahan XOR.

Di sini "state_rel i st" menunjukkan bahawa keadaan "st" ialah keadaan zkVM sah kontrak pintar dalam langkah "i". Seperti yang anda fikirkan, membuktikan "state_rel (i+1) ..." bukanlah perkara remeh.

Bagaimana untuk mengesahkan arahan ZK?

Walaupun semantik pengiraan integer, lakukan pengiraan XOR, dan kemudian simpan integer baharu yang dikira kembali ke tindanan yang sama. Di samping itu, langkah-langkah pelaksanaan arahan ini harus disepadukan ke dalam keseluruhan proses pelaksanaan kontrak pintar, dan susunan serta masa pelaksanaannya mestilah betul.

Oleh itu, kesan pelaksanaan arahan XOR hendaklah mengeluarkan dua nombor daripada tindanan data, menolak keputusan XOR mereka, dan pada masa yang sama menambah pembilang program untuk menunjuk kepada arahan kontrak pintar seterusnya.

Adalah sukar untuk melihat bahawa takrifan sifat ketepatan di sini secara amnya sangat serupa dengan situasi yang kami hadapi semasa mengesahkan VM kod bait tradisional (seperti penterjemah EVM dalam nod Ethereum L1). Ia bergantung pada definisi abstrak peringkat tinggi bagi keadaan mesin (di sini tindanan memori dan aliran pelaksanaan) dan takrifan kelakuan yang dijangkakan bagi setiap arahan (di sini logik aritmetik).

Walau bagaimanapun, seperti yang akan kita lihat di bawah, disebabkan sifat istimewa ZKP dan zkVM, proses pengesahan untuk ketepatannya selalunya sangat berbeza daripada VM biasa. Hanya untuk mengesahkan arahan tunggal yang kami ada di sini bergantung pada ketepatan banyak jadual dalam zkWASM: antaranya ialah jadual julat yang digunakan untuk mengehadkan saiz nilai, jadual bit (jadual bit) digunakan untuk hasil perantaraan pengiraan bit binari , Jadual pelaksanaan yang menyimpan keadaan VM bersaiz malar bagi setiap baris (serupa dengan data dalam daftar dan selak dalam CPU fizikal), dan memori yang mewakili jadual keadaan VM bersaiz berubah secara dinamik (memori, tindanan data dan tindanan panggilan) dan lompat. meja.

Langkah Pertama: Memori Tindanan

Sama seperti VM tradisional, kita perlu memastikan bahawa dua parameter integer arahan boleh dibaca daripada tindanan dan nilai hasil XORnya ditulis kembali ke tindanan dengan betul. Perwakilan formal timbunan juga kelihatan agak biasa (terdapat juga memori global dan ingatan timbunan, tetapi arahan XOR tidak menggunakannya).

zkVM menggunakan skema kompleks untuk mewakili data dinamik kerana prover ZK tidak menyokong struktur data secara asli seperti tindanan atau tatasusunan. Sebaliknya, untuk setiap nilai yang ditolak ke tindanan, jadual memori merekodkan baris yang berasingan, dan beberapa lajur digunakan untuk menunjukkan masa berkesan kemasukan. Sudah tentu, data dalam jadual ini boleh dikawal oleh penyerang, jadi beberapa kekangan mesti dikenakan untuk memastikan bahawa entri jadual benar-benar sepadan dengan arahan tindanan sebenar dalam pelaksanaan kontrak. Ini dicapai dengan mengira dengan teliti bilangan tolakan tindanan semasa pelaksanaan program. Apabila mengesahkan setiap arahan, kita perlu memastikan kiraan ini sentiasa betul. Selain itu, kami mempunyai satu siri lema yang mengaitkan kekangan yang dijana oleh satu arahan dengan carian jadual dan semakan julat masa yang melaksanakan operasi tindanan. Dari peringkat atas, kekangan pengiraan untuk operasi ingatan ditakrifkan seperti berikut.

Langkah 2: Operasi Aritmetik

Sama seperti VM tradisional, kami ingin memastikan bahawa operasi XOR bitwise adalah betul. Ini nampaknya mudah, selepas semua CPU komputer fizikal kami mampu melakukan ini sekali gus.

Tetapi untuk zkVM, ini sebenarnya tidak mudah. Satu-satunya arahan aritmetik yang disokong asli oleh peribahasa ZK ialah penambahan dan pendaraban. Untuk melaksanakan operasi bit binari, VM menggunakan skema yang agak kompleks, di mana satu jadual menyimpan hasil operasi peringkat bait tetap, dan jadual lain bertindak sebagai "pad calar" untuk menunjukkan cara melaksanakan operasi pada berbilang baris jadual. Nombor 64-bit dipecahkan kepada 8 bait dan kemudian dipasang semula untuk memberikan hasilnya.

Serpihan spesifikasi jadual bit ZkWasm

ialah operasi XOR yang sangat mudah dalam bahasa pengaturcaraan tradisional, tetapi di sini banyak lema diperlukan untuk mengesahkan ketepatan jadual tambahan ini. Untuk arahan kami, kami ada:

Langkah Tiga: Aliran Pelaksanaan

Sama seperti VM tradisional, kita perlu memastikan bahawa nilai kaunter program dikemas kini dengan betul. Untuk arahan berurutan seperti XOR, kaunter program perlu ditambah satu selepas setiap langkah.

Memandangkan zkWasm direka untuk menjalankan kod Wasm, ia juga memastikan bahawa sifat kekal memori Wasm dikekalkan sepanjang pelaksanaan.

Bahasa pengaturcaraan tradisional mempunyai sokongan asli untuk jenis data seperti nilai Boolean, integer 8-bit dan integer 64-bit, tetapi dalam litar ZK, pembolehubah sentiasa berubah dalam julat integer modulo nombor perdana yang besar (≈ 2254) . Memandangkan VM biasanya berjalan pada 64 bit, pembangun litar perlu menggunakan sistem kekangan untuk memastikan mereka mempunyai julat berangka yang betul dan jurutera pengesahan formal perlu menjejak sifat invarian tentang julat ini sepanjang proses pengesahan. Penaakulan tentang aliran pelaksanaan dan jadual pelaksanaan melibatkan semua jadual tambahan lain, jadi kita perlu menyemak sama ada julat semua data jadual adalah betul.

Sama seperti kes pengurusan nombor operasi memori, zkVM memerlukan set lema yang serupa untuk mengesahkan aliran kawalan. Secara khusus, setiap arahan panggilan dan pemulangan memerlukan penggunaan timbunan panggilan. Tindanan panggilan dilaksanakan menggunakan skema jadual yang serupa dengan tindanan data. Untuk arahan XOR, kami tidak perlu mengubah suai timbunan panggilan tetapi apabila mengesahkan keseluruhan arahan, kami masih perlu menjejak dan mengesahkan sama ada kiraan operasi aliran kawalan adalah betul.

Sahkan arahan ini

Mari kita satukan semua langkah dan sahkan teorem ketepatan hujung ke hujung arahan zkWasm XOR. Pengesahan berikut diselesaikan dalam persekitaran bukti interaktif, di mana setiap pembinaan formal dan langkah penaakulan logik menjalani pemeriksaan mesin yang paling ketat.

Seperti yang dilihat di atas, pengesahan rasmi litar zkVM boleh dilaksanakan. Tetapi ini adalah tugas yang sukar yang memerlukan pemahaman dan menjejaki banyak sifat invarian yang kompleks. Ini menggambarkan kerumitan perisian yang sedang disahkan: setiap lemma yang terlibat dalam pengesahan perlu dikendalikan dengan betul oleh pembangun litar. Memandangkan pertaruhan yang tinggi yang terlibat, adalah bernilai untuk meminta mereka diperiksa mesin oleh sistem pengesahan rasmi, dan bukannya bergantung semata-mata pada semakan manusia yang teliti.

Atas ialah kandungan terperinci Pengesahan Formal Lanjutan Bukti Sifar Pengetahuan: Cara Mengesahkan Arahan ZK. Untuk maklumat lanjut, sila ikut artikel berkaitan lain di laman web China PHP!