Bug Borrow Checker Rust: Makna Soundness yang Sebenarnya

Sistem tipe Rust seharusnya memberi janji yang tegas: jika kode safe-mu lolos kompilasi, ia tidak mungkin punya dangling pointer, data race, atau use-after-free. Jadi ketika sebuah issue di GitHub menunjukkan potongan Rust yang kelihatannya aman tapi malah mencetak sampah dari stack frame yang sudah mati, dan ternyata lubangnya sudah ada di borrow checker Rust selama sebelas tahun, banyak orang merasa pijakannya goyah. Bug ini membiarkan syarat lifetime sebuah struct lolos lewat assignment covariant pada field. Dengan impl Drop yang jahat, kamu bisa menyimpan referensi ke variabel lokal di sebuah global lalu membacanya setelah variabel itu hilang. AddressSanitizer menyebutnya stack-use-after-scope. Compiler-nya menganggap semuanya baik-baik saja.

Reaksinya bisa ditebak. Ada yang langsung menyatakan cerita keamanan Rust sudah tamat. Ada juga yang angkat bahu: namanya juga bug. Keduanya melewatkan bagian yang menarik. Bug ini adalah eksperimen alami yang bersih tentang nilai jaminan statis, di mana penalaran informal mulai runtuh, dan mengapa jarak antara “sistem tipenya sound” dan “compiler benar-benar menegakkan sistem tipe yang sound” adalah tempat bug paling menarik bersembunyi. Jadi mari kita uji satu per satu kepercayaan umum yang muncul dari cerita ini.

Mitos 1: Bug Unsoundness Berarti Model Keamanan Rust Gagal

Insting pertama adalah menganggap ini sebagai retakan pada teorinya. Bukan. Tidak ada yang menulis ulang aturan lifetime. Tidak ada yang menemukan bahwa ownership dan borrowing ternyata rusak dari dasarnya. Sistem tipe Rust, sebagaimana dirancang di papan tulis dan di RFC, menyatakan program ini harus ditolak. Compiler-nya saja yang gagal menolaknya.

Perbedaan antara spesifikasi dan implementasi ini adalah salah satu patahan tertua di bidang kita. Tony Hoare memberi kita teori communicating sequential processes yang indah; lalu selama bertahun-tahun compiler C salah mengompilasi kode yang sebenarnya valid menurut standar. Teorinya tetap utuh sementara artefaknya bocor. Kami pernah menulis tentang celah spesifikasi-implementasi tempat bug bersarang, dan kasus ini contoh buku teksnya. Aturan lifetime-nya tidak salah. Kode inferensi variance di rustc, bagian yang memutuskan kapan boleh menggantikan &'a T dengan &'static T, punya lubang ketika assignment mengalir lewat field covariant.

Ini bentuk exploit-nya, disederhanakan. Kamu membuat wrapper yang impl Drop-nya menyalin payload ke penyimpanan global 'static. Biasanya compiler memaksa payload menjadi 'static, sehingga referensi ke variabel lokal tidak bisa masuk. Bug ini memungkinkanmu “mencuci” referensi berumur pendek lewat assignment covariant, sehingga wrapper akhirnya menyimpan &l padahal l adalah String lokal:

struct Q<T: 'static + Send>(Option<T>);
impl<T: 'static + Send> Drop for Q<T> {
fn drop(&mut self) {
if let Some(t) = self.0.take() {
KEPT.lock().unwrap().push(Box::new(t)); // escapes to 'static!
}
}
}
fn main() {
{
let l = String::from("hello world, this is long enough");
let mut q = Q(None);
q.0 = Some(&l); // should be rejected; 'static required
} // <- drop runs here, stashing &l in KEPT
// l is gone; KEPT now holds a dangling &'static String
}

Setiap baris secara individual terlihat tidak berbahaya. Unsoundness-nya hanya muncul dalam komposisi: field covariant, assignment yang melonggarkan batas lifetime, dan Drop yang memindahkan payload ke tempat yang lebih panjang umurnya dari referent-nya. Itulah ciri khas bug implementasi pada checker. Invariannya bersifat global, tapi penegakannya bersifat lokal, dan satu jalur kode lupa memeriksa.

Jadi, tidak, model keamanannya tidak gagal. Penegakan model keamanannya yang gagal. Itu kegagalan yang lebih kecil, tapi seperti akan kita lihat, bukan kegagalan yang sepele.

Mitos 2: Tidak Terdeteksi Selama Sebelas Tahun Berarti Bug-nya Tidak Berbahaya

Logika triase tim Rust kurang lebih begini: ini akan jadi P-critical kalau orang-orang sudah mengenainya, tapi sebelas tahun tanpa laporan berarti pemicunya tidak mudah, jadi P-high. Ada benarnya. Untuk benar-benar menyebabkan memory unsafety, kamu butuh impl Drop yang sengaja jahat dan memindahkan data ke lokasi 'static. Hampir tak ada yang menulis seperti itu. Permukaan paparan yang tidak disengaja itu sangat kecil.

Tapi frasa “jarang terpicu secara tidak sengaja” menanggung banyak beban di kalimat itu. Jaminan keamanan bukan hanya soal kecelakaan, melainkan soal apa yang bisa kamu andalkan ketika kode di sekitarmu tidak bersahabat. Seluruh gunanya sistem tipe yang sound adalah kamu bisa bernalar secara modular: aku tidak perlu mengaudit impl Drop-mu, karena compiler sudah membuktikan bahwa komposisi buruk tertentu tidak bisa diekspresikan. Begitu ada lubang, modularitas itu hilang. Dependensi jahat, atau dependensi yang keliru secara halus dari penulis yang berniat baik, kini bisa melakukan sesuatu yang oleh bahasa dijanjikan mustahil.

Sejarah penuh dengan bug “tidak bisa dieksploitasi” yang menjadi sangat bisa dieksploitasi begitu gadget yang tepat muncul. Pertanyaan praktisnya, seperti kata salah satu komentator, adalah apakah memperbaiki ini akan merusak crate nyata di ekosistem, dan jawabannya kemungkinan “sangat sedikit atau tidak ada”, yang merupakan kabar baik. Tapi pelajaran yang benar dari sebelas tahun yang sunyi bukanlah “bug-nya tidak berbahaya”. Melainkan bahwa ketiadaan bukti bukanlah bukti ketiadaan, terutama untuk mode kegagalan yang membutuhkan niat, bukan kebetulan.

Mitos 3: Banyak Mata Membuat Semua Bug Dangkal

Ini mitos yang seharusnya paling membuat kita malu. rustc adalah salah satu compiler paling banyak diteliti yang pernah ditulis. Ia open source, punya tim types yang khusus, komunitas akademik yang aktif (RustBelt memberi kita model formal dari inti Rust bertahun-tahun lalu), dan jutaan pengguna yang menguji setiap hari. Namun sebuah lubang soundness bersarang di inferensi lifetime selama lebih dari satu dekade, melewati penulisan ulang total mesin di sekitarnya.

Hukum Linus mengasumsikan banyak mata melihat ke tempat yang tepat dengan model yang tepat di kepala mereka. Unsoundness pada sistem tipe mengalahkan kedua asumsi itu. Mereka hidup di persimpangan beberapa fitur, seperti variance, urutan drop, coercion, dan trait bound, dan setiap fitur secara lokal benar. Reviewer membaca kode dan melihat invarian yang dimaksud, karena kode itu ditulis oleh orang-orang yang juga melihat invarian yang dimaksud. Bias konfirmasi sudah tertanam dalam prosesnya. Contoh penyangkal membutuhkan cara berpikir seperti penyerang, dan berpikir adversarial terhadap abstraksimu sendiri itu benar-benar sulit.

Ada situs counterexamples.org yang mengkatalogkan cara aturan tipe yang kelihatannya masuk akal bisa rusak, dan benang merahnya adalah mutabilitas yang dikombinasikan dengan hal rumit lainnya, persis bentuk bug ini. Ini bukan pelajaran baru. Sistem tipe ML pernah punya unsoundness terkenal seputar referensi mutable dan polimorfisme, yang diperbaiki dengan value restriction. Array Java bersifat covariant dan bisa melempar ArrayStoreException saat runtime karena perancang bahasa memilih kenyamanan ketimbang soundness. Semakin banyak yang berubah, semakin tiga fitur yang sama (subtyping, mutasi, dan generik) berkombinasi dan menggigit seseorang. Kalau kamu suka arkeologi semacam ini, sejarah enam puluh tahun Lisp menunjukkan betapa lamanya ide-ide ini berevolusi, dan aturan lama Rob Pike tentang kesederhanaan terbaca berbeda ketika kamu menyadari bahwa kompleksitaslah tempat lubang soundness berkembang biak.

Mata memang membantu, tapi tidak cukup. Posisi yang jujur, yang saya dengar dari seseorang yang sedang membangun bahasanya sendiri, kira-kira begini: tidak ada review yang bisa menyelesaikan setiap masalah, jadi kamu butuh metode mekanis yang tidak lelah dan tidak berbagi asumsimu.

Mitos 4: Penalaran Informal Pada Dasarnya Sudah Berupa Bukti

Ketika aturan lifetime Rust dirancang, aturan itu didiskusikan dengan cermat oleh orang-orang pintar, dengan banyak contoh. Itu penalaran informal, dan begitulah hampir semua compiler produksi dibangun. Hasilnya adalah sistem yang sound sejauh yang bisa dilihat siapa pun, yang, seperti yang sudah kita pelajari dua kali, ternyata tidak sama dengan sound.

Jarak di antara keduanya adalah tempat proyek seperti RustBelt dan pekerjaan berkelanjutan pada trait solver generasi berikutnya masuk. RustBelt, dibangun dengan Coq (sekarang Rocq) di atas framework separation-logic Iris, telah memverifikasi secara mesin sebuah model dari aturan tipe inti Rust, termasuk bagian yang menakutkan seperti batas abstraksi unsafe. Itu pencapaian besar. Tapi perhatikan apa yang dibuktikannya: sebuah model Rust, bukan rustc. Bukti itu mencakup kalkulus λRust, sementara compiler produksi sudah menyimpang, menumbuhkan fitur, dan menumpuk keputusan implementasi yang tidak pernah diverifikasi ulang. Isu ini adalah tagihan dari penyimpangan tersebut yang akhirnya jatuh tempo.

Memformalkan seluruh compiler produksi itu sangat mahal. CompCert, compiler C yang terverifikasi secara formal, butuh bertahun-tahun usaha para pakar untuk bahasa yang jauh lebih kecil dari Rust, dan ia memverifikasi pass kompilasi, bukan membuktikan bahwa sistem tipe sumbernya menangkap setiap program buruk. Tak ada yang akan menulis bukti Coq untuk dua juta baris rustc. Jalur yang realistis lebih mirip pertahanan berlapis:

• Model inti yang diverifikasi secara mesin (gaya RustBelt), sehingga teorinya sendiri tidak punya lubang.
• Fuzzing sistematis dan tooling analisis kasus yang menghasilkan program adversarial, yaitu sudut interaksi fitur yang tidak terpikirkan untuk diuji manusia.
• Mutation dan property-based testing pada checker: jika membalik sebuah bound seharusnya membuat program gagal, pastikan memang gagal. Budaya pengujian SQLite adalah teladannya di sini.
• Daftar terpelihara dari masalah unsound yang sudah diketahui (Rust punya lebih dari seratus yang ditandai) diperlakukan sebagai backlog dengan prioritas engineering, bukan sekadar folklore.

Menariknya, pencarian berbasis LLM mungkin justru menjadi nilai tambah di sini: alat yang tanpa lelah menggabungkan fitur dengan cara-cara bengkok adalah persis jenis adversary yang tidak dimiliki penalaran informal. Akhir cerita yang banyak dari kita harapkan adalah Rust yang dispesifikasikan secara formal dengan checker yang terbukti terhadap spesifikasinya. Tapi di antara sekarang dan sana, pekerjaannya membosankan, tidak glamor, dan berupa penyelesaian constraint yang melelahkan.

Mitos 5: Jika Soundness Tidak Absolut, Keamanan Statis Itu Penipuan

Pembacaan sinis berjalan begini: Rust menjanjikan keamanan, janji itu punya celah, jadi janji itu cuma pemasaran dan kita sebaiknya kembali ke YOLO-pointer di C. Ini kebalikan dari yang sebenarnya, dan layak dijelaskan dengan cukup presisi.

Soundness dalam sistem tipe adalah teorema tentang objek matematis. Yang diberikan bahasa produksi kepadamu adalah jaminan statistik dan ekonomis: seluruh kelas bug, seperti use-after-free, data race, dan iterator invalidation, berpindah dari “radiasi latar konstan dalam codebase-mu” menjadi “kejadian yang cukup langka untuk masuk halaman depan ketika ditemukan setelah sebelas tahun”. Bandingkan base rate-nya. Bug memory-safety di codebase C dan C++ berskala besar menyumbang mayoritas CVE serius tahun demi tahun, dan tidak ada lagi yang kaget dengan satu bug individual. Bug unsoundness Rust sangat jarang sehingga setiap bug mendapat issue GitHub sendiri, thread diskusi sendiri, dan budaya postmortem sendiri. Kelangkaan yang bisa kamu hitung adalah dunia yang berbeda dari kelangkaan yang tidak bisa kamu hitung.

Ada juga perbedaan dalam cara kegagalan bertumpuk. Di C, setiap baris adalah potensi bahaya memory-safety, jadi biaya kewaspadaan terus naik seiring ukuran kode. Di Rust, kewaspadaan terkonsentrasi di tepinya: blok unsafe, FFI, dan (seperti yang sekarang kita tahu) checker compiler itu sendiri. Konsentrasi itulah yang membuat audit, tooling seperti Miri, dan metode formal menjadi layak dilakukan. Jaminannya bukan biner; ini penataan ulang drastis tentang di mana risikomu berada.

Sistem tipe dengan bug yang diketahui, yang belum pernah terkena oleh sebelas tahun trafik produksi, tetap jauh lebih kuat dibanding bahasa yang bug-nya justru merupakan desainnya.

Yang Sebenarnya Perlu Kamu Bawa Pulang

Jika kamu menulis Rust, kamu tidak perlu mengubah apa pun. Kodemu tidak diam-diam tidak aman sebelum issue ini diajukan; jalur eksploit praktisnya membutuhkan niat. Jika kamu memelihara library, langkah yang jujur tetap sama seperti dulu: jaga permukaan unsafe tetap kecil, jalankan Miri pada bagian-bagian yang rumit, dan jangan memperlakukan borrow checker sebagai orakel untuk kode jahat orang lain. Perlakukan ia sebagai alat yang sangat andal untuk menangkap kesalahanmu sendiri.

Jika kamu membangun bahasa atau compiler, bug ini adalah hadiah: spesimen langka dan terdokumentasi dengan baik tentang bagaimana soundness benar-benar gagal di produksi. Bukan di teori, tapi di penegakannya; bukan di satu fitur, tapi di persimpangan fitur; bukan tertangkap oleh review, tapi oleh konstruksi adversarial. Tim yang serius menanggapi ini, yang mendanai rewrite trait solver, rework region-constraint, dan tooling yang dekat dengan verifikasi, adalah tim yang jaminannya akan berarti dalam sepuluh tahun.

Dan untuk kita semua: kalibrasi ulang apa itu jaminan. Kita sudah mengacaukan “terbukti” dengan “dijelaskan dengan meyakinkan dan belum pernah dibantah” selama puluhan tahun, di sistem tipe, protokol kriptografi, dan konsensus terdistribusi. Versi dewasa dari kepercayaan bukanlah mengasumsikan jembatannya sempurna. Melainkan tahu bahwa jembatan itu punya inspektur yang mempublikasikan temuan mereka, memperbaiki apa yang mereka temukan, dan menyimpan daftar publik retakan yang belum sempat diperbaiki. Dalam hal itu, sebelas tahun untuk menemukan sebuah lubang bukanlah dakwaan. Itu bukti bahwa sistemnya, yaitu sistem manusia di sekitar compiler, bekerja kurang lebih sebagaimana mestinya.