Menerjemahkan crate `core` dan `alloc` Rust ke Coq untuk verifikasi formal

Menerjemahkan crate core dan alloc Rust

Eksekusi awal 🐥

• Hasil eksekusi awal crate alloc dan core Rust menggunakan coq-of-rust menghasilkan dua berkas kode Coq yang masing-masing berukuran ratusan ribu baris.
• Ini menunjukkan bahwa alat tersebut bekerja bahkan pada codebase besar, tetapi kode Coq yang dihasilkan tidak dapat dikompilasi. Error muncul relatif jarang (sekitar sekali tiap beberapa ribu baris).

Ukuran kode Rust input (berdasarkan perintah cloc)

• alloc: 26.299 baris kode Rust

• core: 54.192 baris kode Rust

• Karena penerjemahan harus dilakukan setelah macro diekspansi, ukuran sebenarnya yang harus diterjemahkan lebih besar.

Pemisahan kode hasil generasi 🪓

• Perubahan utamanya adalah keluaran yang dihasilkan coq-of-rust dibagi menjadi satu berkas untuk setiap berkas Rust input.
• Ini dimungkinkan karena penerjemahan dapat dilakukan tanpa bergantung pada urutan definisi. Dependensi siklik antarb​​erkas Rust memang dilarang di Coq, tetapi pemisahan tetap bisa dilakukan.

Ukuran output

• alloc: 54 berkas Coq, 171.783 baris kode Coq
• core: 190 berkas Coq, 592.065 baris kode Coq

Keuntungan pemisahan kode

• Kode yang dihasilkan lebih mudah dibaca dan ditelusuri
• Kompilasi lebih mudah karena bisa dilakukan secara paralel
• Debugging lebih mudah karena dapat fokus pada satu berkas
• Lebih mudah mengabaikan berkas yang tidak bisa dikompilasi
• Lebih mudah melacak perubahan pada satu berkas sehingga maintenance lebih sederhana

Perbaikan beberapa bug 🐞

• Ada bug akibat konflik antar nama modul. Ini terjadi saat memilih nama modul untuk blok impl.
• Lebih banyak informasi ditambahkan ke nama modul untuk meningkatkan keunikannya. Misalnya, dengan menambahkan klausa where.

Contoh

• Implementasi tipe Mapping untuk trait Default:

  #[derive(Default)]
  struct Mapping<K, V> {
    // ...
  }
  

• Kode Coq sebelumnya:

  Module Impl_core_default_Default_for_dns_Mapping_K_V.
  (* ...trait implementation ... *)
  End Impl_core_default_Default_for_dns_Mapping_K_V.
  

• Kode Coq setelah perbaikan:

  Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V.
  (* ... *)
  

Daftar berkas yang tidak dapat dikompilasi

• 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 mencakup 4% dari seluruh berkas. Bahkan pada berkas yang berhasil dikompilasi pun masih mungkin ada struktur Rust yang belum tertangani.

Contoh 🔎

Kode asli metode unwrap_or_default pada tipe Option

pub fn unwrap_or_default(self) -> T
where
  T: Default,
{
  match self {
    Some(x) => x,
    None => T::default(),
  }
}

Kode Coq hasil terjemahan

Definition unwrap_or_default (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
  let Self : Ty.t := Self T in
  match τ, α with
  | [], [ self ] =>
    ltac:(M.monadic
      (let self := M.alloc (| self |) in
      M.read (|
        M.match_operator (|
          self,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.get_struct_tuple_field_or_break_match (|
                    γ,
                    "core::option::Option::Some",
                    0
                  |) in
                let x := M.copy (| γ0_0 |) in
                x));
            fun γ =>
              ltac:(M.monadic
                (M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                    []
                  |)
                |)))
          ]
        |)
      |)))
  | _, _ => M.impossible
  end.

Kode fungsi yang disederhanakan

Definition unwrap_or_default {T : Set}
  {_ : core.simulations.default.Default.Trait T}
  (self : Self T) :
  T :=
  match self with
  | None => core.simulations.default.Default.default (Self := T)
  | Some x => x
  end.

• Definisi yang disederhanakan ini digunakan saat verifikasi kode. Pembuktian ekuivalensinya ada di CoqOfRust/core/proofs/option.v.

Kesimpulan

• Dengan memformalkan standard library, pekerjaan verifikasi program Rust menjadi dapat dipercaya.

• Target berikutnya adalah menyederhanakan proses pembuktian yang masih merepotkan. Secara khusus, mereka ingin memisahkan langkah-langkah seperti resolusi nama, pengenalan tipe tingkat lanjut, dan penghapusan efek samping dalam proses menunjukkan bahwa simulasi ekuivalen dengan kode Rust asli.

• Jika tertarik pada verifikasi formal untuk proyek Rust, silakan hubungi [e-mail]. Verifikasi formal memberikan tingkat keamanan tertinggi dengan menjamin secara matematis tidak adanya bug terhadap spesifikasi yang diberikan.

Tag:

• coq-of-rust
• Rust
• Coq
• terjemahan
• core
• alloc

Opini GN⁺

1. Integrasi Rust dan Coq: Integrasi Rust dan Coq sangat membantu meningkatkan keandalan program Rust. Menggabungkan keamanan Rust dengan verifikasi formal Coq sangat berguna, terutama untuk aplikasi penting.
2. Pentingnya otomasi: Penerjemahan otomatis menggunakan alat coq-of-rust lebih andal dibanding kerja manual. Namun, karena error masih dapat muncul dalam proses verifikasi, kehati-hatian tetap diperlukan.
3. Pengelolaan codebase kompleks: Dalam menangani codebase besar, pemisahan kode sangat membantu maintenance dan debugging. Ini merupakan faktor penting terutama dalam kerja tim.
4. Kebutuhan verifikasi formal: Verifikasi formal sangat penting khususnya di bidang kritis seperti keuangan, medis, dan penerbangan. Kombinasi Rust dan Coq dapat memberi nilai besar di bidang-bidang ini.
5. Pertimbangan adopsi teknologi: Saat mengadopsi teknologi baru, perlu mempertimbangkan learning curve dan kompatibilitas dengan sistem yang ada. Alat verifikasi formal seperti Coq bisa memiliki learning curve yang tinggi, sehingga dibutuhkan pelatihan dan persiapan yang memadai.

[GN⁺]

Komentar Hacker News

Ringkasan kumpulan komentar Hacker News

• Keandalan alat terjemahan otomatis

  • Alat terjemahan otomatis mulai mendapat kepercayaan. coq-of-rust ditulis dalam Rust dan dapat dikonversi ke Coq untuk membuktikan kebenarannya. Ini mirip dengan cara mencegah serangan Ken Thompson.

• Ukuran program dan verifikasi

  • Ukuran program yang diverifikasi dengan sistem pembuktian semi-otomatis seperti Coq cenderung kecil. Biaya untuk jaminan 100% bisa 10 kali lipat dibanding biaya untuk jaminan 99,9999%.

• Kemungkinan kesalahan dalam proses penerjemahan

  • Ada kemungkinan besar terjadi kesalahan dalam proses menerjemahkan kode ke Coq. Hal ini menimbulkan keraguan terhadap validitas verifikasi atas kode sumber asli.

• Postingan terkait kripto

  • Ada yang membagikan sebuah posting blog dengan sedikit muatan terkait kripto. Ada juga posting yang membahas pendekatan serupa untuk Python.

• Batasan verifikasi formal

  • Ada yang ingat pernah menemukan bug pada kompiler C yang telah diverifikasi secara formal. Ini memunculkan pertanyaan tentang keandalan Coq itu sendiri dan proses penerjemahannya.

• Verifikasi formal Rust

  • Ada yang bertanya apakah jika pustaka standar dasar Rust diverifikasi secara formal, maka kualitas verifikasi formal atas penanganan memori dapat diperoleh selama tidak menggunakan kode unsafe.

• Penulisan spesifikasi verifikasi formal

  • Ada yang bertanya apakah menulis spesifikasi verifikasi formal mirip dengan menulis property test yang lebih kompleks. Menulis property test sendiri sudah sulit dan memakan waktu.

• Perbandingan dengan pendekatan lain

  • Ada permintaan untuk membandingkan perbedaan pendekatan dengan Aeneas atau RustHornBelt. Mereka penasaran bagaimana pointer dan mutable borrow ditangani.

• Adopsi Rust di kernel

  • Ada yang bertanya apakah upaya seperti ini dapat mempercepat adopsi Rust di kernel.

• Penambahan backend Rust untuk F*

  • Ada yang bertanya berapa banyak pekerjaan yang dibutuhkan untuk menambahkan backend Rust ke F*.