perkenalan
Keamanan Bitcoin dan blockchain lain seperti Liquid bergantung pada penggunaan algoritma tanda tangan digital seperti tanda tangan ECDSA dan Schnorr. Perpustakaan AC yang disebut libsecp256k1, dinamai berdasarkan kurva elips tempat perpustakaan beroperasi, digunakan oleh Bitcoin Core dan Liquid untuk menyediakan algoritma tanda tangan digital ini. Algoritma ini menggunakan perhitungan matematis yang disebut a pembalikan modularyang merupakan komponen perhitungan yang relatif mahal.
Di dalam “Perhitungan gcd waktu konstan yang cepat dan inversi modular“Daniel J. Bernstein dan Bo-Yin Yang mengembangkan algoritma inversi modular baru. Pada tahun 2021, algoritma ini diperkenalkan yang disebut “safegcd”. dilaksanakan untuk libsecp256k1 oleh Peter Dettman. Sebagai bagian dari proses peninjauan algoritma baru ini, Blockstream Research adalah orang pertama yang menyelesaikannya tinjauan formal desain algoritme menggunakan Coq Proof Wizard untuk memverifikasi secara formal bahwa algoritme benar-benar diakhiri dengan hasil invers modular yang benar pada input 256-bit.
Kesenjangan antara algoritma dan implementasi
Upaya formalisasi pada tahun 2021 hanya menunjukkan bahwa algoritma yang dirancang oleh Bernstein dan Yang bekerja dengan benar. Namun, penggunaan algoritma ini di libsecp256k1 memerlukan penerapan deskripsi matematis dari algoritma Safegcd dalam bahasa pemrograman C. Misalnya, deskripsi matematis dari algoritma tersebut melakukan perkalian matriks vektor yang dapat mencakup bilangan bulat bertanda hingga 256-bit. Namun, bahasa pemrograman C secara native hanya menyediakan bilangan bulat hingga 64 bit (atau 128 bit untuk beberapa ekstensi bahasa).
Menerapkan algoritma Safegcd memerlukan pemrograman perkalian matriks dan perhitungan lainnya menggunakan bilangan bulat 64-bit C. masih banyak lagi optimasi ditambahkan untuk mempercepat implementasi. Pada akhirnya, ada empat implementasi terpisah dari algoritma Safegcd di libsecp256k1: dua algoritma waktu konstan untuk pembuatan tanda tangan, satu dioptimalkan untuk sistem 32-bit dan satu lagi dioptimalkan untuk sistem 64-bit, dan pada gilirannya dua algoritma waktu variabel untuk verifikasi tanda tangan satu untuk sistem 32-bit dan satu lagi untuk sistem 64-bit.
Dapat dideteksiC
Untuk memverifikasi apakah kode C mengimplementasikan algoritma Safegcd dengan benar, semua detail implementasi harus diperiksa. Kami menggunakan Dapat dideteksiCBagian dari Rantai Alat Perangkat Lunak Terverifikasi untuk memikirkan kode C menggunakan pembukti teorema Coq.
Verifikasi dilakukan dengan menentukan kondisi sebelum dan sesudah menggunakan logika pemisahan untuk setiap fungsi yang akan diverifikasi. Logika pemisahan adalah logika yang berspesialisasi dalam pertimbangan subprogram, alokasi memori, konkurensi, dan banyak lagi.
Setelah setiap fungsi menerima spesifikasi, verifikasi dimulai dengan prasyarat suatu fungsi dan membuat invarian baru setelah setiap pernyataan di badan fungsi, hingga akhirnya kondisi pasca ditetapkan di akhir badan fungsi atau di akhir setiap pengembalian. penyataan. Sebagian besar upaya formalisasi dihabiskan “di antara” baris kode, menggunakan invarian untuk menerjemahkan operasi mentah setiap ekspresi C ke dalam pernyataan tingkat tinggi tentang apa yang diwakili oleh struktur data yang dimanipulasi secara matematis. Misalnya, apa yang dianggap bahasa C sebagai array bilangan bulat 64-bit sebenarnya merupakan representasi dari bilangan bulat 256-bit.
Hasil akhirnya adalah untuk bukti formalDikonfirmasi oleh Coq Proof Wizard bahwa implementasi waktu variabel 64-bit dari algoritma inversi modular libsecp256k1 “safegcd” secara fungsional benar.
Keterbatasan Verifikasi
Ada beberapa keterbatasan untuk membuktikan kebenaran fungsional. Logika pemisahan yang digunakan dalam C yang Dapat Diverifikasi mengimplementasikan apa yang disebut Akurasi parsial. Artinya hanya membuktikan bahwa kode C memberikan hasil yang benar Jika ia kembali, tetapi tidak membuktikan penghentian itu sendiri. Kami mengurangi batasan ini dengan menggunakan bukti Coq kami sebelumnya batasan algoritma Safegcd untuk membuktikan bahwa nilai penghitung loop dari loop utama sebenarnya tidak pernah melebihi 11 iterasi.
Masalah lainnya adalah bahasa C sendiri tidak memiliki spesifikasi formal. Sebaliknya, proyek C yang Dapat Diverifikasi menggunakan Proyek kompiler CompCert Memberikan spesifikasi formal bahasa C. Hal ini menjamin bahwa ketika Anda mengkompilasi program C terverifikasi dengan kompiler CompCert, kode perakitan yang dihasilkan memenuhi spesifikasinya (tunduk pada peringatan di atas). Namun, ini tidak menjamin bahwa kode yang dihasilkan oleh GCC, Clang, atau kompiler lainnya akan berfungsi. Misalnya, kompiler C diperbolehkan memiliki urutan evaluasi berbeda untuk argumen dalam pemanggilan fungsi. Dan bahkan jika bahasa C memiliki spesifikasi formal, kompiler apa pun yang tidak diverifikasi secara formal dapat mengkompilasi program secara tidak benar. Itu berhasil terjadi dalam praktek.
Terakhir, C yang Dapat Diverifikasi tidak mendukung penerusan struct, pengembalian struct, atau penetapan struct. Meskipun struktur di libsecp256k1 selalu diteruskan dengan penunjuk (yang diperbolehkan di C yang Dapat Diverifikasi), ada beberapa kesempatan di mana penetapan struktur digunakan. Untuk pembuktian kebenaran invers modular, ada 3 penugasan yang harus diganti dengan pemanggilan fungsi khusus yang melakukan penugasan struktur bidang demi bidang.
Ringkasan
Blockstream Research telah secara resmi mengkonfirmasi kebenaran fungsi inversi modular libsecp256k1. Pekerjaan ini memberikan bukti lebih lanjut bahwa verifikasi kode C dimungkinkan dalam praktiknya. Dengan menggunakan asisten pembuktian umum, kami dapat memverifikasi perangkat lunak berdasarkan argumen matematika yang kompleks.
Tidak ada yang menghalangi fungsi lainnya yang diterapkan di libsecp256k1 untuk juga diperiksa. Hal ini memungkinkan libsecp256k1 memperoleh jaminan kebenaran perangkat lunak setinggi mungkin.
Ini adalah postingan tamu oleh Russell O’Connor dan Andrew Poelstra. Pendapat yang dikemukakan adalah sepenuhnya milik mereka sendiri dan tidak mencerminkan pendapat BTC Inc atau Majalah Bitcoin.