Pengumuman terkini tentang Verus, alat pengesahan statik untuk kod Rust, telah mencetuskan perbahasan hangat dalam komuniti pembangun mengenai peranan pengesahan formal dalam bahasa pengaturcaraan yang sudah menekankan keselamatan. Ketika Rust terus mendapat populariti untuk jaminan keselamatan memorinya, alat seperti Verus bertujuan untuk membawa ketepatan kod ke tahap seterusnya dengan membuktikan secara matematik bahawa kod memenuhi spesifikasinya.
Ekosistem Alat Pengesahan Rust yang Berkembang
Verus menyertai ekosistem alat pengesahan untuk Rust yang semakin berkembang, termasuk Prusti dan Creusot. Walaupun alat-alat ini berkongsi matlamat yang sama untuk mengesahkan ketepatan kod, mereka mengambil pendekatan yang berbeza terhadap masalah tersebut. Seperti yang dinyatakan oleh seorang pengulas, Yang utama adalah Verus, Prusti dan Creusot, tetapi mereka mengambil pendekatan yang agak berbeza. Ini bukan berlebihan. Menurut kertas SOSP 2024 yang dirujuk dalam komen, kelajuan pengesahan nampaknya menjadi salah satu kelebihan utama Verus berbanding alat serupa.
Alat-alat ini membolehkan pembangun menulis spesifikasi tentang apa yang sepatutnya dilakukan oleh kod mereka, dan kemudian mengesahkan secara statik bahawa kod tersebut memenuhi spesifikasi untuk semua pelaksanaan yang mungkin. Tidak seperti pengujian tradisional, yang hanya boleh memeriksa input tertentu, alat pengesahan formal seperti Verus boleh membuktikan ketepatan merentasi keseluruhan ruang input.
Perbandingan Alat Pengesahan Rust
- Verus: Alat pengesahan statik yang memeriksa kod berdasarkan spesifikasi untuk semua kemungkinan pelaksanaan. Pada masa ini menyokong subset Rust dan membolehkan pengesahan kod yang memanipulasi penuding mentah.
- Prusti: Alat pengesahan lain untuk Rust dengan pendekatan yang berbeza.
- Creusot: Alat pengesahan ketiga dalam ekosistem Rust.
- Kani: Pemeriksa model yang digunakan untuk mengesahkan pustaka standard Rust.
Perkara Utama Perbincangan:
- Kelajuan pengesahan sebagai pembeza antara alat-alat
- Keperluan untuk bahasa spesifikasi yang sama
- Integrasi dengan sistem kesan Rust yang akan datang
- Pertimbangan antara jenis bersandar terbina dalam berbanding alat pengesahan luaran
 |
|---|
| Tangkapan skrin repositori GitHub untuk Verus, menyerlahkan pembangunan dan sumbangan berterusan dalam ekosistem alat pengesahan Rust |
Perbahasan: Pengesahan Formal berbanding Pengujian
Pengumuman ini telah mencetuskan perbahasan falsafah tentang sama ada pengesahan formal diperlukan dalam bahasa seperti Rust yang sudah menyediakan jaminan keselamatan yang kukuh. Sesetengah pembangun mempersoalkan sama ada menambah alat pengesahan di atas Rust adalah berlebihan, dengan hujah bahawa pengujian seharusnya mencukupi untuk kebanyakan kes penggunaan.
Ujian mengesahkan bahawa kod berfungsi pada input tertentu. Pengesahan formal memeriksa bahawa ia berfungsi pada setiap input.
Perspektif ini menyoroti perbezaan asas antara pengujian dan pengesahan. Walaupun ujian boleh menunjukkan bahawa kod berfungsi untuk input tertentu, pengesahan formal boleh membuktikan bahawa kod berfungsi untuk semua input yang mungkin, termasuk kes-kes pinggir yang mungkin terlepas dalam pengujian.
Peranan Jenis Bergantung (Dependent Types)
Satu lagi topik menarik dalam perbincangan ini berkisar pada jenis bergantung dan sama ada ia harus dibina ke dalam bahasa itu sendiri. Jenis bergantung membolehkan jenis bergantung pada nilai, membolehkan spesifikasi yang lebih tepat pada tahap jenis. Walau bagaimanapun, seperti yang ditunjukkan oleh seorang pengulas, menambah jenis bergantung kepada Rust boleh meningkatkan kerumitan sistem jenis yang sudah canggih.
Sesetengah pembangun menyatakan kebimbangan bahawa menjadikan pengesahan formal sebagai bahagian teras Rust mungkin meningkatkan halangan kemasukan terlalu tinggi. Seperti yang dijelaskan oleh seorang pengulas: Perasaan saya adalah bahawa jenis bergantung menambah kerumitan kepada bahasa yang sudah terkenal dengan sistem jenis yang kompleks, jadi saya bimbang tentang meningkatkan bajet kerumitan. Mereka mencadangkan bahawa mengekalkan alat pengesahan secara berasingan membolehkan pembangun yang memerlukannya untuk menggunakannya tanpa membebankan semua orang dengan kerumitan tersebut.
Arah Masa Depan: Bahasa Spesifikasi Umum
Tema berulang dalam komen adalah keperluan untuk bahasa spesifikasi umum merentasi alat pengesahan yang berbeza. Dengan pelbagai alat muncul dalam ruang ini, pembangun menyatakan kekecewaan kerana perlu mempelajari sintaks spesifikasi yang berbeza untuk tugas pengesahan yang serupa.
Jaminan mudah seperti memastikan fungsi tidak pernah panik boleh mendapat manfaat daripada sintaks standard merentasi semua alat pengesahan. Sesetengah pengulas mencadangkan bahawa jaminan asas sedemikian mungkin akhirnya diintegrasikan ke dalam bahasa teras Rust, mungkin sebagai sebahagian daripada sistem kesan akan datang (dahulunya dikenali sebagai kata kunci generik).
Perbincangan itu juga menyentuh tentang usaha berterusan Rust untuk mengesahkan perpustakaan standardnya menggunakan alat seperti Kani, pemeriksa model. Kerja ini menunjukkan kepentingan pengesahan formal yang semakin meningkat dalam memastikan kebolehpercayaan kod kritikal.
Ketika Verus terus berkembang dan meluaskan keupayaannya, ia mewakili langkah penting dalam membawa teknik pengesahan formal kepada khalayak pembangun Rust yang lebih luas. Walaupun tidak setiap projek akan memerlukan tahap jaminan yang disediakan oleh pengesahan formal, mempunyai alat-alat ini tersedia memperkaya ekosistem Rust dan menawarkan pembangun lebih banyak pilihan untuk memastikan ketepatan kod.
Rujukan: Verus