Dalam artikel sebelumnya, kami membahas verifikasi formal lanjutan dari sistem Zero-Knowledge Proof (ZKP): cara memverifikasi instruksi ZK. Dengan memverifikasi secara formal setiap instruksi zkWasm, kami dapat sepenuhnya memastikan keamanan teknis dan kebenaran seluruh sirkuit zkWasm. Dalam artikel ini, kami akan fokus pada perspektif penemuan kerentanan, menganalisis kerentanan spesifik yang diidentifikasi selama proses audit dan verifikasi, dan pelajaran yang dipetik darinya. Untuk diskusi umum tentang verifikasi formal lanjutan dari blockchain ZKP, silakan merujuk ke artikel tentang verifikasi formal lanjutan dari blockchain ZKP.

Sebelum membahas kerentanan ZK, mari kita pahami dulu bagaimana CertiK melakukan verifikasi formal ZK. Untuk sistem kompleks seperti ZK Virtual Machine (zkVM), langkah pertama dalam verifikasi formal (FV) adalah mendefinisikan dengan jelas apa yang perlu diverifikasi dan propertinya. Ini memerlukan tinjauan komprehensif tentang desain sistem ZK, implementasi kode, dan pengaturan pengujian. Proses ini tumpang tindih dengan audit reguler tetapi berbeda dalam hal itu, setelah peninjauan, tujuan verifikasi dan properti harus ditetapkan. Di CertiK, kami menyebutnya sebagai verifikasi berorientasi audit. Pekerjaan audit dan verifikasi biasanya terintegrasi. Untuk zkWasm, kami melakukan audit dan verifikasi formal secara bersamaan.

Apa itu Kerentanan ZK?

Fitur inti dari sistem Zero-Knowledge Proof (ZKP) adalah bahwa mereka memungkinkan transfer bukti perhitungan terenkripsi singkat yang dilakukan secara offline atau pribadi (seperti transaksi blockchain) ke verifikator ZKP. Verifikator memeriksa dan mengkonfirmasi bukti untuk memastikan bahwa perhitungan terjadi seperti yang diklaim. Dalam konteks ini, kerentanan ZK akan memungkinkan peretas untuk mengirimkan bukti ZK palsu untuk transaksi palsu dan membuatnya diterima oleh verifikator ZKP.

Untuk pembuktian zkVM, proses bukti ZK melibatkan menjalankan program, menghasilkan catatan eksekusi untuk setiap langkah, dan mengubah catatan eksekusi ini menjadi satu set tabel numerik (proses yang dikenal sebagai "arithmetization"). Angka-angka ini harus memenuhi serangkaian batasan ("sirkuit"), yang mencakup hubungan antara sel tabel tertentu, konstanta tetap, batasan pencarian database antara tabel, dan persamaan polinomial (atau "gerbang") yang harus dipenuhi oleh setiap pasangan baris tabel yang berdekatan. Verifikasi on-chain dapat mengkonfirmasi keberadaan tabel yang memenuhi semua batasan tanpa mengungkapkan angka spesifik dalam tabel.

Tabel Aritmetisasi dalam zkWasm

Keakuratan setiap kendala sangat penting. Setiap kesalahan dalam kendala, apakah itu terlalu lemah atau hilang, dapat memungkinkan peretas untuk mengirimkan bukti yang menyesatkan. Tabel ini mungkin tampak mewakili pelaksanaan kontrak pintar yang valid tetapi kenyataannya tidak. Dibandingkan dengan VM tradisional, opasitas transaksi zkVM memperkuat kerentanan ini. Dalam rantai non-ZK, rincian perhitungan transaksi dicatat secara publik di blockchain; namun, zkVM tidak menyimpan detail ini secara on-chain. Kurangnya transparansi ini membuat sulit untuk menentukan secara spesifik serangan atau bahkan jika serangan telah terjadi.

Sirkuit ZK yang memberlakukan aturan eksekusi instruksi zkVM sangat kompleks. Untuk zkWasm, implementasi sirkuit ZK-nya melibatkan lebih dari 6.000 baris kode Rust dan ratusan kendala. Kompleksitas ini sering berarti bahwa mungkin ada beberapa kerentanan yang menunggu untuk ditemukan.

Arsitektur Sirkuit zkWasm

Memang, melalui audit dan verifikasi formal zkWasm, kami telah menemukan beberapa kerentanan tersebut. Di bawah ini, kita akan membahas dua contoh representatif dan memeriksa perbedaan di antara mereka.

Kerentanan Kode: Serangan Injeksi Data Load8

Kerentanan pertama melibatkan instruksi Load8 di zkWasm. Dalam zkWasm, pembacaan memori heap dilakukan menggunakan serangkaian instruksi LoadN, di mana N adalah ukuran data yang akan dimuat. Misalnya, Load64 harus membaca data 64-bit dari alamat memori zkWasm. Load8 harus membaca data 8-bit (yaitu, satu byte) dari memori dan pad-nya dengan nol untuk membuat nilai 64-bit. Secara internal, zkWasm mewakili memori sebagai array byte 64-bit, sehingga perlu "memilih" bagian dari array memori. Ini dilakukan dengan menggunakan empat variabel menengah (u16_cells), yang bersama-sama membentuk nilai beban 64-bit lengkap.

Batasan untuk instruksi LoadN ini didefinisikan sebagai berikut:

Kendala ini dibagi menjadi tiga kasus: Load32, Load16, dan Load8. Load64 tidak memiliki kendala karena unit memori persis 64 bit. Untuk kasus Load32, kode memastikan bahwa 4 byte (32 bit) tinggi di unit memori harus nol.

Untuk kasus Load16, kode memastikan bahwa 6 byte (48 bit) tinggi di unit memori harus nol.

Untuk kasus Load8, seharusnya 7 byte (56 bit) tinggi di unit memori menjadi nol. Sayangnya, ini tidak terjadi dalam kode.

Seperti yang Anda lihat, hanya 9 hingga 16 bit tinggi yang dibatasi hingga nol. 48 bit tinggi lainnya dapat berupa nilai apa pun dan masih lulus sebagai "baca dari memori."

Memanfaatkan kerentanan ini, peretas dapat mengutak-atik bukti ZK urutan eksekusi yang sah, menyebabkan instruksi Load8 memuat byte tak terduga ini, yang mengakibatkan kerusakan data. Selain itu, melalui pengaturan kode dan data sekitarnya yang cermat, hal itu dapat memicu eksekusi dan transfer palsu, yang mengarah pada pencurian data dan aset. Transaksi palsu ini dapat melewati pemeriksaan pemeriksa zkWasm dan salah dikenali sebagai transaksi yang sah oleh blockchain.

Memperbaiki kerentanan ini sebenarnya cukup sederhana.

Kerentanan ini mewakili kelas kerentanan ZK yang disebut "kerentanan kode" karena berasal dari implementasi kode dan dapat dengan mudah diperbaiki melalui modifikasi kode lokal kecil. Seperti yang mungkin Anda setujui, kerentanan ini juga relatif lebih mudah diidentifikasi orang.

Kerentanan Desain: Serangan Balik Palsu

Mari kita lihat kerentanan lain, kali ini mengenai pemanggilan dan pengembalian zkWasm. Pemanggilan dan pengembalian adalah instruksi VM mendasar yang memungkinkan satu konteks yang berjalan (misalnya, fungsi) untuk memanggil yang lain dan melanjutkan eksekusi konteks panggilan setelah pemanggil menyelesaikan eksekusinya. Setiap doa mengharapkan pengembalian di kemudian hari. Data dinamis yang dilacak oleh zkWasm selama siklus hidup pemanggilan dan pengembalian dikenal sebagai "bingkai panggilan." Karena zkWasm mengeksekusi instruksi secara berurutan, semua frame panggilan dapat dipesan berdasarkan kemunculannya selama runtime. Di bawah ini adalah contoh kode pemanggilan/pengembalian yang berjalan di zkWasm.

Pengguna dapat memanggil fungsi buy_token() untuk membeli token (mungkin dengan pembayaran atau transfer barang berharga lainnya). Salah satu langkah intinya adalah meningkatkan saldo akun token sebesar 1 dengan memanggil fungsi add_token(). Karena prover ZK itu sendiri tidak mendukung struktur data bingkai panggilan, Tabel Eksekusi (E-Table) dan Tabel Lompat (J-Table) diperlukan untuk merekam dan melacak riwayat lengkap bingkai panggilan ini.

Gambar di atas menggambarkan proses buy_token() memanggil add_token() dan kembali dari add_token() ke buy_token(). Dapat dilihat bahwa saldo akun token meningkat sebesar 1. Dalam Tabel Eksekusi, setiap langkah eksekusi menempati satu baris, termasuk nomor bingkai panggilan saat ini yang sedang dijalankan, nama fungsi konteks saat ini (hanya untuk tujuan ilustrasi), jumlah instruksi yang sedang berjalan dalam fungsi, dan instruksi saat ini yang disimpan dalam tabel (hanya untuk tujuan ilustrasi). Dalam Tabel Lompat, setiap bingkai panggilan menempati satu baris, menyimpan jumlah bingkai pemanggilnya, nama konteks fungsi pemanggil (hanya untuk tujuan ilustrasi), dan posisi instruksi berikutnya dari bingkai pemanggil (sehingga bingkai dapat kembali). Di kedua tabel, ada kolom "jops" yang melacak apakah instruksi saat ini adalah call/return (dalam Tabel Eksekusi) dan jumlah total instruksi call/return untuk frame tersebut (dalam Jump Table).

Seperti yang diharapkan, setiap panggilan harus memiliki pengembalian yang sesuai, dan setiap frame hanya boleh memiliki satu panggilan dan satu pengembalian. Seperti yang ditunjukkan pada gambar di atas, nilai "jops" untuk frame pertama di Jump Table adalah 2, sesuai dengan baris pertama dan ketiga di Tabel Eksekusi, di mana nilai "jops" adalah 1. Semuanya terlihat normal saat ini.

Namun, ada masalah di sini: sementara satu panggilan dan satu pengembalian akan meningkatkan jumlah "jops" untuk frame menjadi 2, dua panggilan atau dua pengembalian juga akan menghasilkan hitungan 2. Memiliki dua panggilan atau dua pengembalian per frame mungkin tampak tidak masuk akal, tetapi penting untuk diingat bahwa inilah yang akan dilakukan peretas dengan melanggar harapan.

Anda mungkin merasa bersemangat sekarang, tetapi apakah kita benar-benar menemukan masalahnya?

Ternyata dua panggilan tidak menjadi masalah karena kendala Tabel Eksekusi dan Tabel Langsung mencegah dua panggilan dikodekan ke dalam baris bingkai yang sama karena setiap panggilan menghasilkan nomor bingkai baru, yaitu, nomor bingkai panggilan saat ini ditambah 1.

Namun, situasinya tidak begitu beruntung untuk dua pengembalian: karena tidak ada bingkai baru yang dibuat saat pengembalian, peretas memang bisa mendapatkan Tabel Eksekusi dan Tabel Lompat dari urutan eksekusi yang sah dan menyuntikkan pengembalian palsu (dan bingkai yang sesuai). Misalnya, contoh Tabel Eksekusi dan Tabel Lompat sebelumnya dari buy_token() memanggil add_token() dapat dirusak oleh peretas ke skenario berikut:

Peretas menyuntikkan dua pengembalian palsu antara panggilan asli dan pengembalian di Tabel Eksekusi dan menambahkan baris bingkai palsu baru di Tabel Langsung (pengembalian asli dan langkah-langkah eksekusi instruksi berikutnya di Tabel Eksekusi perlu ditambah dengan 4). Karena jumlah "jops" untuk setiap baris di Jump Table adalah 2, batasannya terpenuhi, dan pemeriksa bukti zkWasm akan menerima "bukti" dari urutan eksekusi palsu ini. Seperti yang terlihat dari gambar, saldo akun token meningkat 3 kali lipat, bukan 1. Oleh karena itu, peretas dapat memperoleh 3 token dengan harga 1.

Ada berbagai cara untuk mengatasi masalah ini. Salah satu pendekatan yang jelas adalah melacak panggilan dan pengembalian secara terpisah dan memastikan bahwa setiap frame memiliki tepat satu panggilan dan satu pengembalian.

Anda mungkin telah memperhatikan bahwa sejauh ini kami belum menunjukkan satu baris kode pun untuk kerentanan ini. Alasan utamanya adalah tidak ada baris kode yang bermasalah; Implementasi kode sangat selaras dengan tabel dan desain kendala. Masalahnya terletak pada desain itu sendiri, dan begitu juga perbaikannya.

Anda mungkin berpikir kerentanan ini harus jelas, tetapi kenyataannya tidak. Ini karena ada kesenjangan antara "dua panggilan atau dua pengembalian juga akan menghasilkan hitungan 'jops' 2" dan "dua pengembalian sebenarnya dimungkinkan." Yang terakhir membutuhkan analisis terperinci dan komprehensif dari berbagai kendala dalam Tabel Eksekusi dan Tabel Lompat, sehingga sulit untuk melakukan penalaran informal yang lengkap.

Perbandingan Dua Kerentanan

"Kerentanan Injeksi Data Load8" dan "Kerentanan Pengembalian Pemalsuan" keduanya memiliki potensi untuk memungkinkan peretas memanipulasi bukti ZK, membuat transaksi palsu, menipu pemeriksa bukti, dan terlibat dalam pencurian atau pembajakan. Namun, sifat mereka dan cara mereka ditemukan sangat berbeda.

"Kerentanan Injeksi Data Load8" ditemukan selama audit zkWasm. Ini bukan tugas yang mudah, karena kami harus meninjau ratusan kendala di lebih dari 6.000 baris kode Rust dan lusinan instruksi zkWasm. Meskipun demikian, kerentanan itu relatif mudah dideteksi dan dikonfirmasi. Karena kerentanan ini diperbaiki sebelum verifikasi formal dimulai, kerentanan ini tidak ditemui selama proses verifikasi. Jika kerentanan ini tidak ditemukan selama audit, kami dapat mengharapkannya ditemukan selama verifikasi instruksi Load8.

"Kerentanan Pengembalian Pemalsuan" ditemukan selama verifikasi formal setelah audit. Salah satu alasan kami gagal menemukannya selama audit adalah bahwa zkWasm memiliki mekanisme yang mirip dengan "jops" yang disebut "mops," yang melacak instruksi akses memori yang sesuai dengan data historis untuk setiap unit memori selama runtime zkWasm. Kendala pada jumlah pel memang benar karena hanya melacak satu jenis instruksi memori, memori menulis, dan data historis setiap unit memori tidak berubah dan ditulis hanya sekali (jumlah pel adalah 1). Tetapi bahkan jika kami telah memperhatikan potensi kerentanan ini selama audit, kami masih tidak dapat dengan mudah mengkonfirmasi atau mengesampingkan setiap skenario yang mungkin tanpa alasan formal yang ketat pada semua kendala yang relevan, karena sebenarnya tidak ada baris kode yang salah.

Singkatnya, kedua kerentanan ini termasuk dalam kategori "kerentanan kode" dan "kerentanan desain," masing-masing. Kerentanan kode relatif mudah, lebih mudah ditemukan (kode salah), dan lebih mudah untuk dipikirkan dan dikonfirmasi. Kerentanan desain bisa sangat halus, lebih sulit ditemukan (tidak ada kode "salah"), dan lebih sulit untuk dipikirkan dan dikonfirmasi.

Praktik Terbaik untuk Menemukan Kerentanan ZK

Berdasarkan pengalaman kami mengaudit dan memverifikasi secara formal zkVM dan rantai ZK dan non-ZK lainnya, berikut adalah beberapa saran tentang cara terbaik melindungi sistem ZK:

Memeriksa kode dan desain

Seperti disebutkan sebelumnya, kode dan desain ZK dapat mengandung kerentanan. Kedua jenis kerentanan berpotensi membahayakan integritas sistem ZK, sehingga harus diatasi sebelum sistem dioperasikan. Satu masalah dengan sistem ZK, dibandingkan dengan sistem non-ZK, adalah bahwa setiap serangan lebih sulit untuk dideteksi dan dianalisis karena rincian komputasi mereka tidak tersedia untuk umum atau disimpan dalam rantai. Akibatnya, orang mungkin menyadari bahwa serangan hacker telah terjadi, tetapi mereka mungkin tidak tahu rincian teknis tentang bagaimana hal itu terjadi. Ini membuat biaya kerentanan ZK sangat tinggi. Akibatnya, nilai memastikan keamanan sistem ZK terlebih dahulu juga sangat tinggi.

Melakukan audit dan verifikasi formal

Dua kerentanan yang kita diskusikan di sini ditemukan melalui audit dan verifikasi formal. Beberapa orang mungkin berasumsi bahwa verifikasi formal saja meniadakan kebutuhan untuk audit karena semua kerentanan akan terdeteksi melalui verifikasi formal. Namun, rekomendasi kami adalah melakukan keduanya. Seperti yang dijelaskan di awal artikel ini, pekerjaan verifikasi formal berkualitas tinggi dimulai dengan tinjauan menyeluruh, inspeksi, dan penalaran informal tentang kode dan desain, yang tumpang tindih dengan audit. Selain itu, menemukan dan menyelesaikan kerentanan yang lebih sederhana selama audit dapat menyederhanakan dan merampingkan proses verifikasi formal.

Jika Anda melakukan audit dan verifikasi formal untuk sistem ZK, pendekatan optimal adalah melakukan keduanya secara bersamaan. Hal ini memungkinkan auditor dan insinyur verifikasi formal untuk berkolaborasi secara efisien, berpotensi menemukan lebih banyak kerentanan karena input audit berkualitas tinggi diperlukan untuk verifikasi formal.

Jika proyek ZK Anda telah menjalani audit (pujian) atau beberapa audit (pujian besar), saran kami adalah melakukan verifikasi formal di sirkuit berdasarkan hasil audit sebelumnya. Pengalaman kami dengan audit dan verifikasi formal dalam proyek-proyek seperti zkVM dan lainnya, baik ZK maupun non-ZK, telah berulang kali menunjukkan bahwa verifikasi formal sering kali menangkap kerentanan yang terlewatkan selama audit. Mengingat sifat ZKP, sementara sistem ZK harus menawarkan keamanan dan skalabilitas blockchain yang lebih baik daripada solusi non-ZK, kekritisan keamanan dan kebenarannya jauh lebih tinggi daripada sistem non-ZK tradisional. Oleh karena itu, nilai verifikasi formal berkualitas tinggi untuk sistem ZK jauh melebihi sistem non-ZK.

Pastikan keamanan sirkuit dan kontrak pintar

Aplikasi ZK biasanya terdiri dari dua komponen: sirkuit dan kontrak pintar. Untuk aplikasi berbasis zkVM, ada sirkuit zkVM universal dan aplikasi kontrak pintar. Untuk aplikasi yang tidak didasarkan pada zkVM, ada sirkuit ZK khusus aplikasi bersama dengan kontrak pintar terkait yang digunakan pada rantai L1 atau di ujung jembatan yang lain.

Upaya audit dan verifikasi formal kami untuk zkWasm hanya melibatkan sirkuit zkWasm. Namun, dari perspektif keamanan keseluruhan untuk aplikasi ZK, sangat penting untuk mengaudit dan memverifikasi kontrak pintar mereka secara formal juga. Bagaimanapun, akan sangat disesalkan jika, setelah menginvestasikan upaya signifikan untuk memastikan keamanan sirkuit, kelemahan dalam pengawasan kontrak pintar menyebabkan kompromi aplikasi.

Dua jenis kontrak pintar patut mendapat perhatian khusus. Tipe pertama langsung menangani bukti ZK. Meskipun mereka mungkin tidak berskala besar, risikonya sangat tinggi. Tipe kedua terdiri dari kontrak pintar skala menengah hingga besar yang berjalan di atas zkVM. Kami tahu bahwa kontrak ini terkadang bisa sangat kompleks, dan yang paling berharga harus menjalani audit dan verifikasi, terutama karena detail pelaksanaannya tidak terlihat secara on-chain. Untungnya, setelah bertahun-tahun pengembangan, verifikasi formal untuk kontrak pintar sekarang praktis dan siap untuk target bernilai tinggi yang sesuai.

Mari kita rangkum dampak verifikasi formal (FV) pada sistem ZK dan komponennya dengan poin-poin berikut.

Pernyataan:

1. Artikel ini direproduksi dari [panewslab], hak cipta milik penulis asli [CertiK], jika Anda keberatan dengan cetak ulang, silakan hubungi tim Gate Learn, dan tim akan menanganinya sesegera mungkin sesuai dengan prosedur yang relevan.

2. Penafian: Pandangan dan pendapat yang diungkapkan dalam artikel ini hanya mewakili pandangan pribadi penulis dan bukan merupakan saran investasi.

3. Versi bahasa lain dari artikel tersebut diterjemahkan oleh tim Gate Learn dan tidak disebutkan dalam Gate.io, artikel yang diterjemahkan tidak boleh direproduksi, didistribusikan atau dijiplak.