Verifikasi formal dengan menerjemahkan crate core dan alloc Rust ke Coq

 (formal.land)
1 poin oleh GN⁺ 2024-05-16 | 1 komentar | Bagikan ke WhatsApp
  • coq-of-rust, yang memindahkan program Rust ke Coq, mulai menangani hingga crate core dan alloc dari standard library, sehingga mengurangi beban menulis definisi Coq secara manual untuk tiap fungsi primitive
  • Karena kedua crate ini adalah codebase besar yang berisi banyak kode unsafe dan Rust tingkat lanjut, tantangan utamanya adalah menangani hasil terjemahan otomatis sebagai unit yang bisa dikompilasi dan diverifikasi
  • Setelah output dibagi per file Rust input, alloc menjadi 54 file dengan 171.783 baris, dan core menjadi 190 file dengan 592.065 baris, sehingga kompilasi paralel dan debugging menjadi lebih mudah
  • Konflik nama modul pada blok impl telah dikurangi dengan menyertakan informasi klausa where, tetapi file yang saat ini belum dapat dikompilasi di Coq masih tersisa 4% dari keseluruhan
  • Contoh Option::unwrap_or_default menggunakan pendekatan membuktikan ekuivalensi antara definisi terjemahan otomatis dan definisi fungsional yang sederhana, sehingga diperlukan kepercayaan pada otomatisasi sekaligus pemeriksaan pada saat pembuktian

Penanganan primitive standard library Rust

  • Formal Land sedang mengembangkan coq-of-rust, yang menerjemahkan program Rust ke sistem pembuktian formal Coq
  • Sebelumnya, untuk menangani komponen primitive dari standard library Rust, perlu dibuat definisi Coq terpisah yang merepresentasikan perilaku tiap fungsi
  • Untuk mengurangi beban ini, crate core dan alloc Rust diterjemahkan dengan coq-of-rust
  • Hasil terjemahannya dapat dilihat di jalur berikut

Hasil eksekusi terjemahan awal

  • Saat coq-of-rust pertama kali dijalankan pada alloc dan core, dihasilkan 2 file Coq berukuran ratusan ribu baris yang masing-masing mencakup keseluruhan crate
  • Terbukti bahwa tool tersebut bisa berjalan pada codebase besar, tetapi kode Coq yang dihasilkan belum langsung dapat dikompilasi
  • Error muncul jarang, tetapi kira-kira pada tingkat satu error setiap beberapa ribu baris
  • Menurut cloc, ukuran kode Rust input adalah sebagai berikut
    • alloc: 26.299 baris kode Rust
    • core: 54.192 baris kode Rust
  • Karena ekspansi macro terjadi selama proses terjemahan, target terjemahan sebenarnya lebih besar daripada jumlah baris asli

Pemecahan kode Coq yang dihasilkan

  • Perubahan terbesar adalah memecah output coq-of-rust menjadi satu file Coq untuk tiap file Rust input
  • Pemecahan ini dimungkinkan karena terjemahannya tidak sensitif terhadap urutan definisi dan bersifat context-free
  • Biasanya ada dependensi siklik antarfile Rust dan Coq tidak mengizinkannya, tetapi dalam metode terjemahan ini pemisahan per file dimungkinkan
  • Setelah pemecahan, ukuran output adalah sebagai berikut
    • alloc: 54 file Coq, 171.783 baris kode Coq
    • core: 190 file Coq, 592.065 baris kode Coq
  • Dengan memecah file, eksplorasi dan pemeliharaan kode yang dihasilkan menjadi lebih mudah
    • Lebih mudah memparalelkan kompilasi
    • Bisa fokus melakukan debugging satu file demi satu file
    • Lebih mudah mengecualikan file yang tidak dapat dikompilasi
    • Lebih mudah melacak diff pada satu file

Perbaikan konflik nama modul dan file yang tersisa

  • Beberapa bug muncul dari konflik nama modul pada blok impl
  • Cara penyelesaiannya adalah memasukkan lebih banyak informasi ke nama modul untuk meningkatkan keunikannya
    • Informasi klausa where yang sebelumnya hilang kini disertakan
    • Misalnya, pada implementasi trait Default untuk Mapping<K, V>, kondisi bahwa K dan V sama-sama harus mengimplementasikan Default direfleksikan dalam nama modul
  • File yang saat ini tidak dapat dikompilasi di Coq adalah sebagai berikut
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • Ini setara dengan 4% dari seluruh file
  • Di dalam file yang dapat dikompilasi pun masih ada komponen Rust yang belum tertangani dan diaxiomatiskan, sehingga sulit menilai seluruh cakupan yang belum didukung hanya dari rasio ini

Contoh terjemahan Option::unwrap_or_default

  • Option::unwrap_or_default di Rust mengembalikan x jika Some(x), dan memanggil T::default() jika None
  • coq-of-rust menerjemahkannya menjadi definisi Coq berbentuk monadic
    • Mencocokkan argumen input dan tipe
    • Pada cabang Some, mengambil tuple field lalu menyalinnya
    • Pada cabang None, memanggil metode default dari trait core::default::Default
  • Dalam verifikasi nyata, definisi fungsional yang lebih sederhana digunakan alih-alih definisi yang dihasilkan otomatis
    • Jika None, mengembalikan core.simulations.default.Default.default
    • Jika Some x, mengembalikan x
  • Bukti bahwa definisi yang dihasilkan otomatis ekuivalen dengan definisi sederhana ada di CoqOfRust/core/proofs/option.v
  • Jika kode Rust asli berubah, perubahan tersebut akan terdeteksi melalui bukti ini
  • Karena penerjemahan library core dilakukan secara otomatis, definisi yang dihasilkan dapat lebih dipercaya daripada definisi yang ditulis manual
  • Namun, coq-of-rust juga bisa memiliki kesalahan atau ketidaklengkapan, sehingga validitas kode perlu diperiksa pada saat pembuktian

Tugas yang tersisa

  • Kepercayaan terhadap formalisasi standard library dalam verifikasi program Rust meningkat
  • Target berikutnya tetap menyederhanakan proses pembuktian yang membosankan
  • Secara khusus, untuk menunjukkan bahwa simulasi ekuivalen dengan kode Rust asli, diperlukan pekerjaan berikut
    • Resolusi nama
    • Pengenalan tipe tingkat tinggi
    • Penghilangan efek samping
  • Menangani tahap-tahap ini secara terpisah menjadi arah perbaikan ke depan

Bacaan terkait

1 komentar

 
GN⁺ 2024-05-16
Komentar Hacker News

  • Benar-benar mengesankan
    Terjemahan otomatis seperti ini memindahkan objek kepercayaan ke alatnya. coq-of-rust sendiri ditulis dalam Rust, bukan Coq, jadi struktur rekursifnya cukup mengejutkan. Namun jika pendekatan ala CompCert digabungkan dengan cara menghindari serangan Trusting Trust dari Ken Thompson menggunakan compiler kedua, seperti dalam “Countering Trusting Trust through Diverse Double-Compiling” (2009) karya David A. Wheeler [0], tampaknya pembuktian kebenaran bisa dilakukan
    Untuk memverifikasinya, terjemahkan translator coq-of-rust dari Rust ke Coq menggunakan coq-of-rust. Karena penerjemahan itu dilakukan oleh Rust, meskipun kita tidak memercayainya, cukup buktikan di dalam Coq sifat kebenaran yang diinginkan, khususnya bahwa semantik dipertahankan saat menerjemahkan program Rust ke Coq
    Seperti dalam makalahnya, kemungkinan akan lebih mudah membuktikan dengan definisi yang lebih fungsional daripada definisi yang dihasilkan, jadi tinggal melalui proses membuktikan ekuivalensi antar-definisi seperti yang dilakukan pada pustaka standar. Jika translator coq-of-rust saat ini, khususnya lib/ [1], berisi 6.350 baris Rust, menulis seluruh translator dalam Coq dan membuktikan bahwa ia ekuivalen dengan hasil yang dihasilkan juga terlihat realistis
    Setelah itu, jika translator coq-of-rust versi Coq yang sudah terbukti dijalankan pada source coq-of-rust yang ditulis dalam Rust, definisi Coq yang keluar harus cocok dengan output translator coq-of-rust versi Rust yang digunakan pada awalnya
    Sebagai catatan tambahan, menyenangkan melihat pekerjaan semacam ini mendapat pendanaan industri. Saya cenderung sinis terhadap kripto, tetapi memang benar bahwa kebutuhan mereka akan kebenaran mendorong peningkatan di bidang-bidang yang saya minati, seperti Rust, Coq, dan dukungan untuk mahasiswa magister yang saya kenal
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • Saya salah satu penulisnya, dan prosedur seperti itu memang bisa menjadi cara yang baik untuk memverifikasi coq-of-rust
      Namun meskipun kodenya sendiri pendek, ia bergantung pada compiler Rust untuk mem-parse dan melakukan type checking pada kode Rust input. Jadi bagian itu juga perlu diverifikasi, atau setidaknya diberi spesifikasi formal meski tanpa pembuktian. API rustc yang cukup besar dan tidak stabil menjadi hambatan, tetapi tetap bisa menjadi salah satu cara untuk meningkatkan tingkat kepercayaan
    • Ini mengingatkan saya pada masa ketika dulu bekerja dengan SPARK Ada. Pada proyek yang tidak memiliki target Ada yang didukung, khususnya pada perangkat yang sangat kecil, kami biasanya mengonversi Ada ke C lalu mengompilasinya untuk target tersebut, sehingga berbagai bentuk analisis statis bisa dilakukan di sisi SPARK
      Tentu muncul masalah bahwa output atau converter-nya harus diverifikasi, tetapi kode C yang dihasilkan cukup mudah dibaca untuk tujuan verifikasi, gayanya juga terbatas, dan kepercayaan terhadap alatnya cukup tinggi. Analisis statis SPARK hanyalah salah satu bagian dari keseluruhan proses verifikasi dan validasi, sementara pengujian dan aktivitas lain menyediakan lapisan kepercayaan tambahan. Secara keseluruhan, pendekatan itu bekerja cukup baik
    • Alasan kripto membantu pekerjaan seperti ini bukan hanya karena ada batasan kebenaran, tetapi juga karena banyak kekayaan berpindah ke orang-orang yang tertarik pada ilmu komputer
      Mereka membelanjakan uang itu untuk riset ilmu komputer bukan hanya karena menguntungkan bagi mereka, tetapi juga karena itu merupakan kegiatan filantropi yang bersinggungan dengan hobi mereka
    • Saya tidak begitu paham bagaimana pendekatan itu mencegah compiler Rust yang dipakai untuk membuat biner menyuntikkan payload berbahaya. Kita memang bisa membangun A menjadi B, lalu membangun B menjadi A, kemudian membandingkan binernya
      Pendekatan lain adalah proof-carrying code. Compiler Rust mengeluarkan pembuktian Coq bahwa output executable sesuai dengan semantik source code input
      Tentu saja, bisa juga menulis compiler untuk subset Rust, misalnya tanpa borrow checker atau optimisasi, ke machine code arsitektur tertentu, lalu melakukan bootstrap semuanya dari sana

  • Ukuran program yang diverifikasi dari awal sampai akhir dengan sistem pembuktian deduktif semi-otomatis seperti Coq itu kecil. Pustaka mungkin lebih mudah karena tingkat interaksi antarkode lebih rendah, tetapi program umum tidak demikian
    Dalam praktiknya, pertumbuhan ukuran program yang bisa diverifikasi dengan cara ini lebih lambat daripada pertumbuhan ukuran rata-rata seluruh program. Verifikasi perangkat lunak yang sound, yaitu menunjukkan bahwa ia 100% sesuai dengan spesifikasi, jelas berguna untuk hal-hal seperti pembuktian kebenaran algoritma inti, tetapi sulit diskalakan
    Karena itu, sebagian riset bergeser ke metode yang tidak sound. Biaya jaminan 100% bisa 10 kali lipat dari jaminan 99,9999%, dan selisih probabilitas itu bisa lebih kecil daripada probabilitas kegagalan di luar perangkat lunak. Sistem fisik sejak awal tidak bisa dibuktikan sesuai dengan spesifikasi, dan spesifikasi itu sendiri juga bisa saja tidak cukup cocok dengan kenyataan

    • Intinya adalah, jika kita membuktikan bagian unsafe dari pustaka standar dan jaminan keamanan Rust, maka memory safety, ketiadaan data race, dan sebagainya untuk semua kode Rust aman yang hanya menggunakan pustaka standar dapat dibuktikan secara transitif
      Membuktikan bahwa hanya kode unsafe yang benar membutuhkan usaha jauh lebih kecil daripada membuktikan semua kode Rust. Ini menjadi jawaban atas kritik yang sering muncul saat membicarakan jaminan keamanan Rust: “bagaimana dengan kode unsafe?” Celah yang tidak cukup kuat untuk ditangani hanya oleh type system Rust dapat diisi dengan sistem yang lebih kuat seperti Coq

  • Ada bagian yang sulit saya pahami dari upaya seperti ini. Jika kode harus dikonversi ke Coq secara manual atau semimanual, bukankah kemungkinan membuat kesalahan dalam proses itu jauh lebih besar daripada manfaat yang didapat dari verifikasi formal?
    Dengan kata lain, bagaimana kita tahu bahwa apa yang kita buktikan masih berlaku untuk kode asli?

    • Kita tidak bisa tahu. Pada akhirnya kita harus memercayai sesuatu, entah itu hardware, compiler, spesifikasi, kernel tepercaya Coq, dan sebagainya
      Verifikasi formal sering dibahas seolah-olah sepenuhnya menghilangkan kemungkinan bug, tetapi dalam praktiknya lebih tepat dikatakan sangat menurunkan kemungkinan bug. Meski begitu, penerjemahan otomatis antara Rust dan Coq sangat mengurangi kompleksitas hal-hal yang harus dipercaya, sehingga seharusnya lebih dipilih daripada penerjemahan manual
    • Itu memang batasan yang benar, tetapi bukan batasan yang separah itu
      Dalam banyak kasus, bug dalam penerjemahan hanya membuat pembuktian menjadi tidak mungkin. Lalu seseorang akan menyelidiki mengapa pembuktian tidak lolos dan menemukan bug penerjemahan tersebut
      Masalah sebenarnya adalah jika bug penerjemahan secara tepat meniadakan bug dalam kode asli. Jika tidak ada risiko sistematis, kemungkinan dua bug saling menghapus seperti ini cukup rendah
    • Kode diterjemahkan otomatis dengan coq-of-rust. Jika masalah ditemukan dalam penerjemahan, cukup perbaiki sekali di alat coq-of-rust, dan semua hasil terjemahan akan diperbarui

  • Untuk pembaca yang berminat: saya mengirimkan posting blog ini karena konten terkait kriptonya tidak terlalu langsung dibandingkan tulisan lain di blog yang sama, tetapi di sana ada banyak tulisan yang secara teknis lebih menarik
    Khususnya, dua tulisan terbaru membahas penerapan pendekatan yang sama bukan ke Rust, melainkan ke Python

  • Saya teringat sebuah kuliah [1] tentang fuzzer yang dulu menemukan bug pada compiler C yang sudah diverifikasi secara formal. Penyebabnya adalah verifikasi formalnya tidak mencakup frontend dan backend
    Saya juga paham munculnya pertanyaan seberapa jauh Coq itu sendiri atau penerjemahannya bisa dipercaya, dan saya juga bertanya-tanya bagaimana ini akan disinkronkan dengan pembaruan Rust, tetapi bahkan verifikasi formal yang sempurna pun tidak berarti akurasi 100% dari awal sampai akhir
    [1] https://youtu.be/Ux0YnVEaI6A

  • Saya sama sekali bukan ahli verifikasi formal, tetapi jika library dasar Rust diverifikasi secara formal dan tidak memakai kode unsafe, apakah semua program Rust yang memakai library yang sudah diverifikasi secara formal itu pada dasarnya akan memiliki kualitas setingkat verifikasi formal dalam hal penanganan memori?

    • Keamanan Rust hampir tidak berkaitan dengan bug
      Rust punya definisi “safe” sendiri, dan ini bisa dianggap sebagai subset dari memory safety. Bahkan dalam kode Rust yang sepenuhnya safe, data race, deadlock, kehabisan memori, dan tentu saja kesalahan logika tetap mungkin terjadi
    • Sampai batas tertentu saya rasa memang itulah impiannya, tetapi ada banyak catatan dan beberapa hal harus cocok terlebih dahulu
      Pertama, semantik unsafe Rust harus diformalkan. Karya perintis RustBelt[1] dari Ralf Jung merupakan kemajuan besar, tetapi belum lengkap. Khususnya, asal-usul pointer ternyata menjadi unsur yang rumit
      Kedua, sebagai bagian dari itu diperlukan model formal untuk borrow checker. Stacked borrows[2] adalah upaya yang baik tetapi memiliki cacat, dan Tree borrows[3] mungkin bisa memperbaikinya, meski bisa juga muncul sesuatu yang lebih canggih
      Ketiga, diperlukan model memori formal. Ini terutama berkaitan dengan perilaku operasi atomik dan sinkronisasi, sehingga sangat penting bagi komponen standard library seperti Arc. Secara luas diterima bahwa model memori Rust harus mirip dengan C++ dan dapat berinteroperasi dengannya, tetapi masalah “out of thin air” dan fitur yang belum ada seperti seqlock masih tersisa. Itu salah satu alasan kernel Linux masih memakai modelnya sendiri
      Keempat, perlu ada bukti bahwa jaminan keamanan dapat dikomposisikan dengan baik. Secara khusus, jaminan keamanan harus tetap terjaga ketika kode yang sound dan ditulis dengan unsafe Rust dikomposisikan dengan kode safe Rust. Sejauh ini hasilnya bagus, tetapi harus dibuktikan untuk keseluruhan sistem
      Kelima, agar pembuktian seperti itu berlaku untuk semua kode, semua bug soundness[1] yang tersisa di Rust harus ditutup. Banyak dari masalah ini bersifat teoretis atau baru benar-benar penting pada kode adversarial[5], sehingga progresnya lambat
      Bahkan setelah semua itu selesai, jaminannya tetap hanya parsial. Sebagian sangat besar dari permukaan yang berinteraksi dengan sistem didasarkan pada kode unsafe. Jika yang dilakukan hanya komputasi murni mungkin tidak masalah, tetapi misalnya jika membuat UI grafis, masih ada sangat banyak hal yang bisa salah
      Meski begitu, ada jalur maju yang praktis, dan itu mengarah ke situasi yang jauh lebih baik daripada keadaan umum sistem masa kini yang penuh kerentanan
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • Saya bukan ahli Rust, tetapi tampaknya ada cukup banyak unsafe di kode core. Wajar saja
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      Saya tidak berpikir Coq dengan cara yang disajikan di sini bisa memverifikasi semua pemanggilan unsafe

  • Bisakah dibandingkan bagaimana pendekatan ini berbeda dari Aeneas atau RustHornBelt? Bagaimana pointer dan mutable borrow ditangani?

    • Saya tidak tahu bagaimana RustHornBelt bekerja. Kami berfokus pada kode yang aman, tetapi untuk blok unsafe pun kami tetap menghasilkan terjemahan dengan pendekatan “upaya terbaik”
      Dibandingkan dengan Aeneas, tujuannya sangat mirip. Sebab keduanya sama-sama berupaya memverifikasi program Rust dengan interactive theorem prover. Namun di coq-of-rust, kami menulis secara manual versi kode yang murni fungsional sebagai target pembuktian, atau karena pekerjaannya repetitif, menulisnya dengan bantuan GitHub Copilot, lalu membuktikan bahwa versi itu ekuivalen dengan hasil terjemahan otomatis. Aeneas bertujuan menghasilkan versi fungsional tersebut secara langsung
      Semua pointer diperlakukan seolah-olah merupakan pointer mutable, yaitu tipe *. Informasi dari borrow checker Rust tidak digunakan; ini membuat terjemahannya lebih sederhana, tetapi biayanya dibayar pada saat pembuktian
      Untuk menalar tentang pointer dalam pembuktian, kami memungkinkan pengguna menyediakan allocator khusus yang dapat dirancang sesuai bagaimana memori akan digunakan. Misalnya, jika program menggunakan tiga variabel mutable global, memori bisa dibuat sebagai record dengan tiga entri. Entri-entri ini awalnya bernilai None untuk menunjukkan keadaan belum dialokasikan
      Kami belum tahu sejauh mana teknik ini dapat diskalakan, tetapi setidaknya untuk saat ini kami bisa menghindari penalaran dengan separation logic. Kami berharap sebagian besar program yang ingin diverifikasi, terutama di sisi aplikasi, memiliki disiplin memori yang relatif “sederhana”

  • Apakah menulis spesifikasi verifikasi formal mirip dengan menggunakan property-based testing yang lebih kompleks? Bahkan menulis property-based test juga cukup sulit dan memakan waktu begitu melewati program yang tidak rumit

    • Mirip, tetapi tidak selalu sama. Property-based testing biasanya menentukan deskripsi input pada level antarmuka sistem, fungsi atau prosedur, atau level yang lebih tinggi, lalu menguji apakah output memenuhi suatu properti atau sekumpulan properti
      Saat melakukan verifikasi formal pada level yang sama, tampilannya bisa cukup mirip. Namun alat verifikasi formal dapat masuk lebih dalam. Misalnya, alat itu bisa menjawab pertanyaan seperti “ada invariant untuk loop ini; bisakah dibuktikan bahwa invariant tersebut benar-benar dipertahankan pada setiap iterasi?” atau “bisakah dibuktikan bahwa selama komputasi ini tidak pernah terjadi underflow/overflow pada perhitungan antara mana pun?”
      Yang pertama juga bisa dilakukan dengan property-based testing jika inti loop dipisahkan menjadi prosedur tersendiri lalu dijalankan pada banyak state antara untuk menguji properti invariant. Yang kedua jauh lebih sulit kecuali program dipecah secara ekstrem sampai bisa dijalankan terpisah per baris

  • Saya bahkan tidak tahu bahwa hal seperti ini mungkin dilakukan
    Saya penasaran apakah upaya semacam ini bisa mempercepat adopsi Rust pada bagian-bagian inti untuk masuk ke kernel

  • Bisakah seseorang menjelaskan konsep “verifikasi” dengan sangat sederhana? Saya penasaran mengapa ada satu bahasa utuh seperti Coq hanya untuk tujuan ini, dan apa makna praktisnya bagi masyarakat luas