Teknologi verifikasi Rust untuk diterapkan pada kode sistem tingkat rendah

Alat Verus untuk memverifikasi ketepatan kode Rust

• Verus adalah alat untuk memverifikasi ketepatan kode yang ditulis dalam Rust
• Pengembang menulis spesifikasi yang harus dipenuhi kode, dan Verus memeriksa secara statis apakah kode Rust yang dapat dieksekusi selalu memenuhi spesifikasi untuk semua kemungkinan eksekusi kode
• Alih-alih menambahkan pemeriksaan saat runtime, Verus bergantung pada solver yang kuat untuk membuktikan bahwa kode tersebut benar
• Verus saat ini mendukung subset Rust (sedang diperluas), dan dalam beberapa kasus memungkinkan pengembang memverifikasi kode secara statis melampaui sistem tipe Rust standar (misalnya, manipulasi pointer mentah)

Status saat ini Verus

• Verus sedang dalam pengembangan aktif
• Fitur bisa rusak atau hilang, dan dokumentasinya juga masih belum lengkap
• Jika ingin mencoba Verus, Anda perlu siap meminta bantuan di Zulip

Mencoba Verus

• Untuk mencoba Verus di browser, kunjungi Verus Playground
• Untuk pengembangan yang lebih kompleks, ikuti petunjuk pemasangan lalu lihat dokumen-dokumen di bawah ini, mulai dari tutorial dan referensi

Dokumentasi Verus

• Tutorial dan referensi
• Dokumentasi API untuk pustaka standar Verus
• Panduan verifikasi kode konkurensi
• Tujuan proyek
• Berkontribusi ke Verus
• Lisensi

Menghubungi, melaporkan isu, dan memulai diskusi

• Untuk melaporkan isu, memulai diskusi di GitHub, atau bergabung dengan Zulip jika membutuhkan diskusi real-time dan bantuan
• Gunakan isu GitHub untuk masalah fungsional yang dapat direproduksi (bug), dan gunakan GitHub Discussions untuk percakapan yang lebih terbuka tentang permintaan fitur dan fitur yang direncanakan
• Kontribusi sangat diterima; jika ingin berkontribusi dengan kode, lihat tips pada Contributing to Verus

Opini GN⁺

• Rust dikenal luas sebagai bahasa yang cocok untuk pemrograman sistem karena menjamin keamanan dan performa, dan Verus terlihat seperti proyek yang dapat semakin memperkuat keunggulan Rust ini. Terutama, fitur verifikasi pemrograman konkurensi terlihat sangat menarik

• Namun proyek ini masih pada tahap awal dan tampaknya dukungan sintaks Rust yang didukung masih terbatas, jadi perlu pengembangan lebih lanjut agar dapat digunakan di produksi. Namun, karena jaminan keamanan kode melalui analisis statis adalah hal yang penting, proyek ini tampak berpotensi berkembang dengan baik

• Meskipun masih tahap awal dan terdapat kebutuhan perbaikan seperti dokumentasi yang belum lengkap dan dukungan sintaks yang terbatas, proyek ini berpotensi menjadi peran penting di ekosistem Rust dalam jangka panjang. Dalam bahasa Rusia khususnya pemrograman sistem atau blockchain yang menuntut keandalan tinggi, penggunaannya diperkirakan akan tinggi

[GN⁺]

Komentar Hacker News

• Membuat controller Kubernetes yang diverifikasi secara formal menggunakan Verus
  • Bisa membuktikan sifat liveness bahwa controller pada akhirnya akan menyesuaikan cluster ke state yang diinginkan sesuai permintaan
  • Ada banyak nuansa halus saat mendefinisikan ketepatan (perubahan cepat pada kebutuhan desired state, sifat asinkron, kegagalan, dan sebagainya)
  • Kodenya ada di tautan GitHub dan terhubung dengan paper yang akan terbit di OSDI 2024
• Langkah kecil menuju Verus: Anda bisa menambahkan precondition dan postcondition menggunakan debug_assert Rust
  • Kompilator Rust secara default menghapus hal ini pada build produksi
  • Contoh pada tutorial Verus dan contoh pengecekan runtime menggunakan debug_assert disediakan
• Pertanyaan pemula tentang perbedaan antara "verifikasi kebenaran kode" dan "pembuktian kebenaran kode"
  • Ingin tahu apakah ada materi pembelajaran yang baik tentang "pembuktian" kode untuk praktisi yang latar belakang CS/matematikanya kurang kuat
  • Sangat penasaran mengapa proof "zero knowledge" begitu penting dan kenapa hal ini terasa sangat relevan
• Rust belum punya standar seperti yang sudah ada di C/C++, Common Lisp, dan Ada/SPARK2014
  • Jadi ini masih dianggap target yang berubah-ubah jika dibandingkan dengan alat verifikasi yang dikembangkan untuk Ada/SPARK2014
• Dafny adalah "bahasa pemrograman sadar verifikasi" yang dapat dikompilasi ke Rust (tautan GitHub)
• Seorang kontributor utama menyampaikan presentasi yang sangat bagus tentang Verus di Rust Meetup Zürich (tautan YouTube)
  • Kesan saya, sintaks "ghost" benar-benar rapi di dalam program (sedikit mengingatkan pada Ada)
• Perbandingan Verus dan SPARK
  • Apakah ini adalah verifier kelas umum yang sama? Selain fakta bahwa Verus adalah verifier untuk Rust, bukan untuk Ada, apa bedanya?
• Adakah yang ahli Verus bisa membandingkan performa dan ekspresivitas Verus dengan Lean4?
  • Pemahaman saya adalah Verus adalah verifier berbasis SMT, sedangkan Lean adalah proof assistant interaktif sekaligus alat berbasis SMT
  • Namun pemahaman saya tentang verifikasi formal terbatas, jadi akan lebih baik mendengar pandangan orang yang benar-benar menguasai metode formal perangkat lunak
• Apakah ada hubungan antara Verus dan Kani? Apakah fungsinya beda? (tautan GitHub Kani)
• Apakah ada cara mengimplementasikan agar kode hasilnya tetap menjadi kode Rust yang valid dan tetap dapat dikompilasi dengan toolchain Rust vanilla?