/ Tumpukan Perangkat Lunak Lengkap Web3 Verifikasi Formal Tingkat Lanjut/
CertiK baru-baru ini merilis laporan verifikasi formal tingkat lanjut pada modul Cosmos SDK Bank, yang, sepengetahuan kami, merupakan upaya pertama yang berhasil dalam verifikasi formal Cosmos SDK. Verifikasi formal adalah teknik yang menggunakan logika matematika untuk memastikan bahwa suatu sistem sesuai dengan spesifikasi sehingga berperilaku seperti yang diharapkan dalam semua masukan dan kondisi yang memungkinkan. Pada artikel ini, kami akan memperkenalkan langkah-langkah spesifik untuk memverifikasi modul Cosmos SDK Bank secara formal, serta beberapa hasil verifikasi.
Apa itu Cosmos SDK?
Cosmos Software Development Kit (disingkat SDK) adalah kerangka kerja yang memungkinkan pengembang membangun aplikasi blockchain khusus. Dengan menggunakan Cosmos SDK, pengembang dapat dengan mudah meluncurkan blockchain Layer 1 mereka sendiri tanpa harus mengkhawatirkan desain dan implementasi dari lapisan konsensus hingga lapisan aplikasi. Cosmos SDK menyediakan modul inti standar yang dapat langsung diimpor dan digunakan oleh rantai apa pun, seperti modul staking, auth, gov, dan mint.
sumber:
Modul bank
Modul bank di Cosmos SDK bertanggung jawab atas semua fungsi yang terkait dengan manajemen token, seperti transfer token asli. Pengiriman token harus memenuhi banyak batasan dan ketentuan. Misalnya, akun harus memiliki ketersediaan token yang memadai, tidak termasuk token yang telah dipertaruhkan, dikunci, atau dalam proses pelepasan paket. Dengan dukungan modul seperti staking dan auth, modul bank mengatur seluruh proses pengiriman token. Meskipun modul bank bergantung pada beberapa modul lainnya, karena modul tersebut tidak berada dalam cakupan verifikasi formal ini, kami membuat beberapa asumsi tentang fungsinya untuk menyederhanakan proses.
Modul bank SDK terdiri dari beberapa sub-modul, termasuk penjaga dan tipe, yang merupakan komponen inti yang menentukan perilaku modul dan tipe data. Kami akan fokus pada submodul penjaga karena mencakup fungsi dan fitur utama modul.
Submodul penjaga memiliki dua komponen utama: lihat dan kirim. Penjaga tampilan bertanggung jawab untuk mengelola akun dan saldo, sedangkan penjaga pengiriman bertanggung jawab untuk mengubah saldo akun, seperti mentransfer dan mempertaruhkan token yang terkunci atau tidak terkunci. Aliran modul bank ditunjukkan pada gambar di bawah ini, dan panah menunjukkan arah dari komponen ke fungsi atau Keeper.
sumber:
Metode autentikasi
Seperti disebutkan sebelumnya, cakupan verifikasi ini terbatas pada modul bank. Sebelum verifikasi dimulai, terlebih dahulu kita merumuskan spesifikasi formal untuk tipe data pada modul bank. Misalnya, terdapat struktur data token di modul bank, yang berisi denominasi tipe string dan jumlah tipe big.Int, yang didefinisikan dalam kode sumber sebagai berikut:
Strukturnya sederhana, dan kami mendefinisikannya dalam Coq (bahasa pemodelan dan verifikasi formal kami) sebagai berikut:
Berdasarkan definisi ini, pertama-tama kami membuktikan beberapa properti tentang operasi dasar koin untuk meletakkan dasar bagi integritas fungsional modul bank, karena memerlukan modifikasi dan manipulasi jenis koin yang sering. Misalnya:
Lemma ini membuktikan invarian mendasar: mengurangkan dua koin tidak mengubah denominasinya, juga tidak menyebabkan saldo negatif.
Mirip dengan contoh sebelumnya, komponen dasar setiap transisi keadaan dimodelkan dalam Coq, termasuk KV Store, GasMeter, Error Handling, dan Context.
Untuk spesifikasi detail tipe data dan verifikasinya, silakan lihat:
Modelkan penjaganya
Setelah menyelesaikan pemodelan komponen dasar, kita dapat memodelkan penjaga inti modul bank untuk menjelaskan fungsi modul. Penjaga bank memiliki dua antarmuka, satu untuk akses baca-saja ke data token dan yang lainnya untuk transfer token dan pemeliharaan pasokan.
View keeper bertanggung jawab menangani akses read-only ke saldo akun dan berisi empat fungsi untuk menghitung saldo akun:
GetBalance: Kueri saldo akun denominasi tertentu melalui alamat. Ini mempertimbangkan dua kasus: urutan byte nol dan urutan byte bukan nol. Verifikasi formal memastikan bahwa fungsi GetBalance memberikan hasil yang benar dalam kedua kasus.
LockedCoins: Mengembalikan semua token akun yang tidak dapat dikonsumsi sesuai dengan alamat. Karena keterbatasan waktu, kami membuat asumsi tentang beberapa implementasi dari modul auth.
GetAllBalances: Mengembalikan semua saldo akun di bawah alamat yang ditentukan.
GetAccountsBalances: Mengembalikan semua saldo akun dari penyimpanan, dan mengambil bidang BAddress dan BCoins sebagai catatan.
Manajer Pengiriman menangani transfer dan pasokan token. Selama transfer, ia mempertahankan pasokan token sehingga tidak ada token baru yang dicetak.
SetBalance: Mengatur saldo token untuk akun melalui alamat. Fungsi ini mempertimbangkan dua kasus: saldo disetel ke nol dan saldo disetel ke bukan nol. Dalam kedua kasus tersebut, kebenaran SetBalance terbukti.
subUnlockedCoin: Mengurangi jumlah (token) yang ditentukan dari sebuah alamat. Fungsi rekursif subUnlockedCoins melakukan operasi yang sama pada sekumpulan koin. Properti yang relevan dari fungsi-fungsi ini dianggap sebagai asumsi aksiomatik.
addCoin: Tambahkan jumlah (token) yang ditentukan ke alamat. Fungsi rekursif addCoins melakukan operasi yang sama pada sekumpulan koin. Properti yang relevan dari fungsi-fungsi ini dianggap sebagai asumsi aksiomatik.
SendCoins: Mengirim uang dari satu alamat akun ke alamat akun lainnya, sehingga emas di kedua alamat tersebut terupdate. Jika penerima tidak ada, akun baru akan dibuat untuknya.
Dengan menggunakan model komponen inti di atas, kita dapat memulai verifikasi.
Proses verifikasi
Verifikasi kami dilakukan dengan mendeskripsikan secara formal properti invarian dari fungsi-fungsi ini dan membuktikannya dalam sistem pembuktian tambahan, dengan fokus utama pada fungsi inti "View Keeper" dan "Send Keeper".
Misalnya, spesifikasi dan lemma setBalance_ok membuktikan kebenaran fungsi setBalance dari modul BaseSendKeeper, secara khusus membuktikan properti berikut:
Ketika send.setBalance kembali ke status "Ok", terdapat MultiStore baru.Pada saat ini, lingkungan uctx yang diperbarui berasal dari lingkungan lama asli ctx dengan memperbarui MultiStore baru.
Saldo yang ditetapkan adalah token yang valid (memiliki properti token yang diperlukan dalam sistem).
Hubungan setBalance_prop dipertahankan untuk memastikan bahwa fungsi memperbarui saldo di newMultiStore dengan cara yang diharapkan dan menghasilkan uctx lingkungan yang diperbarui.
Setelah pengaturan saldo selesai, gunakan alamat akun dan saldo denominasi (Denom) untuk memanggil view.GetBalance pada lingkungan uctx yang diperbarui, dan saldo yang sama yang ditetapkan oleh send.setBalance akan dikembalikan.
Properti ini dijelaskan dalam bahasa spesifikasi Coq sebagai berikut:
Untuk kode Coq properti lainnya, kunjungi:
karir masa depan
Landasan verifikasi ini dibangun atas beberapa asumsi dan aksioma yang dapat kita verifikasi lebih dalam untuk memperluas cakupan verifikasi. Pekerjaan di masa depan berfokus pada bidang-bidang berikut:
Verifikasi asumsi: Verifikasi saat ini mengandalkan serangkaian asumsi sebagai dasar pembuktian. Asumsi ini dapat diuji di masa depan untuk memastikan bahwa asumsi tersebut secara akurat mencerminkan perilaku dan properti sistem yang diinginkan.
Verifikasi modul Auth: Modul ini bertanggung jawab untuk mengelola data akun dan mekanisme tanda tangan, dan merupakan komponen inti dari Cosmos SDK. Kedepannya dapat diverifikasi sepenuhnya secara formal untuk memastikan implementasi modul dan interaksi dengan modul lain akurat.
Lebih banyak teorema tentang menitipkan, mencetak, dan menjual koin: Memperluas cakupan verifikasi dan memperkenalkan lebih banyak teorema tentang menitipkan, mencetak, dan menjual koin akan membantu untuk memahami mekanisme operasi sistem secara lebih komprehensif. Teorema ini dapat dikombinasikan dengan verifikasi modul autentikasi untuk memastikan konsistensi dan kebenaran sistem secara keseluruhan.
Memperluas seluruh infrastruktur Cosmos SDK: pekerjaan verifikasi pada tahap ini terutama difokuskan pada modul bank dan komponen terkait. Di masa depan, proses verifikasi formal dapat diperluas ke seluruh infrastruktur Cosmos SDK, sehingga meningkatkan akurasi, keamanan, dan stabilitas platform secara keseluruhan, serta menyediakan lingkungan yang lebih stabil dan andal bagi pengembang dan pengguna.
Integrasikan dengan modul lain: Karena Cosmos SDK menyertakan berbagai modul yang saling berhubungan, akan sangat bermanfaat untuk mengeksplorasi interaksi dan ketergantungan di antara modul-modul tersebut. Hal ini memerlukan verifikasi kebenaran interaksi antar modul dan memastikan bahwa perubahan apa pun pada satu modul tidak berdampak buruk pada modul lainnya.
Pemodelan dan verifikasi mekanisme insentif: Cosmos SDK juga mengintegrasikan mekanisme insentif seperti staking dan distribusi hadiah. Penelitian di masa depan akan memodelkan dan memvalidasi mekanisme ini untuk memastikan mekanisme tersebut benar dan konsisten dengan insentif ekonomi yang diharapkan.
Makalah ini menyajikan kasus pertama yang berhasil dari verifikasi formal tingkat lanjut dari modul Cosmos SDKbank, yang menghasilkan kerja efektif untuk landasan keamanan dan keandalan ekosistem blockchain. Pekerjaan di masa depan akan memperluas pencapaian ini dengan memvalidasi asumsi, memvalidasi modul lain, dan mencakup seluruh infrastruktur Cosmos SDK, yang pada akhirnya membangun platform yang lebih solid dan kredibel bagi pengembang dan pengguna.
Lihat Asli
Halaman ini mungkin berisi konten pihak ketiga, yang disediakan untuk tujuan informasi saja (bukan pernyataan/jaminan) dan tidak boleh dianggap sebagai dukungan terhadap pandangannya oleh Gate, atau sebagai nasihat keuangan atau profesional. Lihat Penafian untuk detailnya.
Penjelasan mendetail tentang verifikasi formal modul standar Cosmos SDK
/ Tumpukan Perangkat Lunak Lengkap Web3 Verifikasi Formal Tingkat Lanjut/
CertiK baru-baru ini merilis laporan verifikasi formal tingkat lanjut pada modul Cosmos SDK Bank, yang, sepengetahuan kami, merupakan upaya pertama yang berhasil dalam verifikasi formal Cosmos SDK. Verifikasi formal adalah teknik yang menggunakan logika matematika untuk memastikan bahwa suatu sistem sesuai dengan spesifikasi sehingga berperilaku seperti yang diharapkan dalam semua masukan dan kondisi yang memungkinkan. Pada artikel ini, kami akan memperkenalkan langkah-langkah spesifik untuk memverifikasi modul Cosmos SDK Bank secara formal, serta beberapa hasil verifikasi.
Apa itu Cosmos SDK?
Cosmos Software Development Kit (disingkat SDK) adalah kerangka kerja yang memungkinkan pengembang membangun aplikasi blockchain khusus. Dengan menggunakan Cosmos SDK, pengembang dapat dengan mudah meluncurkan blockchain Layer 1 mereka sendiri tanpa harus mengkhawatirkan desain dan implementasi dari lapisan konsensus hingga lapisan aplikasi. Cosmos SDK menyediakan modul inti standar yang dapat langsung diimpor dan digunakan oleh rantai apa pun, seperti modul staking, auth, gov, dan mint.
sumber:
Modul bank
Modul bank di Cosmos SDK bertanggung jawab atas semua fungsi yang terkait dengan manajemen token, seperti transfer token asli. Pengiriman token harus memenuhi banyak batasan dan ketentuan. Misalnya, akun harus memiliki ketersediaan token yang memadai, tidak termasuk token yang telah dipertaruhkan, dikunci, atau dalam proses pelepasan paket. Dengan dukungan modul seperti staking dan auth, modul bank mengatur seluruh proses pengiriman token. Meskipun modul bank bergantung pada beberapa modul lainnya, karena modul tersebut tidak berada dalam cakupan verifikasi formal ini, kami membuat beberapa asumsi tentang fungsinya untuk menyederhanakan proses.
Modul bank SDK terdiri dari beberapa sub-modul, termasuk penjaga dan tipe, yang merupakan komponen inti yang menentukan perilaku modul dan tipe data. Kami akan fokus pada submodul penjaga karena mencakup fungsi dan fitur utama modul.
Submodul penjaga memiliki dua komponen utama: lihat dan kirim. Penjaga tampilan bertanggung jawab untuk mengelola akun dan saldo, sedangkan penjaga pengiriman bertanggung jawab untuk mengubah saldo akun, seperti mentransfer dan mempertaruhkan token yang terkunci atau tidak terkunci. Aliran modul bank ditunjukkan pada gambar di bawah ini, dan panah menunjukkan arah dari komponen ke fungsi atau Keeper.
sumber:
Metode autentikasi
Seperti disebutkan sebelumnya, cakupan verifikasi ini terbatas pada modul bank. Sebelum verifikasi dimulai, terlebih dahulu kita merumuskan spesifikasi formal untuk tipe data pada modul bank. Misalnya, terdapat struktur data token di modul bank, yang berisi denominasi tipe string dan jumlah tipe big.Int, yang didefinisikan dalam kode sumber sebagai berikut:
Strukturnya sederhana, dan kami mendefinisikannya dalam Coq (bahasa pemodelan dan verifikasi formal kami) sebagai berikut:
Berdasarkan definisi ini, pertama-tama kami membuktikan beberapa properti tentang operasi dasar koin untuk meletakkan dasar bagi integritas fungsional modul bank, karena memerlukan modifikasi dan manipulasi jenis koin yang sering. Misalnya:
Lemma ini membuktikan invarian mendasar: mengurangkan dua koin tidak mengubah denominasinya, juga tidak menyebabkan saldo negatif.
Mirip dengan contoh sebelumnya, komponen dasar setiap transisi keadaan dimodelkan dalam Coq, termasuk KV Store, GasMeter, Error Handling, dan Context.
Untuk spesifikasi detail tipe data dan verifikasinya, silakan lihat:
Modelkan penjaganya
Setelah menyelesaikan pemodelan komponen dasar, kita dapat memodelkan penjaga inti modul bank untuk menjelaskan fungsi modul. Penjaga bank memiliki dua antarmuka, satu untuk akses baca-saja ke data token dan yang lainnya untuk transfer token dan pemeliharaan pasokan.
View keeper bertanggung jawab menangani akses read-only ke saldo akun dan berisi empat fungsi untuk menghitung saldo akun:
GetBalance: Kueri saldo akun denominasi tertentu melalui alamat. Ini mempertimbangkan dua kasus: urutan byte nol dan urutan byte bukan nol. Verifikasi formal memastikan bahwa fungsi GetBalance memberikan hasil yang benar dalam kedua kasus.
LockedCoins: Mengembalikan semua token akun yang tidak dapat dikonsumsi sesuai dengan alamat. Karena keterbatasan waktu, kami membuat asumsi tentang beberapa implementasi dari modul auth.
GetAllBalances: Mengembalikan semua saldo akun di bawah alamat yang ditentukan.
GetAccountsBalances: Mengembalikan semua saldo akun dari penyimpanan, dan mengambil bidang BAddress dan BCoins sebagai catatan.
Manajer Pengiriman menangani transfer dan pasokan token. Selama transfer, ia mempertahankan pasokan token sehingga tidak ada token baru yang dicetak.
SetBalance: Mengatur saldo token untuk akun melalui alamat. Fungsi ini mempertimbangkan dua kasus: saldo disetel ke nol dan saldo disetel ke bukan nol. Dalam kedua kasus tersebut, kebenaran SetBalance terbukti.
subUnlockedCoin: Mengurangi jumlah (token) yang ditentukan dari sebuah alamat. Fungsi rekursif subUnlockedCoins melakukan operasi yang sama pada sekumpulan koin. Properti yang relevan dari fungsi-fungsi ini dianggap sebagai asumsi aksiomatik.
addCoin: Tambahkan jumlah (token) yang ditentukan ke alamat. Fungsi rekursif addCoins melakukan operasi yang sama pada sekumpulan koin. Properti yang relevan dari fungsi-fungsi ini dianggap sebagai asumsi aksiomatik.
SendCoins: Mengirim uang dari satu alamat akun ke alamat akun lainnya, sehingga emas di kedua alamat tersebut terupdate. Jika penerima tidak ada, akun baru akan dibuat untuknya.
Dengan menggunakan model komponen inti di atas, kita dapat memulai verifikasi.
Proses verifikasi
Verifikasi kami dilakukan dengan mendeskripsikan secara formal properti invarian dari fungsi-fungsi ini dan membuktikannya dalam sistem pembuktian tambahan, dengan fokus utama pada fungsi inti "View Keeper" dan "Send Keeper".
Misalnya, spesifikasi dan lemma setBalance_ok membuktikan kebenaran fungsi setBalance dari modul BaseSendKeeper, secara khusus membuktikan properti berikut:
Ketika send.setBalance kembali ke status "Ok", terdapat MultiStore baru.Pada saat ini, lingkungan uctx yang diperbarui berasal dari lingkungan lama asli ctx dengan memperbarui MultiStore baru.
Saldo yang ditetapkan adalah token yang valid (memiliki properti token yang diperlukan dalam sistem).
Hubungan setBalance_prop dipertahankan untuk memastikan bahwa fungsi memperbarui saldo di newMultiStore dengan cara yang diharapkan dan menghasilkan uctx lingkungan yang diperbarui.
Setelah pengaturan saldo selesai, gunakan alamat akun dan saldo denominasi (Denom) untuk memanggil view.GetBalance pada lingkungan uctx yang diperbarui, dan saldo yang sama yang ditetapkan oleh send.setBalance akan dikembalikan.
Properti ini dijelaskan dalam bahasa spesifikasi Coq sebagai berikut:
Untuk kode Coq properti lainnya, kunjungi:
karir masa depan
Landasan verifikasi ini dibangun atas beberapa asumsi dan aksioma yang dapat kita verifikasi lebih dalam untuk memperluas cakupan verifikasi. Pekerjaan di masa depan berfokus pada bidang-bidang berikut:
Verifikasi asumsi: Verifikasi saat ini mengandalkan serangkaian asumsi sebagai dasar pembuktian. Asumsi ini dapat diuji di masa depan untuk memastikan bahwa asumsi tersebut secara akurat mencerminkan perilaku dan properti sistem yang diinginkan.
Verifikasi modul Auth: Modul ini bertanggung jawab untuk mengelola data akun dan mekanisme tanda tangan, dan merupakan komponen inti dari Cosmos SDK. Kedepannya dapat diverifikasi sepenuhnya secara formal untuk memastikan implementasi modul dan interaksi dengan modul lain akurat.
Lebih banyak teorema tentang menitipkan, mencetak, dan menjual koin: Memperluas cakupan verifikasi dan memperkenalkan lebih banyak teorema tentang menitipkan, mencetak, dan menjual koin akan membantu untuk memahami mekanisme operasi sistem secara lebih komprehensif. Teorema ini dapat dikombinasikan dengan verifikasi modul autentikasi untuk memastikan konsistensi dan kebenaran sistem secara keseluruhan.
Memperluas seluruh infrastruktur Cosmos SDK: pekerjaan verifikasi pada tahap ini terutama difokuskan pada modul bank dan komponen terkait. Di masa depan, proses verifikasi formal dapat diperluas ke seluruh infrastruktur Cosmos SDK, sehingga meningkatkan akurasi, keamanan, dan stabilitas platform secara keseluruhan, serta menyediakan lingkungan yang lebih stabil dan andal bagi pengembang dan pengguna.
Integrasikan dengan modul lain: Karena Cosmos SDK menyertakan berbagai modul yang saling berhubungan, akan sangat bermanfaat untuk mengeksplorasi interaksi dan ketergantungan di antara modul-modul tersebut. Hal ini memerlukan verifikasi kebenaran interaksi antar modul dan memastikan bahwa perubahan apa pun pada satu modul tidak berdampak buruk pada modul lainnya.
Pemodelan dan verifikasi mekanisme insentif: Cosmos SDK juga mengintegrasikan mekanisme insentif seperti staking dan distribusi hadiah. Penelitian di masa depan akan memodelkan dan memvalidasi mekanisme ini untuk memastikan mekanisme tersebut benar dan konsisten dengan insentif ekonomi yang diharapkan.
Makalah ini menyajikan kasus pertama yang berhasil dari verifikasi formal tingkat lanjut dari modul Cosmos SDKbank, yang menghasilkan kerja efektif untuk landasan keamanan dan keandalan ekosistem blockchain. Pekerjaan di masa depan akan memperluas pencapaian ini dengan memvalidasi asumsi, memvalidasi modul lain, dan mencakup seluruh infrastruktur Cosmos SDK, yang pada akhirnya membangun platform yang lebih solid dan kredibel bagi pengembang dan pengguna.