Pada bulan Juni 2016, kegembiraan memuncak karena “DAO,” yang dibangun di atas blockchain Ethereum, akan menjadi dana investasi terdesentralisasi dan sepenuhnya digital pertama di dunia.

Namun dalam beberapa minggu, ia malah menjadi contoh utama peretasan DeFi setelah penyerang mencuri ether senilai $50 juta darinya.

Untuk memecahkan DAO, penyerang mengeksploitasi apa yang disebut kerentanan reentrancy, yaitu kerentanan konkurensi di mana satu metode kontrak pintar tertentu dipanggil sementara metode lain masih dijalankan, dan DAO hanyalah bagian dari pengembangan jangka panjang dari DAO. kontrak pintar Yang pertama, mengalami kesalahan seperti itu.

Penerus terkemuka termasuk Uniswap/Lendf.Me, yang telah mencuri $25 juta pada tahun 2020, CREAM, yang telah mencuri $18 juta pada tahun 2021, dan Fei, yang telah mencuri $80 juta pada tahun 2022.

Alasan mengapa bug ini tetap ada adalah karena bug ini dapat melibatkan interaksi kode tak terduga yang tersebar di seluruh kontrak pintar, bahkan terkadang di seluruh kontrak pintar yang berbeda. Jumlah interaksi kode tersebut bisa sangat besar, sehingga menyulitkan manusia untuk mendeteksi dan menghilangkan kontrak pintar yang tidak diinginkan .kode diperlukan.

Selain itu, interaksi ini seringkali sulit untuk diuji secara otomatis dan sistematis.

TLA+: Pembasmi

Masukkan Logika Tindakan Temporal (TLA+), sebuah bahasa untuk menentukan dan memvalidasi sistem yang kompleks. TLA+ tidak hanya menemukan kesalahan tetapi juga memverifikasi keberadaannya.

Bagaimana ini mungkin, Anda bertanya? TLA+ hadir dengan seperangkat alat untuk verifikasi formal ringan dalam bentuk yang disebut pemeriksaan model. Melalui pemeriksaan model, ia secara mendalam mengeksplorasi semua kemungkinan interaksi bersamaan dari model kode - area yang sangat sulit untuk diuji - dan menemukan bug.

Bayangkan seorang pembasmi hama yang menerangi setiap sudut dan celah untuk mengekspos dan menghilangkan hama yang tidak diinginkan yang bersembunyi di sudut-sudut gelap yang sering diabaikan atau diabaikan. Yang penting, setelah model kode dibuat, pemeriksaan model hampir tidak memerlukan masukan manusia untuk dijalankan, sehingga sangat hemat biaya.

Sebagai ilustrasi dengan beberapa angka yang dibuat-buat: Jika praktik standar industri seperti pengujian dan tinjauan keamanan menghilangkan 80% bug, dan verifikasi formal "kelas berat" menghilangkan 99%, maka penggunaan TLA+ menghilangkan 90% hanya dengan satu sejumlah kecil upaya verifikasi kelas berat.

TLA+ dan Komputer Internet

Tim teknik kami menggunakan TLA+ untuk menganalisis semua aspek komputasi Internet, termasuk kontrak pintar yang sangat penting bagi keamanan yang berjalan di platform. Meskipun komputer Ethereum dan Internet memiliki model eksekusi yang berbeda, kesalahan masuk kembali dapat muncul dalam kontrak pintar di kedua blockchain.

Faktanya, karena throughputnya yang tinggi, komputer Internet memungkinkan beberapa panggilan bersamaan ke satu kontrak pintar, sehingga pembuat kontrak pintar harus lebih berhati-hati untuk menghilangkan interaksi bersamaan yang tidak diinginkan. Karena keamanan sangat penting bagi keberhasilan komputer di Internet, TLA+ digunakan di banyak kontrak pintar untuk mendeteksi kesalahan selama fase pengembangan.

Wadah analisis TLA+ (kontrak pintar untuk komputer di internet) baru-baru ini dilakukan pada Chain-Key Bitcoin (ckBTC) yang baru dirilis, yang hasilnya akan saya bagikan di bawah.

Kontrak pintar ckBTC

Untuk membahas analisis TLA+ terhadap ckBTC, mari kita mulai dengan ikhtisar tingkat tinggi tentang ckBTC. ckBTC adalah token asli komputer internet yang didukung secara aman oleh Bitcoin (BTC) dengan rasio 1:1.

Buku besar ckBTC adalah kontrak pintar kontainer di blockchain komputer Internet yang melacak berapa banyak ckBTC yang dimiliki setiap pengguna akhir. Buku besar yang sama ini memungkinkan pengguna akhir untuk mentransfer ckBTC mereka ke pengguna akhir lainnya dengan lebih cepat dan lebih murah daripada mentransfer BTC di jaringan Bitcoin.

Untuk mengonversi ckBTC ke BTC dan sebaliknya, pengguna akhir berinteraksi dengan kontrak pintar yang berbeda, pembuat ckBTC.

Pada tingkat tinggi, operasi konversi dari BTC ke ckBTC terlihat seperti ini:

Langkah-langkah untuk mendapatkan ckBTC:

1. Pengguna akhir pertama-tama mentransfer sejumlah BTC ke alamat setoran Bitcoin khusus pengguna, semua alamat setoran sepenuhnya dikontrol oleh kode wadah cerdas pembuat ckBTC karena kunci rantai tanda tangan ECDSA, yang menciptakan UTXO baru yang dimiliki oleh setoran tersebut alamat;

2. Pengguna akhir memberi tahu kontrak pintar ckBTC mint tentang UTXO yang baru disimpan dengan meminta mint untuk memperbarui saldo pengguna;

3. Kontrak cerdas pembuatnya kemudian menggunakan integrasi Bitcoin pada komputer Internet untuk mengambil semua UTXO yang dimiliki oleh alamat penyimpanan yang dikontrol oleh pembuatnya namun khusus untuk pengguna daftar pembukuan internal UTXO yang telah diprosesnya;

4. Terakhir, pembuatnya menginstruksikan buku besar untuk mencetak ckBTC baru untuk semua UTXO baru dengan rasio 1:1, dan setelah selesai, ia menambahkan UTXO yang baru ditemukan ke daftar UTXO yang diproses.

Penafian: Proses di atas menghilangkan proses KYT (Kenali Transaksi Anda) demi kesederhanaan.

Kontrak pintar ckBTC bertemu dengan TLA+

Gambaran tingkat tinggi yang disajikan di atas sebenarnya menyembunyikan masalah konkurensi yang tidak kentara, dan kabar baiknya adalah kita dapat mendeteksi masalah tersebut menggunakan toolkit TLA+.

Namun sebelum TLA+ dapat mendeteksi apa pun, kita harus menyediakan dua hal terlebih dahulu:

  • Buat model sistem kami menggunakan bahasa TLA+

  • Tentukan properti TLA+ yang kami harapkan akan diterapkan oleh sistem

Model ini adalah versi sistem yang disederhanakan namun tetap terdefinisi sepenuhnya, yang dalam kasus kami mencakup kontrak pintar minter, tetapi juga semua bagian sistem terkait lainnya, yaitu kontrak buku besar dan jaringan Bitcoin.

Untuk setiap komponen, kami memodelkan statusnya dan bagaimana tindakan relevan yang mungkin dilakukan pengguna akhir (yaitu mentransfer BTC atau ckBTC, menyetor BTC, atau melakukan tindakan berbeda yang dilakukan oleh pembuatnya) mengubah statusnya.

Semua elemen ini agak disederhanakan dalam model, dengan bagian-bagian yang menjadi fokus analisis (misalnya kode minter) dimodelkan secara lebih rinci, sementara bagian lain (misalnya jaringan Bitcoin) dimodelkan dengan kurang rinci, pada kenyataannya, model TLA+ mirip dengan spesifikasi desain rinci suatu sistem.

Secara intuitif, fitur utama yang ingin kami terapkan adalah memastikan bahwa ckBTC kami didukung sepenuhnya. Dengan kata lain, tidak ada pengguna akhir yang dapat “menghabiskan dua kali lipat” BTC yang mereka setorkan untuk mendapatkan lebih banyak ckBTC daripada yang mereka setorkan.

Namun untuk menganalisis properti seperti itu, kita harus membuat intuisi ini sangat tepat dengan mengungkapkannya secara formal dalam bahasa TLA+. Definisi formal kami adalah bahwa total pasokan ckBTC (yaitu, jumlah seluruh saldo ckBTC pengguna akhir, sebagaimana disimpan oleh buku besar ckBTC) tidak melebihi jumlah total BTC yang dikendalikan oleh wadah pencetakan (yaitu, nilai semua UTXO dimiliki oleh alamat deposit) .

Deteksi dan selesaikan masalah

Setelah kita membuat model dan properti, toolkit TLA+ dapat menganalisis model. Untuk menjalankan analisis, pertama-tama kita tentukan pengaturan untuk menjalankan analisis. Misalnya, pengaturan kami untuk ckBTC hanya mencakup dua pengguna akhir yang berbeda, dan sejumlah kecil dari total pasokan Bitcoin (misalnya, 5 satoshi).

Meskipun pengaturan ini sangat terbatas, studi empiris menunjukkan bahwa sebagian besar masalah dalam sistem komputer dapat ditemukan di sejumlah kecil entitas. Pengaturan kecil memungkinkan analisis untuk secara sistematis mengeksplorasi semua kemungkinan rangkaian tindakan yang ditentukan oleh model dan memeriksa apakah properti yang ditentukan berlaku dalam urutan tersebut.

Selain itu, analisis berjalan sepenuhnya secara otomatis, yaitu tidak memerlukan masukan manusia apa pun, dan jika properti ini tidak berlaku, analisis ini memberi kita urutan operasi yang tepat yang melanggar properti tersebut.

Misalnya, analisis dapat mengungkapkan bahwa kami dapat melanggar properti "tidak ada ckBTC tanpa jaminan" dalam skenario seperti yang digambarkan di bawah ini:

Di Sini:

  • Pengguna akhir menyetor BTC, sama seperti sebelumnya;

  • Namun, sekarang pengguna akhir kemudian menginstruksikan pembuat ckBTC untuk memperbarui saldo dua kali berturut-turut, dan di komputer internet, pembaruan ini dapat berinteraksi dengan kontrak pintar lainnya secara bersamaan;

  • Dua pembaruan yang berjalan secara bersamaan menanyakan jaringan Bitcoin untuk semua UTXO yang disimpan oleh pengguna akhir, dan keduanya menerima respons UTXO yang sama yang disimpan pada langkah 1. Karena UTXO belum ada dalam daftar "diproses", kedua pembaruan tersebut menganggap UTXO baru;

  • Kedua pembaruan tersebut menginstruksikan buku besar untuk mencetak jumlah ckBTC yang sesuai pada langkah 4.

Oleh karena itu, pada akhir langkah 4, kami berada dalam keadaan di mana pasokan ckBTC dua kali lipat jumlah UTXO di alamat deposit, yang melanggar properti "tidak ada ckBTC yang tidak didukung".

Perhatikan bahwa kesalahan ini hanya terjadi karena pembaruan pada saldo pengguna akhir dijalankan secara bersamaan - ini sebenarnya merupakan kesalahan masuk kembali dengan gaya yang sama seperti yang menyebabkan DAO mati.

Salah satu cara untuk mengatasi masalah ini adalah dengan mencegah pembaruan saldo berjalan secara paralel untuk pengguna akhir yang sama, kita dapat melakukan ini dengan meminta pembuat menyimpan pengguna akhir dalam daftar pengguna yang "terkunci" ketika pembaruan saldo dimulai, dan menyimpannya di sana. selama durasi daftar pembaruan untuk mencapai hal ini.

Jika pengguna akhir mencoba untuk memulai pembaruan saldo bersamaan lainnya, pembaruan pertama-tama akan memeriksa dan menemukan pengguna akhir spesifik ini dalam daftar pengguna yang terkunci, lalu dibatalkan.

Perhatikan bahwa kami sedikit menyederhanakan serangan di sini: penguncian sebenarnya adalah pola yang cukup umum untuk kontrak pintar IC, dan pembuat ckBTC telah menerapkannya sejak awal. Namun, penguncian yang tidak dilakukan dengan benar akan membuka pintu bagi serangan di atas, yang dapat dideteksi oleh TLA+.

Selain itu, kami menemukan beberapa kasus edge yang melanggar "tidak ada ckBTC yang tidak didukung" dan properti penting lainnya, dan setelah kami menerapkan semua perbaikan, TLA+ dapat memverifikasi dan mengonfirmasi bahwa tidak ada lagi pelanggaran properti dalam pengaturan yang kami tentukan.

Haruskah Anda menggunakan TLA+ untuk kontrak pintar Anda?

Sangat! Oke, oke, mungkin saya harus memberikan jawaban yang lebih bernuansa, yang digunakan tim R&D kami untuk kontrak pintar penting di komputer Internet setiap kali melibatkan konkurensi non-sepele.

Misalnya, analisis TLA+ menemukan bug konkurensi halus di Tata Kelola Komputer Internet dan Wadah Buku Besar yang terlewatkan dalam tinjauan keamanan manual sebelumnya dan dapat menyebabkan masalah, kasus, dan poin yang signifikan — TLA+ berperan penting dalam mengungkap masalah pelik tersebut.

Tentu saja, ada harga yang harus dibayar dalam hal memperoleh pengetahuan dan kemudian membangun modelnya, namun secara empiris harga tersebut masuk akal, terutama mengingat sifat keamanan blockchain yang berisiko tinggi.

Seseorang tidak boleh terintimidasi oleh bahasa TLA+ itu sendiri, meskipun namanya menakutkan, mengakses fitur-fitur canggihnya cukup sederhana. Faktanya, lembar contekan TLA+ yang menjelaskan hampir semua fitur TLA+ secara kasar dapat dimuat dalam satu halaman:

  • mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html

Terlebih lagi, upaya yang diperlukan untuk membangun model ini sebanding dengan tinjauan keamanan manual standar. Misalnya, untuk pembuat ckBTC, dibutuhkan total sekitar 3 minggu bagi 1 orang untuk memahami desain, membuat model awal, dan properti.

Model TLA+ yang dihasilkan jauh lebih sederhana daripada implementasinya, karena lebih sederhana daripada kode dan karena sifat TLA+ tingkat tinggi. Model pembuat ckBTC memerlukan sekitar 250 baris kode dibandingkan dengan ribuan baris implementasi Rust. Mungkin mengejutkan, salah satu bagian tersulit dalam upaya adalah menentukan properti yang diperlukan, karena sering kali kita menemukan kesenjangan dalam spesifikasi intuitif.

Setelah model selesai, analisis (pemeriksaan model) selesai secara otomatis. Analisis bisa memakan waktu lama untuk dijalankan – misalnya, untuk ckBTC, diperlukan waktu lebih dari 20 jam untuk menyelesaikannya. Terakhir, manfaat lain dari TLA adalah pemodelan dan analisis dapat dilakukan pada tahap desain sebelum kode diimplementasikan, yang membantu menghilangkan pemfaktoran ulang yang besar karena kesalahan desain di kemudian hari.

Dimana TLA+ tidak ada gunanya

Di sisi negatifnya, TLA+ kurang membantu untuk program sekuensial yang kompleks, dibandingkan dengan program yang berjalan bersamaan, dan juga tidak baik dalam menangani protokol kriptografi yang kompleks, yang mana terdapat alat lain (misalnya Tamarin) yang lebih berguna.

Terakhir, terdapat masalah dalam menjaga model TLA+ dan implementasi sebenarnya tetap sinkron, seiring dengan berkembangnya kode implementasi seiring berjalannya waktu, kode tersebut mungkin tidak lagi sesuai dengan model, sehingga sulit dilakukan tanpa dukungan alat.

Faktanya, tim R&D kami sedang mencoba memecahkan masalah ini – saya harap kami dapat segera membagikan beberapa alat kepada Anda!

Saya harap ikhtisar ini menggugah minat Anda dalam menggunakan TLA+ untuk kontrak pintar penting Anda, dan jika ya, pantau terus - postingan lanjutan dengan tutorial yang lebih mendalam tentang cara menggunakan TLA+ untuk kontrak pintar akan segera hadir, dan Terlampir adalah model TLA+ aktual yang dikembangkan oleh tim Litbang kami.

Konten IC yang Anda minati

Kemajuan Teknologi |. Informasi Proyek |

Kumpulkan dan ikuti IC Binance Channel

Ikuti terus informasi terkini