Pengumuman terbaru tentang Verus, sebuah alat verifikasi statis untuk kode Rust, telah memicu perdebatan sengit di kalangan komunitas pengembang tentang peran verifikasi formal dalam bahasa pemrograman yang sudah menekankan keamanan. Seiring Rust terus mendapatkan popularitas karena jaminan keamanan memorinya, alat seperti Verus bertujuan untuk membawa kebenaran kode ke tingkat berikutnya dengan membuktikan secara matematis bahwa kode memenuhi spesifikasinya.
Ekosistem Alat Verifikasi Rust yang Berkembang
Verus bergabung dengan ekosistem alat verifikasi untuk Rust yang terus berkembang, termasuk Prusti dan Creusot. Meskipun alat-alat ini memiliki tujuan yang sama untuk memverifikasi kebenaran kode, mereka mengambil pendekatan berbeda untuk menyelesaikan masalah. Seperti yang dicatat oleh seorang komentator, Yang utama adalah Verus, Prusti dan Creusot, tetapi mereka mengambil pendekatan yang cukup berbeda. Ini tidak berlebihan. Menurut makalah SOSP 2024 yang dirujuk dalam komentar, kecepatan verifikasi tampaknya menjadi salah satu keunggulan utama Verus dibandingkan alat serupa.
Alat-alat ini memungkinkan pengembang untuk menulis spesifikasi tentang apa yang seharusnya dilakukan oleh kode mereka, dan kemudian memverifikasi secara statis bahwa kode tersebut memenuhi spesifikasi tersebut untuk semua kemungkinan eksekusi. Tidak seperti pengujian tradisional, yang hanya dapat memeriksa input tertentu, alat verifikasi formal seperti Verus dapat membuktikan kebenaran di seluruh ruang input.
Perbandingan Alat Verifikasi Rust
- Verus: Alat verifikasi statis yang memeriksa kode terhadap spesifikasi untuk semua kemungkinan eksekusi. Saat ini mendukung subset dari Rust dan memungkinkan verifikasi kode yang memanipulasi raw pointer.
- Prusti: Alat verifikasi lain untuk Rust dengan pendekatan yang berbeda.
- Creusot: Alat verifikasi ketiga dalam ekosistem Rust.
- Kani: Model checker yang digunakan untuk memverifikasi pustaka standar Rust.
Poin Diskusi Utama:
- Kecepatan verifikasi sebagai pembeda antara alat-alat tersebut
- Kebutuhan akan bahasa spesifikasi yang umum
- Integrasi dengan sistem efek Rust yang akan datang
- Pertimbangan antara dependent types bawaan vs alat verifikasi eksternal
 |
|---|
| Tangkapan layar repositori GitHub untuk Verus, menyoroti pengembangan dan kontribusi berkelanjutannya dalam ekosistem alat verifikasi Rust |
Perdebatan: Verifikasi Formal vs. Pengujian
Pengumuman ini telah memicu perdebatan filosofis tentang apakah verifikasi formal diperlukan dalam bahasa seperti Rust yang sudah memberikan jaminan keamanan yang kuat. Beberapa pengembang mempertanyakan apakah menambahkan alat verifikasi di atas Rust itu berlebihan, dengan argumen bahwa pengujian seharusnya cukup untuk sebagian besar kasus penggunaan.
Pengujian memverifikasi bahwa kode berfungsi pada input tertentu. Verifikasi formal memeriksa bahwa kode berfungsi pada setiap input.
Perspektif ini menyoroti perbedaan mendasar antara pengujian dan verifikasi. Sementara pengujian dapat menunjukkan bahwa kode berfungsi untuk input tertentu, verifikasi formal dapat membuktikan bahwa kode berfungsi untuk semua kemungkinan input, termasuk kasus-kasus ekstrem yang mungkin terlewatkan dalam pengujian.
Peran Tipe Dependen
Benang menarik lainnya dalam diskusi ini berpusat pada tipe dependen dan apakah mereka harus dibangun ke dalam bahasa itu sendiri. Tipe dependen memungkinkan tipe bergantung pada nilai, memungkinkan spesifikasi yang lebih tepat pada level tipe. Namun, seperti yang ditunjukkan oleh seorang komentator, menambahkan tipe dependen ke Rust dapat secara signifikan meningkatkan kompleksitas sistem tipe yang sudah canggih.
Beberapa pengembang menyatakan kekhawatiran bahwa menjadikan verifikasi formal sebagai bagian inti dari Rust mungkin membuat hambatan masuk terlalu tinggi. Seperti yang dijelaskan oleh seorang komentator: Perasaan saya adalah bahwa tipe dependen menambah kompleksitas pada bahasa yang sudah terkenal dengan sistem tipe yang kompleks, jadi saya khawatir tentang melampaui anggaran kompleksitas. Mereka menyarankan bahwa menjaga alat verifikasi terpisah memungkinkan pengembang yang membutuhkannya untuk menggunakannya tanpa membebani orang lain dengan kompleksitas.
Arah Masa Depan: Bahasa Spesifikasi Umum
Tema berulang dalam komentar adalah kebutuhan akan bahasa spesifikasi umum di berbagai alat verifikasi. Dengan munculnya beberapa alat di bidang ini, pengembang menyatakan frustrasi karena harus mempelajari sintaks spesifikasi yang berbeda untuk tugas verifikasi yang serupa.
Jaminan sederhana seperti memastikan fungsi tidak pernah panik bisa mendapatkan manfaat dari sintaks standar di semua alat verifikasi. Beberapa komentator menyarankan bahwa jaminan mendasar seperti itu mungkin akhirnya diintegrasikan ke dalam bahasa inti Rust, mungkin sebagai bagian dari sistem efek yang akan datang (sebelumnya dikenal sebagai generik kata kunci).
Diskusi juga menyinggung upaya berkelanjutan Rust untuk memverifikasi pustaka standarnya menggunakan alat seperti Kani, sebuah model checker. Pekerjaan ini menunjukkan pentingnya verifikasi formal dalam memastikan keandalan kode kritis.
Seiring Verus terus berkembang dan memperluas kemampuannya, ini mewakili langkah penting dalam membawa teknik verifikasi formal kepada audiens yang lebih luas dari pengembang Rust. Meskipun tidak setiap proyek akan memerlukan tingkat jaminan yang disediakan oleh verifikasi formal, ketersediaan alat-alat ini memperkaya ekosistem Rust dan menawarkan pengembang lebih banyak pilihan untuk memastikan kebenaran kode.
Referensi: Verus