Lean membuktikan kebenaran program, tetapi bug tetap ditemukan di dalamnya

 (kirancodes.me)
1 poin oleh GN⁺ 6 hari lalu | 1 komentar | Bagikan ke WhatsApp
  • Hasil fuzzing pada implementasi zlib yang telah diverifikasi secara formal menemukan heap buffer overflow di lean_alloc_sarray milik runtime Lean 4
  • Setelah lebih dari 100 juta pengujian menggunakan AI fuzzer Claude, AFL++, dan AddressSanitizer, terkonfirmasi 4 crash dan 1 kerentanan memori
  • Masalah yang ditemukan terbagi menjadi dua: overflow di runtime dan penolakan layanan (DoS) berbasis Out-of-Memory di Archive.lean
  • Algoritme kompresi dan dekompresi yang telah diverifikasi terbukti aman, tetapi kerentanan tetap ada di parser arsip dan lapisan runtime yang belum diverifikasi
  • Kesimpulannya, verifikasi formal sangat kuat, tetapi tanpa menjamin keamanan Trusted Computing Base (TCB), stabilitas sistem secara keseluruhan tidak bisa dijamin

Bug ditemukan pada program yang lolos verifikasi Lean

  • Hasil fuzzing pada implementasi zlib yang diverifikasi secara formal dengan Lean menemukan heap buffer overflow di runtime Lean 4
    • Kode aplikasi yang telah diverifikasi tidak memiliki kerentanan memori
    • Namun, overflow terjadi di fungsi lean_alloc_sarray milik runtime Lean dan memengaruhi semua versi Lean 4
  • Dilakukan lebih dari 100 juta putaran fuzzing menggunakan AI fuzzer Claude, AFL++, AddressSanitizer, Valgrind, UBSan, dan lainnya
    • 16 fuzzer paralel dijalankan terhadap 6 permukaan serangan, termasuk kompresi, dekompresi, dan pemrosesan arsip di lean-zip
    • Dalam 19 jam, ditemukan 4 input yang menyebabkan crash dan 1 kerentanan memori
  • Dua bug utama terkonfirmasi
    • Heap buffer overflow di lean_alloc_sarray pada runtime Lean
    • Penolakan layanan (DoS) berbasis Out-of-Memory di modul Archive.lean milik lean-zip
  • Batasan verifikasi formal pun terlihat jelas
    • Algoritme kompresi dan dekompresi di lean-zip telah diverifikasi sepenuhnya, tetapi parser arsip (Archive.lean) tidak diverifikasi sehingga memiliki kerentanan DoS
    • Bug runtime adalah masalah di dalam Trusted Computing Base, sehingga berdampak pada semua program Lean
  • Kesimpulannya, verifikasi formal Lean membuktikan kestabilan kode aplikasi, tetapi komponen di luar cakupan verifikasi tetap dapat menyimpan kerentanan
    • Verifikasi hanya kuat dalam ruang lingkup yang dicakupnya, dan keamanan lapisan kepercayaan dasar tetap mutlak diperlukan

Ringkasan eksperimen fuzzing

  • Basis kode yang diuji adalah implementasi zlib terverifikasi dari lean-zip
    • Semua theorem, specification, dokumentasi, dan binding C FFI dihapus sehingga hanya menyisakan kode Lean murni
    • Claude dibuat tidak mengetahui bahwa kode tersebut telah diverifikasi, untuk mencegah bias

  • Lingkungan eksperimen

    • 16 fuzzer paralel dijalankan terhadap 6 permukaan serangan: ZIP, gzip, DEFLATE, tar, tar.gz, compression
    • AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck, flawfinder, dan lainnya dipakai bersamaan
    • Total 105,823,818 eksekusi dengan 359 file seed, termasuk 48 file exploit buatan tangan
    • Dalam 19 jam, ditemukan 4 input crash dan 1 kerentanan memori

Bug 1: Heap buffer overflow di runtime Lean

  • Fungsi rentan: lean_alloc_sarray
    • Fungsi yang mengalokasikan semua array skalar seperti ByteArray, FloatArray, dan lainnya
    • Perhitungan sizeof(lean_sarray_object) + elem_size * capacity dapat mengalami integer overflow

  • Penyebab masalah

    • Saat capacity mendekati SIZE_MAX, penjumlahan mengalami overflow sehingga buffer kecil dialokasikan
    • Setelah itu pemanggil membaca n byte dan terjadilah heap buffer overflow

  • Kondisi pemicu

    • Terjadi saat nbytes di lean_io_prim_handle_read bernilai sangat besar
    • Dapat direproduksi dengan file 156 byte yang memiliki header ZIP64 dengan compressedSize sebesar 0xFFFFFFFFFFFFFFFF
    • Berdampak pada semua versi Lean 4, termasuk nightly terbaru
    • Contoh kode reproduksi
    def main : IO Unit := do
  IO.FS.writeFile "test.bin" "hello"
  let h ← IO.FS.Handle.mk "test.bin" .read
  let n : USize := (0 : USize) - (1 : USize)
  let _ ← h.read n
    • Menjalankan kode di atas memicu overflow di lean_alloc_sarray
    • PR perbaikan telah diajukan

Bug 2: Penolakan layanan (DoS) di parser arsip lean-zip

  • Fungsi rentan: readExact (Archive.lean)
    • Menggunakan langsung field compressedSize dari direktori pusat ZIP tanpa validasi
    • Saat memanggil h.read, ukuran yang diminta bisa sangat besar sehingga memicu alokasi memori berlebihan dan OOM

  • Reproduksi masalah

    • Jika file ZIP 156 byte mengklaim ukuran hingga beberapa exabyte, proses akan berhenti dengan INTERNAL PANIC: out of memory
    • unzip bawaan sistem memvalidasi ukuran pada header, tetapi lean-zip tidak melakukannya

Bagian yang luput dari verifikasi formal

  • Penyebab kerentanan DoS

    • Modul Archive.lean berada di area yang tidak diverifikasi
    • Pipeline kompresi dan dekompresi, seperti DEFLATE, Huffman, dan CRC32, telah diverifikasi sepenuhnya dan tidak bermasalah
    • Kerentanan muncul pada bagian yang tidak tercakup verifikasi

  • Hakikat overflow di runtime

    • Runtime Lean termasuk dalam Trusted Computing Base (TCB)
    • Semua pembuktian Lean mengasumsikan runtime berjalan dengan benar
    • Karena itu, bug pada runtime memengaruhi keamanan semua program Lean

Kestabilan kode yang telah diverifikasi

  • Hasil dari 105 juta eksekusi

    • Pada kode C yang dihasilkan Lean, tidak ditemukan heap overflow, use-after-free, stack overflow, UB, maupun akses di luar batas array
    • Menurut evaluasi Claude, basis kode ini termasuk “salah satu basis kode yang paling aman terhadap memori”

  • Efek sistem tipe Lean

    • Dengan dependent types dan struktur well-founded recursion, kelas kerentanan umum (kelas CVE) yang sering muncul pada implementasi zlib berbasis C/C++ dapat dicegah secara struktural

  • Kesimpulan

    • Area kode yang diverifikasi terbukti sangat kokoh dan sulit dipatahkan oleh fuzzer
    • Namun, kerentanan tetap ada pada bagian yang tidak diverifikasi dan pada lapisan runtime
    • Verifikasi dibatasi oleh cakupan penerapannya dan oleh keamanan basis kepercayaan

Pelajaran utama

  • Verifikasi formal sangat kuat di area kode yang benar-benar dicakup, tetapi komponen sekitar yang belum diverifikasi maupun lapisan runtime tetap bisa mengancam kestabilan keseluruhan
  • Keamanan Trusted Computing Base wajib dijamin, dan bahkan pada sistem yang telah diverifikasi pun pertanyaan “siapa yang mengawasi para pengawas? (Quis custodiet ipsos custodes)” tetap tersisa

Tautan referensi

Bacaan terkait

1 komentar

 
GN⁺ 6 hari lalu
Komentar Hacker News

  • Judul dan framing tulisan ini terasa agak aneh
    Penulis sebenarnya dengan jelas mengatakan bahwa ia tidak menemukan bug atau error di dalam kode yang telah dibuktikan
    Dua bug yang ditemukan berada di luar cakupan pembuktian, yang satu adalah spesifikasi yang terlewat, dan yang lain adalah heap overflow pada runtime C++
    Saya ingin menekankan bahwa bug yang ditemukan ada di runtime Lean, bukan di kernel yang melakukan verifikasi
    Lihat dokumentasi Lean

    • Saat membahas bug dalam sistem yang terverifikasi, menurut saya kita harus mempertimbangkan seluruh binary
      Jika Anda kehilangan bitcoin karena buffer overflow, fakta bahwa bug itu ada di runtime tidak akan terlalu menghibur
      Juga, jika program crash, kebanyakan pengguna akan menganggap itu sebagai bug
      Cukup banyak orang juga mungkin menjalankan Lean di lingkungan production nyata
    • Dari judulnya saya mengira ada bug di kernel Lean, padahal sebenarnya masalahnya ditemukan di runtime Lean dan lean-zip
      Jika bukan di kernel, maka dampaknya terhadap keandalan pembuktian itu sendiri tidak besar
    • Spesifikasi yang terlewat pada lean-zip adalah masalah penting dari sudut pandang filosofi verifikasi
      Bahkan jika Anda memverifikasi program “Hello world”, Anda harus menspesifikasikan bukan hanya output-nya tetapi juga efek samping-nya
      Jika korupsi memori bisa terjadi di batas antara runtime dan kernel, keandalan pembuktian bisa menurun
      Pada akhirnya, yang paling penting adalah mendefinisikan dengan jelas “apa yang harus diverifikasi”
    • Melihat daftar tulisan di situs ini, rasanya lucu karena makin lama makin terasa clickbait
      Daftar tulisan terkait
    • Menyebut bug di runtime Lean sebagai bug lean-zip itu seperti menyebut bug di JRE sebagai bug aplikasi Java
      Penulis tampak seperti sengaja mendorong pembaca ke arah kesalahpahaman

  • Saya juga pernah mengalami hal serupa dengan kode yang telah dibuktikan
    Dalam kasus saya, masalahnya bukan overflow melainkan cacat spesifikasi (spec bug)
    Jika spesifikasinya salah, maka kode dan buktinya bisa sempurna tetapi tetap bekerja berbeda dari perilaku yang dimaksud
    Pada akhirnya, kesulitan verifikasi terletak pada mengekspresikan niat manusia secara akurat
    Keyakinan bahwa AI akan menyelesaikan verifikasi secara sempurna bisa memberi rasa yakin yang keliru

    • Saya juga punya pengalaman serupa
      Spesifikasi yang bisa dibuktikan dengan alat seperti Lean, TLA+, dan Z3 biasanya disederhanakan dan memerlukan banyak asumsi
      Meski begitu, ini tetap alat yang sangat kuat
      Ia membantu mempersempit bug dalam algoritme yang kompleks dan membuat batas spesifikasi terlihat jelas
      Berkat AI, pekerjaan pembuktian seperti ini jadi jauh lebih mudah
    • Pertanyaan yang selalu muncul adalah “bagaimana kita bisa mempercayai sistem verifikasinya sendiri”
      Program lain yang memverifikasi sebuah program pada akhirnya juga bisa memiliki bug
      Kemustahilan verifikasi diri yang sepenuhnya lengkap mengingatkan pada prinsip ketidakpastian Heisenberg
      Pada akhirnya, verifikasi adalah proses meningkatkan kepercayaan melalui “implementasi independen kedua”
    • Bug di kode saya terbagi menjadi dua jenis
      (1) berjalan berbeda dari yang dimaksud
      (2) berjalan sesuai maksud, tetapi maksudnya sendiri salah
      Proof assistant dapat mencegah (1), tetapi tidak dapat mencegah (2)
      Artinya, soundness desain tidak bisa dibuktikan
      Memverifikasi semuanya seperti seL4 terlalu mahal dan memakan waktu lama
    • Menurut saya kita membutuhkan cara untuk memverifikasi spesifikasi itu sendiri
      Idealnya, kita menggabungkan logika formal + adversarial thinking untuk mencantumkan secara lengkap apa yang harus dilakukan program dan apa yang tidak boleh dilakukannya

  • Judulnya terasa seperti clickbait
    Tidak ada bug pada bagian yang dibuktikan, jadi saya tidak paham kenapa ditulis seperti itu
    Di HN saya ingin membaca tulisan yang berbasis fakta, dan ini terasa seperti membuang waktu

    • Apakah adil untuk mengatakan bahwa dalam perangkat lunak terverifikasi “hanya bug yang melanggar pembuktian yang dihitung sebagai bug”?
      Ia diiklankan sebagai “tanpa bug”, tetapi pada kenyataannya hanya “dalam cakupan yang diekspresikan sempurna oleh spesifikasi”
      Sesuatu bisa benar dalam keadaan mati — artinya, secara teoretis benar tetapi dalam praktiknya tetap rusak
    • Judulnya memang benar secara teknis, tetapi ia menggambarkan masalah pada kode lean-zip yang tidak diverifikasi seolah-olah itu bug pada bagian yang telah dibuktikan
    • Pada akhirnya, pesan “jelaskan dengan tegas cakupan bagian yang dibuktikan” itu menarik dan masuk akal
    • Bug kedua tampak seperti dibuat-buat tanpa dasar
      Tidak ada rujukan kode, dan kalau melihat kode aslinya, jelas bahwa itu adalah salah paham
    • Pada akhirnya lean-zip hanyalah binding Zlib

  • Masalah seperti ini juga sering muncul dalam verifikasi sistem terdistribusi
    Pembuktian hanya valid di dalam kondisi tertentu (operating envelope), dan kegagalan yang menarik biasanya terjadi di batas-batas itu
    TLA+ juga sama, jika realitas keluar dari asumsi, pembuktian menjadi tidak berarti
    Yang saya inginkan adalah kemampuan untuk mendeklarasikan operating envelope secara mekanis dan memantaunya saat runtime

    • Saya juga pernah menemukan bug hardware CPU secara langsung
      Tetapi kebanyakan bug bukan berasal dari hardware, melainkan karena orang tidak membaca dokumentasi
      Dengan pemodelan formal saja, jumlah bug sudah bisa dikurangi sangat banyak

  • Ini kabar baik yang cukup mudah diprediksi
    Ini berarti LLM bisa menghasilkan kode yang lolos verifikasi formal
    Ke depannya, bug akan makin banyak bergeser ke lapisan hardware
    Pada akhirnya kita akan membutuhkan formalisasi spesifikasi hardware
    Jika pabrikan tidak membukanya, bisa timbul konflik dengan komunitas
    Dalam jangka panjang, arahnya akan bercabang menjadi kepunahan kerentanan atau penyisipan yang disengaja

  • Awalnya saya mengira penulis tidak menguji bagian yang sudah dibuktikan
    Namun setelah dibaca, bug justru ditemukan di luar cakupan pembuktian
    Jadi judulnya terasa agak hiperbolis

    • Penulis postingannya sendiri ikut muncul
      Ia berargumen bahwa jika itu adalah bug pada sistem terverifikasi, maka seluruh binary harus menjadi objek yang dinilai
      Ia juga mengungkapkan bahwa ia benar-benar menemukan input yang memicu crash pada bagian parsing header kompresi di Archive.lean

  • Ini mengingatkan pada kutipan terkenal Donald Knuth
    “Waspadalah, mungkin ada bug di kode di atas; saya hanya membuktikan bahwa itu benar, saya belum menjalankannya”

  • Tidak memverifikasi parser tampak seperti kesalahan besar
    Parsing format binary selalu merupakan area yang berbahaya

  • Intinya adalah agen AI bekerja sama dengan fuzzer dan menemukan heap buffer overflow di Lean
    Ini pencapaian yang cukup besar

    • Menurut saya ini penemuan yang sangat berguna

  • Bagian ketika Claude mengatakan “ini salah satu codebase paling aman terhadap memori yang pernah saya analisis” terasa mengesankan
    Tetapi ini terdengar seperti lelucon seolah-olah itu codebase pertama yang pernah dianalisis Claude

    • Claude yang dilatih luas dengan RL jelas bukan baru pertama kali menganalisis code
      Justru itu alasan kenapa ia bisa sebagus ini
    • Mungkin Claude sedang melakukan sesuatu yang rahasia yang tidak kita ketahui 😄