Panduan untuk alat keamanan kontrak pintar

Kita akan menggunakan tiga teknik pengujian dan analisis program yang berbeda:

• Analisis statis dengan Slither. Semua jalur program diperkirakan dan dianalisis pada saat yang sama, melalui berbagai presentasi program (misalnya, grafik aliran kontrol)
• Fuzzing dengan Echidna. Kode dieksekusi dengan pembuatan transaksi pseudo-acak. Fuzzer akan mencoba menemukan urutan transaksi yang melanggar properti tertentu.
• Eksekusi simbolis dengan Manticore. Sebuah teknik verifikasi formal, yang menerjemahkan setiap jalur eksekusi menjadi rumus matematika, di mana batasan-batasan dapat diperiksa di atasnya.

Setiap teknik memiliki kelebihan dan kekurangannya masing-masing, dan akan berguna dalam kasus-kasus tertentu:

* jika semua jalur dieksplorasi tanpa kehabisan waktu (timeout)

Slither menganalisis kontrak dalam hitungan detik, namun, analisis statis mungkin menghasilkan alarm palsu dan kurang cocok untuk pemeriksaan kompleks (misalnya, pemeriksaan aritmatika). Jalankan Slither melalui API untuk akses instan ke detektor bawaan atau melalui API untuk pemeriksaan yang ditentukan pengguna.

Echidna perlu berjalan selama beberapa menit dan hanya akan menghasilkan positif yang sebenarnya (true positive). Echidna memeriksa properti keamanan yang diberikan pengguna, yang ditulis dalam Solidity. Alat ini mungkin melewatkan bug karena didasarkan pada eksplorasi acak.

Manticore melakukan analisis "paling berat". Seperti Echidna, Manticore memverifikasi properti yang diberikan pengguna. Alat ini akan membutuhkan lebih banyak waktu untuk berjalan, tetapi dapat membuktikan validitas suatu properti dan tidak akan melaporkan alarm palsu.

Alur kerja yang disarankan

Mulailah dengan detektor bawaan Slither untuk memastikan bahwa tidak ada bug sederhana yang ada saat ini atau yang akan muncul di kemudian hari. Gunakan Slither untuk memeriksa properti yang terkait dengan pewarisan, dependensi variabel, dan masalah struktural. Seiring berkembangnya basis kode, gunakan Echidna untuk menguji properti yang lebih kompleks dari state machine. Kunjungi kembali Slither untuk mengembangkan pemeriksaan kustom untuk perlindungan yang tidak tersedia dari Solidity, seperti melindungi agar suatu fungsi tidak ditimpa (overridden). Terakhir, gunakan Manticore untuk melakukan verifikasi yang ditargetkan pada properti keamanan kritis, misalnya, operasi aritmatika.

• Gunakan CLI Slither untuk menangkap masalah umum
• Gunakan Echidna untuk menguji properti keamanan tingkat tinggi dari kontrak Anda
• Gunakan Slither untuk menulis pemeriksaan statis kustom
• Gunakan Manticore setelah Anda menginginkan jaminan mendalam tentang properti keamanan kritis

Catatan tentang pengujian unit (unit test). Pengujian unit diperlukan untuk membangun perangkat lunak berkualitas tinggi. Namun, teknik-teknik ini bukanlah yang paling cocok untuk menemukan celah keamanan. Teknik ini biasanya digunakan untuk menguji perilaku positif dari kode (yaitu, kode berfungsi seperti yang diharapkan dalam konteks normal), sementara celah keamanan cenderung berada pada kasus ekstrem (edge case) yang tidak dipertimbangkan oleh pengembang. Dalam studi kami terhadap puluhan tinjauan keamanan kontrak pintar, cakupan pengujian unit tidak berpengaruh pada jumlah atau tingkat keparahan celah keamanan (opens in a new tab) yang kami temukan dalam kode klien kami.

Menentukan Properti Keamanan

Untuk menguji dan memverifikasi kode Anda secara efektif, Anda harus mengidentifikasi area yang memerlukan perhatian. Karena sumber daya yang Anda habiskan untuk keamanan terbatas, menentukan ruang lingkup bagian yang lemah atau bernilai tinggi dari basis kode Anda penting untuk mengoptimalkan upaya Anda. Pemodelan ancaman (threat modeling) dapat membantu. Pertimbangkan untuk meninjau:

• Penilaian Risiko Cepat (Rapid Risk Assessments) (opens in a new tab) (pendekatan pilihan kami saat waktu terbatas)
• Panduan Pemodelan Ancaman Sistem Berpusat pada Data (opens in a new tab) (alias NIST 800-154)
• Pemodelan ancaman Shostack (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• Penggunaan Asersi (Assertions) (opens in a new tab)

Komponen

Mengetahui apa yang ingin Anda periksa juga akan membantu Anda memilih alat yang tepat.

Area luas yang sering kali relevan untuk kontrak pintar meliputi:

• State machine. Sebagian besar kontrak dapat direpresentasikan sebagai state machine. Pertimbangkan untuk memeriksa bahwa (1) Tidak ada state tidak valid yang dapat dicapai, (2) jika suatu state valid maka state tersebut dapat dicapai, dan (3) tidak ada state yang menjebak kontrak.

  • Echidna dan Manticore adalah alat yang disukai untuk menguji spesifikasi state-machine.

• Kontrol akses. Jika sistem Anda memiliki pengguna dengan hak istimewa (misalnya, pemilik, pengontrol, ...) Anda harus memastikan bahwa (1) setiap pengguna hanya dapat melakukan tindakan yang diizinkan dan (2) tidak ada pengguna yang dapat memblokir tindakan dari pengguna dengan hak istimewa yang lebih tinggi.

  • Slither, Echidna, dan Manticore dapat memeriksa kontrol akses yang benar. Misalnya, Slither dapat memeriksa bahwa hanya fungsi yang masuk daftar putih (whitelisted) yang tidak memiliki pengubah (modifier) onlyOwner. Echidna dan Manticore berguna untuk kontrol akses yang lebih kompleks, seperti izin yang diberikan hanya jika kontrak mencapai state tertentu.

• Operasi aritmatika. Memeriksa keandalan operasi aritmatika sangatlah penting. Menggunakan SafeMath di mana-mana adalah langkah yang baik untuk mencegah limpahan (overflow)/underflow, namun, Anda tetap harus mempertimbangkan kelemahan aritmatika lainnya, termasuk masalah pembulatan dan kelemahan yang menjebak kontrak.

  • Manticore adalah pilihan terbaik di sini. Echidna dapat digunakan jika aritmatika berada di luar cakupan pemecah (solver) SMT.

• Kebenaran pewarisan. Kontrak Solidity sangat bergantung pada pewarisan ganda (multiple inheritance). Kesalahan seperti fungsi bayangan (shadowing function) yang kehilangan panggilan super dan urutan linierisasi c3 yang disalahartikan dapat dengan mudah terjadi.

  • Slither adalah alat untuk memastikan deteksi masalah-masalah ini.

• Interaksi eksternal. Kontrak berinteraksi satu sama lain, dan beberapa kontrak eksternal tidak boleh dipercaya. Misalnya, jika kontrak Anda bergantung pada oracle eksternal, apakah kontrak tersebut akan tetap aman jika separuh dari oracle yang tersedia disusupi?

  • Manticore dan Echidna adalah pilihan terbaik untuk menguji interaksi eksternal dengan kontrak Anda. Manticore memiliki mekanisme bawaan untuk membuat stub kontrak eksternal.

• Kesesuaian standar. Standar Ethereum (misalnya, ERC-20) memiliki sejarah kelemahan dalam desainnya. Waspadai keterbatasan standar yang Anda gunakan sebagai dasar.

  • Slither, Echidna, dan Manticore akan membantu Anda mendeteksi penyimpangan dari standar tertentu.

Lembar contekan pemilihan alat

Area lain perlu diperiksa tergantung pada tujuan Anda, tetapi area fokus yang bersifat umum ini adalah awal yang baik untuk sistem kontrak pintar apa pun.

Audit publik kami berisi contoh properti yang telah diverifikasi atau diuji. Pertimbangkan untuk membaca bagian Automated Testing and Verification dari laporan berikut untuk meninjau properti keamanan di dunia nyata:

• 0x (opens in a new tab)
• Balancer (opens in a new tab)