- Verus adalah alat untuk memverifikasi kebenaran kode yang ditulis dengan Rust; ketika pengembang menuliskan spesifikasi tentang apa yang harus dilakukan kode, alat ini secara statis memeriksa apakah kode Rust yang dapat dijalankan memenuhi spesifikasi tersebut pada semua kemungkinan eksekusi
- Alat ini membuktikan bahwa kode benar dengan menggunakan solver yang kuat tanpa menambahkan pemeriksaan runtime, dan saat ini baru mendukung sebagian dari Rust
- Dalam beberapa kasus, alat ini juga dapat memeriksa secara statis kebenaran kode yang memanipulasi raw pointer, melampaui sistem tipe Rust standar
- Proyek ini masih aktif dikembangkan; beberapa fitur bisa rusak atau belum tersedia, dan dokumentasinya juga belum lengkap, sehingga pengguna perlu siap meminta bantuan di Zulip
- Verus Playground untuk browser, panduan instalasi, tutorial dan referensi, dokumentasi API pustaka standar, panduan verifikasi kode konkurensi, serta contoh dan pengujian disediakan sebagai jalur belajar dan eksperimen
Apa yang diverifikasi Verus
- Verus adalah alat untuk memverifikasi kebenaran kode Rust
- Pengembang menuliskan perilaku yang harus dijalankan kode sebagai spesifikasi
- Verus secara statis memeriksa apakah kode Rust yang dapat dijalankan selalu memenuhi spesifikasi tersebut pada semua kemungkinan eksekusi
- Alih-alih menambahkan pemeriksaan runtime, Verus menggunakan solver untuk membuktikan bahwa kode benar
- Cakupan dukungan saat ini adalah subset dari Rust, dan pekerjaan untuk memperluas cakupan itu sedang berlangsung
- Dalam beberapa kasus, Verus dapat memverifikasi secara statis kebenaran kode yang melampaui sistem tipe Rust standar, misalnya kode yang memanipulasi raw pointer
Status pengembangan dan hal yang perlu diperhatikan saat menggunakan
- Verus adalah proyek yang masih aktif dikembangkan
- Beberapa fitur bisa rusak atau belum tersedia
- Dokumentasi masih belum lengkap
- Jika ingin mencoba Verus, pengguna perlu siap meminta bantuan di Zulip
- Komunitas Verus telah menerbitkan sejumlah makalah penelitian, dan berbagai proyek di industri maupun akademia menggunakan Verus
- Daftar terkait dapat dilihat di halaman publications and projects
Cara memulai dan alat pengembangan
- Untuk mencoba Verus di browser, Anda dapat menggunakan Verus Playground
- Untuk pengembangan yang lebih serius, Anda perlu mengikuti panduan instalasi
- Pembelajaran dapat dimulai dari Tutorial and reference
- Pemformat otomatis verusfmt untuk kode Verus juga didukung
Dokumentasi dan materi pembelajaran
- Sumber daya dokumentasi yang sedang dikerjakan mencakup hal-hal berikut
- Tutorial and reference: tutorial dan referensi Verus
- API documentation for Verus's standard library: dokumentasi API pustaka standar Verus
- Guide for verifying concurrent code: panduan verifikasi kode konkurensi
- Contributing to Verus
- Best Practices untuk menerbitkan crate terkait Verus ke crates.io
- Verus License
- Verus Logos
Contoh dan partisipasi komunitas
- Contoh penggunaan Verus menyediakan berbagai titik awal selain dokumentasi
- Publications and projects: publikasi dan proyek yang menggunakan Verus
- Videos, slides, and exercises: video, slide, dan latihan dari tutorial Verus satu hari
- Standalone examples: contoh mandiri yang menggunakan Verus untuk tugas-tugas kecil dan spesifik
- Small and medium-sized examples: contoh yang menunjukkan berbagai fitur Verus
- Unit tests: pengujian yang berisi contoh sintaks dan fitur Verus
- Pelaporan isu dan diskusi dapat dilakukan di GitHub atau Zulip
- Untuk permintaan fitur dan diskusi terbuka digunakan GitHub discussions, sedangkan bug yang dapat direproduksi pada fitur yang sudah ada ditempatkan di GitHub issues
- Jika ingin berkontribusi pada kode, Anda dapat merujuk ke panduan dalam Contributing to Verus
1 komentar
Pendapat di Hacker News
Pernah mencoba menulis controller Kubernetes yang diverifikasi secara formal dengan Verus
Pada dasarnya, kita bisa membuktikan properti liveness seperti “suatu saat controller akan menyesuaikan cluster ke state target yang diminta”
Namun jika memikirkan kasus ketika state target berubah cepat, asinkroni, kegagalan, dan sebagainya, menspesifikasikan “kebenaran” itu sendiri punya banyak sisi yang subtil
Kode: https://github.com/vmware-research/verifiable-controllers/, paper terkait rencananya akan dimuat di OSDI 2024
Sebagai langkah kecil menuju Verus, kita bisa menambahkan debug_assert Rust pada precondition dan postcondition
Compiler Rust secara default menghapusnya di build produksi
Contoh verifikasi di tutorial Verus menuliskan rentang input dan kondisi hasil dengan
requiresdanensures, sementara versi pemeriksaan runtime mengecek kondisi yang sama saat eksekusi, sepertidebug_assert(-16 <= x1),debug_assert(x8 == 8 * x1)Tool desain pembuktian/verifikasi/kontrak Rust lain seperti Creusot memakai sintaks berbasis atribut, yang umumnya terasa lebih ringan dan lebih Rust-like
Semoga cara seperti ini juga memungkinkan di rilis Verus mendatang
Ini alat dokumentasi yang sangat bagus, dan melengkapi type system serta testing dengan sangat baik
"contracts": https://docs.rs/contracts/latest/contracts/Saya menambahkan precondition dan postcondition ke sebagian besar fungsi, dan di JVM ada flag untuk menghapusnya dengan mudah di build produksi
Dari sudut pandang orang yang tidak punya banyak pengalaman ilmu komputer nyata, saya penasaran: apa bedanya verifikasi pada “memverifikasi kebenaran kode” di README dengan “pembuktian” yang disebut di tempat lain?
Saya juga ingin tahu materi yang bagus untuk programmer praktisi tanpa latar belakang kuat di ilmu komputer/matematika untuk belajar “membuktikan” sesuatu tentang kode
Selain itu, saya juga tidak begitu paham mengapa zero-knowledge proof begitu penting dan relevan. Misalnya saya pernah mendengar hal seperti x.com/ZorpZK, tetapi tidak mengerti kenapa itu keren
Namun pendekatan Coq yang dipakai Verus dan Software Foundations berbeda
Verus mencoba membuktikan properti secara otomatis dengan sistem pemecah constraint otomatis bernama SMT solver, sedangkan Coq mengharuskan jauh lebih banyak bagian dibuktikan secara manual dan otomatisasinya terbatas
Keduanya punya kelebihan dan kekurangan; otomatisasi bagus ketika berhasil, tetapi membuat frustrasi ketika tidak berhasil
Zero-knowledge proof sebaiknya dianggap sebagai bidang yang agak berbeda, dan banyak orang yang bekerja di verifikasi/pembuktian formal juga tidak menyentuh zero-knowledge proof. Lebih baik menganggapnya sebagai primitive kriptografi
Zero-knowledge proof punya overhead besar dan kekurangan apa yang disebut “killer app”, jadi kegunaan praktis, kepentingan, atau relevansinya belum terlalu besar, tetapi secara konseptual menarik
Saya juga berharap ada materi belajar yang bagus. Dokumentasi Dafny cukup baik, tetapi verifikasi perangkat lunak formal tampaknya belum sampai pada tahap yang nyaman dipakai programmer biasa yang bukan PhD ilmu komputer/matematika
Kalau hanya melihat contoh, kelihatannya relatif mudah, tetapi segera kita bertemu “tidak bisa dibuktikan”, dan jawaban mengapa demikian sering masuk ke detail implementasi mendalam yang sepertinya hanya diketahui penulisnya
Misalnya, kita bisa memverifikasi bahwa kita mengetahui kata sandi tanpa mengirim kata sandi ke server, sehingga server jahat atau penyerang man-in-the-middle lebih sulit mengintip kata sandi
Ini juga bisa memberi opsi yang lebih baik untuk verifikasi identitas. Kita bisa membuktikan bahwa kita memiliki identitas yang diterbitkan pemerintah tanpa harus menyerahkan dokumen itu sendiri ke server, sehingga bisa mengurangi kejadian “disimpan maksimal 2 tahun/3 tahun/6 bulan” lalu akhirnya bocor
Pembuktian tentang kode belum menjadi hal yang dilakukan programmer praktisi
Hoare logic adalah titik awal yang bagus, dan kadang diajarkan juga di kelas pengantar ilmu komputer
Coq punya kurva belajar yang curam, dan akan lebih sulit lagi jika tidak terbiasa dengan OCaml atau bahasa serupa. Why3 mungkin lebih ramah bagi pemula: https://www.why3.org
Pembuktian dan verifikasi bisa berarti hal yang sama, tetapi pembuktian terasa lebih interaktif, sedangkan verifikasi terasa seperti sesuatu yang bisa diotomatisasi, misalnya model checking atau pemecahan SMT atas program beranotasi
Bagi yang belum tahu proyek serupa, Dafny adalah “bahasa pemrograman yang sadar verifikasi” yang dapat dikompilasi ke Rust: https://github.com/dafny-lang/dafny
Beberapa hari lalu saya menulis artikel pengantar untuk pemula Dafny: https://www.linkedin.com/pulse/getting-started-dafny-your-fi...
Terlihat sangat keren. Akan berguna bagi orang-orang jika ada panduan atau contoh tentang cara menambahkan bukti ke codebase yang sudah ada
Misalnya, bayangkan aplikasi GUI minimal yang hanya punya satu kotak teks, menerima lewat request HTTP sebuah array yang tidak diketahui saat kompilasi dan tidak tepercaya, lalu melakukan bubble sort dan menampilkannya
Bubble sort itu punya bug yang disengaja, seperti kesalahan off-by-one yang membuat elemen terakhir tetap apa adanya, dan unit test kebetulan tidak menangkap bug tersebut. Kekhawatiran bahwa pengujian tidak lengkap bisa menjadi motivasi utama untuk beralih ke pembuktian
Lalu akan bagus jika ditunjukkan proses mengganti unit test dengan bukti, sambil menemukan dan memperbaiki bug tersebut
Tidak perlu menjelaskan kode pembuktian itu sendiri secara rinci; cukup fokus pada detail praktis seperti batas antara kode matematika yang sudah dibuktikan dan kode input/output yang belum dibuktikan, command line yang dipakai untuk pembuktian dan build, serta arsip zip yang bisa dicoba langsung
Sebenarnya, sekadar membaca dari standard input dan menulis ke standard output pun sepertinya sudah cukup
Salah satu kontributor utama pernah memberikan presentasi yang sangat bagus tentang Verus di Zürich Rust meetup: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
Saya terkesan dengan betapa rapinya kode “ghost” ini masuk ke dalam program, dan itu sedikit mengingatkan saya pada Ada
Saya penasaran apakah Rust sudah punya standar seperti C/C++, Common Lisp, atau Ada/SPARK2014
Kalau belum ada, dibandingkan dengan alat verifikasi yang dikembangkan untuk Ada/SPARK2014, targetnya jadi terus bergerak
Warisan Ada/SPARK2014, dari bare metal sampai aplikasi safety-critical berintegritas tinggi, juga sulit diabaikan
Apakah yang dimaksud ini?
Saya penasaran apa hubungan antara ini dan Kani. Apakah keduanya bekerja secara berbeda?
https://github.com/model-checking/kani
Verifier otomatis berbasis SMT seperti Verus, Dafny, F*, dan VCC milik saya mengharuskan anotasi pada hampir semua fungsi dan loop, tetapi memberikan jaminan yang lebih luas tentang kebenaran program
Alat berbasis interactive prover seperti Coq atau Lean biasanya membutuhkan lebih banyak arahan dari pengguna, tetapi bisa menjamin properti yang lebih kompleks
Saya penasaran bagaimana Verus dibandingkan dengan SPARK
Apakah keduanya termasuk verifier dari kategori umum yang sama? Selain fakta bahwa Verus adalah verifier untuk Rust, bukan untuk Ada, apa perbedaannya?
Akan bagus jika seseorang yang mengenal Verus dengan baik bisa menjelaskan perbedaan performa dan daya ekspresif antara Verus dan Lean4
Pemahaman saya, Verus adalah alat verifikasi berbasis SMT, sedangkan Lean adalah interactive prover sekaligus alat berbasis SMT
Namun pemahaman saya tentang bidang verifikasi formal terbatas, jadi saya ingin mendengar pandangan dari orang yang memahami metode formal perangkat lunak
Misalnya, seperti buku “Software Foundations” untuk Coq, kita bisa merumuskan dan membuktikan proposisi tentang kode C, tetapi tampaknya hampir tidak ada yang melakukannya dengan Lean dan tooling-nya juga kurang
Kita juga bisa menulis program dengan Lean4 lalu membuktikan sesuatu tentang program tersebut, dan ada sebagian orang yang mulai melakukannya sedikit demi sedikit
Memformalkan matematika murni dan menerbitkan makalah tentangnya adalah cara utama Lean4 dan Coq digunakan saat ini
Jenis hal yang benar-benar dapat dinyatakan dan dibuktikan oleh Lean/Coq memang lebih umum, tetapi untuk program dunia nyata, tingkat keumuman seperti itu belum tentu diperlukan