Metode yang Diformalisasi untuk Mengompilasi C ke Rust yang Aman

 (arxiv.org)
2 poin oleh GN⁺ 2024-12-22 | 1 komentar | Bagikan ke WhatsApp

  • Metode yang Diformalisasi untuk Mengompilasi C ke Rust yang Aman

  • Meskipun popularitas bahasa Rust meningkat pesat, banyak basis kode penting masih ditulis dalam C, dan menulis ulang secara manual tidak realistis. Karena itu, menerjemahkan C ke Rust secara otomatis muncul sebagai alternatif menarik.

  • Berbagai penelitian sebelumnya telah bergerak ke arah menangani semakin banyak bagian C dengan memanfaatkan fitur-fitur Rust (misalnya unsafe). Namun, meskipun otomasi tampak menjanjikan, menghasilkan kode yang bergantung pada unsafe akan meniadakan jaminan keamanan memori yang disediakan Rust, sehingga keuntungan utama dari porting basis kode lama ke bahasa yang aman memori menghilang.

  • Kami mengeksplorasi jalur lain untuk menerjemahkan C ke Rust yang aman, yaitu menghasilkan kode yang mematuhi sistem tipe Rust sehingga jaminan keamanan memori mudah dipenuhi.

  • Penelitian kami mencakup beberapa kontribusi unik:

    • translasi berbasis tipe untuk sebagian C ke Rust yang aman
    • analisis statis baru berbasis "pohon partisi" yang memungkinkan ekspresi aritmatika pointer C melalui slice dan operasi pemisahan di Rust
    • analisis yang secara tepat menyimpulkan borrow mana yang harus bersifat mutable
    • strategi kompilasi untuk tipe struct C yang kompatibel dengan pembedaan alokasi non-owner dan owner di Rust

  • Kami menerapkan metodologi ini pada basis kode C yang telah diverifikasi secara formal: perpustakaan kriptografi HACL* dan parser biner serta serializer EverParse. Hasilnya menunjukkan subset C yang kami dukung cukup untuk menerjemahkan kedua aplikasi tersebut ke Rust yang aman.

  • Hasil evaluasi menunjukkan bahwa untuk beberapa bagian yang melanggar disiplin aliasing Rust, refaktorasi operasional otomatis sudah memadai, dan pengaruh kinerja dari beberapa salinan strategis yang disisipkan hampir tidak signifikan.

  • Khususnya pada aplikasi pendekatan ini terhadap HACL*, 80.000 baris perpustakaan kriptografi terverifikasi yang mengimplementasikan semua algoritma modern berhasil ditulis sepenuhnya dalam Rust. Ini adalah kasus pertama.

Bacaan terkait

1 komentar

 
GN⁺ 2024-12-22
Komentar Hacker News

  • Setelah mem-porting proyek ke Rust, saya menemukan beberapa kesimpulan

    • Mengonversi program C menjadi Rust dapat dengan cepat menemukan bug berkat batasan ketat Rust
    • Konversi otomatis dari C ke Rust bukanlah solusi yang sepenuhnya tuntas karena desain kedua bahasa berbeda secara mendasar
    • Dalam beberapa kasus, porting dari C ke Rust mungkin tidak mungkin, karena terdapat ketidakamanan yang melekat pada desainnya
    • Kemajuan alat bantu kemungkinan akan membuat proses porting lebih lancar

  • Kode basis C yang telah diverifikasi secara formal berbeda dari kode basis C sistem yang umum

  • Pada tahun 2002, para peneliti menerbitkan makalah tentang Cyclone, sebuah dialek C yang aman, dan menemukan bug keamanan saat mem-porting dari C ke Cyclone

    • Konversi manual atau otomatis semacam ini berpotensi meningkatkan adopsi bahasa yang aman serta menemukan bug-bug yang sudah ada

  • Terjemahan langsung ke Rust dapat menghasilkan bagian aman dan tidak aman, dan pekerjaan manual dapat difokuskan untuk memverifikasi keamanan bagian yang tidak aman

    • Bahkan jika bagian tidak amannya besar, masih ada manfaatnya

  • Harapan terhadap pendekatan mengompilasi sebagian kecil dari C cukup rendah

    • Karena model kepemilikan Rust terlalu berbeda dari program C di dunia nyata

  • Rasa ingin tahu tentang perbandingan dengan fitur konversi C di Zig

    • Zig dapat membuat lingkungan campuran antara kode baru dan kode C lama dengan baik, dan juga dapat digunakan sebagai kompiler C
    • Ingin tahu mengapa para pemelihara Linux kernel tidak mempertimbangkan Zig sebagai pengganti C

  • Pertanyaan apakah C2Rust bisa menghasilkan kode yang benar secara formal

    • Tidak terlihat tautan ke source code yang menghasilkan kode Rust

  • Jika pustaka C berfungsi, menerjemahkan dengan memanfaatkan ketidakamanan Rust bisa jadi bernilai

    • Rust umumnya kurang memiliki pustaka

  • Menarik bahwa tingkat optimasi tinggi tidak begitu meningkatkan kecepatan Rust

    • Penasaran seberapa baik prosesnya bila mengompilasi langsung dari C ke Rust dengan tingkat optimasi O3