Pendahuluan

Keamanan Bitcoin, dan blockchain lainnya, seperti Liquid, bergantung pada penggunaan algoritma tanda tangan digital seperti ECDSA dan tanda tangan Schnorr. Sebuah pustaka C bernama libsecp256k1, dinamai sesuai dengan kurva eliptik tempat pustaka ini beroperasi, digunakan oleh Bitcoin Core dan Liquid, untuk menyediakan algoritma tanda tangan digital ini. Algoritma ini memanfaatkan perhitungan matematis yang disebut invers modular, yang merupakan komponen perhitungan yang relatif mahal.

Dalam “Perhitungan gcd waktu konstan cepat dan invers modular,” Daniel J. Bernstein dan Bo-Yin Yang mengembangkan algoritma invers modular baru. Pada tahun 2021, algoritma ini, yang disebut “safegcd,” diimplementasikan untuk libsecp256k1 oleh Peter Dettman. Sebagai bagian dari proses penilaian untuk algoritma baru ini, Blockstream Research adalah yang pertama menyelesaikan verifikasi formal dari desain algoritma tersebut dengan menggunakan asisten bukti Coq untuk secara formal memverifikasi bahwa algoritma tersebut benar-benar mengakhiri dengan hasil invers modular yang benar pada input 256-bit.

Kesenjangan antara Algoritma dan Implementasi

Upaya formalitas pada tahun 2021 hanya menunjukkan bahwa algoritma yang dirancang oleh Bernstein dan Yang berfungsi dengan benar. Namun, menggunakan algoritma tersebut di libsecp256k1 memerlukan implementasi deskripsi matematis dari algoritma safegcd dalam bahasa pemrograman C. Misalnya, deskripsi matematis dari algoritma melakukan perkalian matriks dari vektor yang dapat selebar integer bertanda 256 bit, namun bahasa pemrograman C hanya akan secara native menyediakan integer hingga 64 bit (atau 128 bit dengan beberapa ekstensi bahasa).

Mengimplementasikan algoritma safegcd memerlukan pemrograman perkalian matriks dan perhitungan lainnya menggunakan integer 64 bit C. Selain itu, banyak optimisasi lainnya telah ditambahkan untuk membuat implementasi cepat. 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 dioptimalkan untuk sistem 64 bit, dan dua algoritma waktu variabel untuk verifikasi tanda tangan, sekali lagi satu untuk sistem 32 bit dan satu untuk sistem 64 bit.

Verifiable C

Untuk memverifikasi bahwa kode C mengimplementasikan algoritma safegcd dengan benar, semua detail implementasi harus diperiksa. Kami menggunakan Verifiable C, bagian dari Verified Software Toolchain untuk penalaran tentang kode C menggunakan pembuktian teorema Coq.

Verifikasi dilakukan dengan menentukan precondition dan postcondition menggunakan logika pemisahan untuk setiap fungsi yang sedang diverifikasi. Logika pemisahan adalah logika yang dikhususkan untuk penalaran tentang subrutin, alokasi memori, konkurensi, dan lainnya.

Setelah setiap fungsi diberikan spesifikasi, verifikasi dilakukan dengan memulai dari precondition fungsi, dan menetapkan invarian baru setelah setiap pernyataan di dalam tubuh fungsi, sampai akhirnya menetapkan post condition di akhir tubuh fungsi atau di akhir setiap pernyataan pengembalian. Sebagian besar upaya formalitas dihabiskan “di antara” baris kode, menggunakan invarians untuk menerjemahkan operasi mentah setiap ekspresi C menjadi pernyataan tingkat tinggi tentang apa yang diwakili oleh struktur data yang dimanipulasi secara matematis. Misalnya, apa yang dianggap bahasa C sebagai array dari integer 64-bit mungkin sebenarnya adalah representasi dari integer 256-bit.

Hasil akhirnya adalah bukti formal, yang diverifikasi oleh asisten bukti Coq, bahwa implementasi waktu variabel 64-bit dari algoritma invers modular safegcd libsecp256k1 adalah benar secara fungsional.

Batasan Verifikasi

Ada beberapa batasan pada bukti kebenaran fungsional. Logika pemisahan yang digunakan dalam Verifiable C menerapkan apa yang dikenal sebagai kebenaran parsial. Itu berarti hanya membuktikan bahwa kode C mengembalikan hasil yang benar jika ia mengembalikan, tetapi tidak membuktikan penghentian itu sendiri. Kami mengurangi batasan ini dengan menggunakan bukti Coq sebelumnya tentang batasan pada algoritma safegcd untuk membuktikan bahwa nilai penghitung loop dari loop utama sebenarnya tidak pernah melebihi 11 iterasi.

Masalah lain adalah bahwa bahasa C itu sendiri tidak memiliki spesifikasi formal. Sebagai gantinya, proyek Verifiable C menggunakan proyek kompiler CompCert untuk memberikan spesifikasi formal dari bahasa C. Ini menjamin bahwa ketika program C yang telah diverifikasi dikompilasi dengan kompiler CompCert, kode assembly yang dihasilkan akan memenuhi spesifikasinya (tergantung pada batasan di atas). Namun, ini tidak menjamin bahwa kode yang dihasilkan oleh GCC, clang, atau kompiler lainnya akan berfungsi dengan baik. Misalnya, kompiler C diizinkan memiliki urutan evaluasi yang berbeda untuk argumen dalam pemanggilan fungsi. Dan bahkan jika bahasa C memiliki spesifikasi formal, setiap kompiler yang tidak diverifikasi secara formal masih dapat mengkompilasi program secara salah. Ini terjadi dalam praktik.

Terakhir, Verifiable C tidak mendukung pengoperasian struktur, mengembalikan struktur, atau menetapkan struktur. Sementara di libsecp256k1, struktur selalu diteruskan dengan pointer (yang diperbolehkan dalam Verifiable C), ada beberapa kesempatan di mana penetapan struktur digunakan. Untuk bukti kebenaran invers modular, ada 3 penetapan yang harus diganti dengan pemanggilan fungsi khusus yang melakukan penetapan struktur bidang demi bidang.

Ringkasan

Blockstream Research telah secara formal memverifikasi kebenaran fungsi invers modular libsecp256k1. Pekerjaan ini memberikan bukti lebih lanjut bahwa verifikasi kode C adalah mungkin dalam praktik. Menggunakan asisten bukti yang serbaguna memungkinkan kami untuk memverifikasi perangkat lunak yang dibangun di atas argumen matematis yang kompleks.

Tidak ada yang menghalangi sisa fungsi yang diimplementasikan di libsecp256k1 untuk diverifikasi juga. Jadi, adalah mungkin bagi libsecp256k1 untuk mendapatkan jaminan kebenaran perangkat lunak tertinggi yang mungkin.

Ini adalah posting tamu oleh Russell O’Connor dan Andrew Poelstra. Pendapat yang diungkapkan sepenuhnya adalah milik mereka sendiri dan tidak mencerminkan pendapat BTC Inc atau Bitcoin Magazine.

Sumber: Bitcoin Magazine

Implementasi Safegcd yang Diverifikasi Secara Formal muncul pertama kali di Crypto Breaking News.