Banyak tulisan dari firma keamanan belakangan ini bercerita soal cara mereka mengarahkan agen AI ke sebuah basis kode lalu menemukan puluhan bug. Trail of Bits menulis hal yang berbeda. Menurut mereka, agentic code review hanyalah satu bagian kecil dari cara AI dipakai dalam tinjauan keamanan. Bagian yang lebih menarik justru terjadi sebelum review kode dimulai.
TL;DR
- Trail of Bits menghabiskan enam bulan mengaudit sebagian Miden zkVM dengan agen AI yang terlebih dahulu membangun peralatan sendiri: LSP server, decompiler, mesin static analysis, dan model Lean dari eksekutor VM.
- Analisis berbasis abstract interpretation menemukan lebih dari 400 lokasi validasi tipe yang bisa diperbaiki, dan satu di antaranya berkategori high severity.
- Temuan high severity berasal dari nilai advice yang tidak divalidasi di prosedur mod_12289, yang bisa dipakai prover jahat untuk memalsukan tanda tangan Falcon dan menguras dana akun Miden.
- Pemodelan formal di Lean menghasilkan 95 bukti kebenaran untuk seluruh komponen aritmetika biner core library, dan menemukan dua bug halus di prosedur rotr dan wrapping_mul yang lolos dari unit test.
- Tim Miden mengadopsi mesin static analysis yang dikembangkan selama audit ini untuk mengamankan pembaruan core library ke depan.
Dalam audit terbaru mereka, tim Trail of Bits menghabiskan enam bulan membiarkan agen AI membangun peralatan sendiri: sebuah LSP server, sebuah decompiler, sebuah mesin static analysis, dan sebuah model Lean dari eksekutor VM. Semua dibangun dari nol. Peralatan itu kemudian menemukan masalah keamanan nyata, termasuk satu temuan berkategori high severity yang bisa dipakai memalsukan tanda tangan Falcon dan menguras dana pemegang akun.
Konteks: Miden VM dan bahasa assembly yang belum punya alat
Pada akhir 2025, tim Miden mendatangi Trail of Bits untuk mereview sebagian VM zero-knowledge mereka sebelum peluncuran. Salah satu bagian yang masuk lingkup review adalah Miden core library, yang berisi sekumpulan kecil primitif kriptografi yang ditulis dalam bahasa assembly khusus bernama Miden assembly atau MASM.
Dari sudut pandang auditor, kombinasi itu menarik sekaligus menyulitkan. Menarik karena proyeknya high-assurance dan menulis kode kriptografi kompleks di bahasa assembly tingkat rendah. Sulit karena bahasa itu sama sekali baru.
Masalah utamanya soal arsitektur. Miden VM memakai arsitektur stack machine, yang berarti setiap instruksi membaca nilai dari stack dan menuliskan hasilnya kembali ke puncak stack. Secara konsep sederhana, tapi bikin kode MASM susah direview: input dan output instruksi selalu implisit, tidak muncul di teks kode. Ditambah lagi, karena Miden VM arsitektur yang benar-benar baru, praktis belum ada dukungan IDE, LSP server, atau linter untuk bahasa itu.
Karena implementasinya belum feature complete dan mereka punya waktu enam bulan, pertanyaan yang mereka ajukan ke diri sendiri cukup tajam: apa yang bisa dihabiskan waktu dan token untuk memastikan review nanti menemukan sebanyak mungkin bug?
Membangun peralatannya lebih dulu
Langkah pertama adalah bertanya alat seperti apa yang mereka ingin sudah tersedia saat review dimulai. Karena biasanya memakai VS Code, syntax highlighting dan navigasi kode dianggap kebutuhan dasar untuk bisa mengikuti alur data di sebuah basis kode. Dari situ mereka butuh LSP server dan ekstensi VS Code.
Temuan bug dari audit Trail of Bits terhadap Miden core library
| Prosedur | Deskripsi masalah | Dampak |
|---|---|---|
| mod_12289 | Sisa pembagian dari prover tidak divalidasi sebelum dipakai | High severity; tanda tangan Falcon bisa dipalsukan |
| rotr | Perilaku salah untuk input besar jika rotasi kelipatan 32 | Lolos dari unit test yang ada |
| wrapping_mul | Membuang nilai milik pemanggil dari stack sebelum kembali | Lolos dari unit test yang ada |
Hasilnya cepat. Dalam beberapa hari, Claude membangun prototipe yang sudah menyediakan sebagian besar fungsi yang diinginkan: syntax highlighting, goto definition, pencarian referensi kode, dan menampilkan docstring prosedur saat kursor diarahkan. Setelah fitur dasar itu ada, mereka menambahkan fitur yang lebih spesifik bahasa, seperti dokumentasi instruksi inline dan efek stack untuk tiap instruksi. Tujuannya menghindari perpindahan konteks saat auditor harus mencari makna instruksi di tempat lain.
Perkakas kedua lebih ambisius: decompiler untuk prosedur MASM, supaya reviewer bisa cepat memahami alur kontrol dan alur data tingkat tinggi. Menurut Trail of Bits, ini masalah yang lebih sulit dari yang terlihat awalnya. Stack machine lifting dan decompilation memang bidang yang sudah banyak diteliti, tapi mendekompilasi MASM yang ditulis tangan tetap sulit karena beberapa alasan:
- Sebagian besar prosedur di core library tidak punya deklarasi signature, sehingga jumlah input dan output harus disimpulkan dari konteks.
- Prosedur MASM tidak mengikuti konvensi pemanggilan yang terdefinisi baik, dan efek stack bersih dari pemanggilan semacam itu umumnya tidak bisa ditentukan secara statis. Akibatnya, setiap kegagalan analisis menjalar ke atas sepanjang rantai pemanggilan.
- While-loop tidak harus stack neutral, yang berarti kondisi while-loop bisa menempati slot stack berbeda di setiap iterasi. Ini membuat pemetaan input instruksi ke slot stack untuk instruksi berikutnya jadi tidak mungkin.
- Cabang berbeda dalam pernyataan kondisional bisa punya efek stack yang berbeda, sehingga pelacakan stack dan inferensi signature ikut sulit.
Konsekuensinya mereka sadar tidak bisa mendekompilasi semua prosedur MASM kalau ingin hasilnya tetap benar. Jadi mereka membatasi diri: fokus mendekompilasi subset MASM yang terdefinisi baik dengan hasil yang benar.
Selama pengembangan, pola kerjanya menarik. Mereka bergantian memakai Claude untuk perencanaan dan pengembangan, dan Codex untuk review kode. Setiap kali fitur baru selesai, agen diminta mendekompilasi sekumpulan prosedur acak dari core library lalu membandingkan hasilnya dengan MASM asli untuk mencari regresi. Setiap masalah yang ditemukan ditambahkan sebagai regression test untuk diperbaiki model.
Decompiler ini jadi bagian terbesar dari pekerjaan perkakas, dengan lebih dari 100 commit buatan AI selama beberapa bulan. Menariknya, manfaat terbesar bukan pipeline dekompilasinya, melainkan kerangka analisis internal dan intermediate representation yang dihasilkan, karena keduanya bisa dipakai ulang untuk static analysis.
Abstract interpretation dan 400 lebih temuan validasi tipe
Dengan decompiler di tangan, mereka punya intermediate representation dari setiap prosedur, lengkap dengan input dan output instruksi yang sudah terisi sebagai ekspresi. Itu membuka pintu untuk membawa mesin static analysis standar, termasuk data flow analysis, ke masalah pencarian bug di kode MASM.
Mereka membangun sejumlah analysis pass di atas intermediate representation itu, menjawab pertanyaan seperti: apakah nilai advice dari prover seperti sisa pembagian dan modular inverse sudah divalidasi dengan benar, apakah batasan tipe seperti input harus bilangan bulat 32-bit atau boolean sudah ditegakkan, dan apakah variabel lokal sudah diinisialisasi di semua jalur eksekusi.
Salah satu teknik yang mereka pakai adalah abstract interpretation. Idenya sederhana: alih-alih menjalankan program dengan angka nyata, analisis melacak tipe nilai yang mungkin ada di stack di setiap langkah, misalnya bilangan bulat 32-bit atau unknown. Analisis berjalan berulang sampai tidak ada informasi baru yang ditemukan. Karena selalu melacak semua nilai yang mungkin dengan sedikit ruang ekstra, analisis ini tidak bisa melewatkan kasus nyata. Kalau sebuah pemeriksaan lolos di analisis, pemeriksaan itu dijamin berlaku di setiap eksekusi program yang sebenarnya.
Mereka memakai Claude dan Codex untuk membangun mesin abstract interpretation yang umum, lalu mengimplementasikan sejumlah analysis pass konkret di atasnya, dengan agen yang bergantian antara pengembangan dan review kode. Mereka juga meminta agen merancang antarmuka command line untuk decompiler dan linter MASM baru, supaya perkakas itu bisa dipakai di alur review kode yang digerakkan agen.
Hasilnya, saat review sebenarnya berjalan, analisis itu mengidentifikasi lebih dari 400 lokasi unik tempat validasi tipe bisa diperbaiki. Menurut Trail of Bits, hampir semua lokasi itu bisa dijangkau dari API publik library, sehingga developer pihak ketiga bisa memanggilnya tanpa validasi yang memadai. Dari 400 lebih itu, satu temuan berkategori high severity.
Temuan high severity: remainder yang tidak divalidasi
Temuan serius itu berasal dari nilai advice yang kurang dibatasi di prosedur mod_12289. Prosedur itu mereduksi nilai 64-bit modulo 12289, dengan hasil bagi dan sisa pembagian disediakan sebagai nilai advice oleh prover.
Di situ letak celahnya. Hasil baginya diperiksa supaya dipastikan bernilai 64-bit yang valid, direpresentasikan sebagai dua limb 32-bit. Tapi sisanya tidak pernah divalidasi sebelum diteruskan ke instruksi 32-bit u32overflowing_sub. Dengan mengubah-ubah hasil bagi dan sisa pembagian secara hati-hati supaya batasan yang dipaksakan operasi pengurangan tetap terpenuhi, peneliti menemukan bahwa mod_12289 bisa mengembalikan nilai yang bukan sisa pembagian yang benar.
Dampaknya bukan teoretis. Prover jahat bisa memanfaatkan itu untuk memalsukan tanda tangan Falcon dan menguras dana akun Miden mana pun yang dikendalikan pasangan kunci Falcon.
Pelajaran teknisnya umum dan sering terlewat: nilai yang disediakan prover adalah input prakomputasi yang datang dari stack advice terpisah dan harus divalidasi dengan sangat hati-hati. Memvalidasi satu bagian dari sepasang nilai tidak cukup kalau bagian lainnya dipakai di operasi aritmetika yang sama.
💬 Komentar (0)
Belum ada komentar. Jadilah yang pertama! 💬