Audit Kode Pakai AI Agent: Temuan Falcon Signature di Miden zkVM

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.

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.

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.

Ketika tidak ada bug: membuktikan dengan Lean

Pertanyaan berikutnya yang mereka ajukan cukup menarik: kalau prosedur di core library memang benar dan tidak berisi bug, apakah bisa dibuktikan memakai proof assistant seperti Lean?

Menurut mereka, Miden VM sangat cocok untuk pemodelan formal karena set instruksinya kecil dan sebagian besar instruksi tidak punya efek samping. Untuk memodelkan MASM secara formal, mereka mulai dengan mengimplementasikan eksekutor Miden VM minimal di Lean, lalu meminta Claude membangun penerjemah otomatis dari prosedur MASM ke Lean.

Saat review, beberapa agen bekerja paralel untuk membuktikan kebenaran sebanyak mungkin prosedur di seluruh library. Karena kernel Lean bisa memvalidasi bahwa proof yang dihasilkan benar, yang perlu diaudit manual hanyalah pernyataan teoremanya, untuk memastikan tiap teorema membuktikan properti kebenaran yang tepat untuk prosedur yang bersangkutan. Supaya teoremanya mudah direview, mereka memperkenalkan tipe Lean untuk elemen field dan tipe integer yang diimplementasikan di core library.

Hasil kerja pemodelan formal ini: 95 bukti kebenaran yang mencakup seluruh komponen aritmetika biner di core library. Lebih dari itu, pekerjaan ini menemukan dua bug halus yang tidak tertangkap unit test yang sudah ada:

• Kasus tepi di rotr, rotasi kanan 64-bit. Perilakunya salah untuk input besar yang melebihi Goldilocks prime jika besar pergeseran rotasinya kelipatan 32.
• Masalah di wrapping_mul, perkalian 256-bit. Prosedur itu membuang nilai milik pemanggil dari stack sebelum kembali.

Ada juga temuan menarik dari sisi proses: review manual mengungkap bahwa proof kebenaran untuk rotr 64-bit memerlukan asumsi tambahan, yaitu shift modulo 32 tidak sama dengan nol, supaya proof-nya bisa selesai.

Kenapa ini baru bisa dilakukan sekarang

Bagian yang paling relevan untuk tim engineering adalah soal ekonomi. Trail of Bits menyebut perkakas yang mereka kembangkan dan library serta proof Lean yang dihasilkan semuanya adalah proyek sampingan yang tidak akan mungkin dikerjakan satu atau dua tahun lalu. Proyek seperti itu sifatnya sangat eksploratif, hasil akhir dan potensi manfaatnya sulit diprediksi, sehingga sulit dijual ke klien di muka.

Yang berubah, menurut mereka, adalah agen sekarang cukup baik untuk membawa proyek non-esensial semacam ini dengan supervisi ringan. Itu mengubah perhitungan soal proyek mana yang layak dikejar. Proyek sampingan yang gagal, kata mereka, sekarang hanya memakan biaya token.

Manfaatnya di proyek Miden cukup jelas: LSP server dan mesin static analysis memperbaiki cakupan review manual, memperkuat review yang digerakkan agen, dan menemukan masalah keamanan nyata yang berpotensi menyebabkan kerugian dana besar. Proof kebenaran Lean yang dihasilkan AI juga menaikkan tingkat assurance di komponen library yang luas dan fundamental. Tim Miden sendiri mengadopsi mesin static analysis yang dikembangkan untuk review ini, sehingga proyek sampingan itu sekarang ikut mengamankan pembaruan core library ke depan.

Yang bisa diambil tim lain

Beberapa pelajaran praktis dari kasus ini, tanpa perlu punya tim audit sekelas Trail of Bits:

• Perkakas dulu, review kemudian. Waktu enam bulan dihabiskan untuk membangun LSP, decompiler, dan analysis engine sebelum review dimulai. Investasi di perkakas itulah yang membuat review manual dan review agen jauh lebih efektif.
• Pisahkan fase pengembangan dan fase review. Pola Claude untuk pengembangan dan Codex untuk review kode memberi sudut pandang kedua yang tidak menilai hasil kerjanya sendiri.
• Butuh verifikator deterministik. Yang membuat 95 proof Lean bisa dipercaya bukan agennya, tapi kernel Lean yang bisa memvalidasi hasilnya. Tanpa verifikator seperti itu, output agen tetap harus diperiksa manual sepenuhnya.
• Audit pernyataan, bukan hanya bukti. Untuk pekerjaan formal, yang diperiksa manual adalah teorema yang dibuktikan, bukan langkah pembuktiannya. Ini pembagian kerja yang penting: mesin memverifikasi, manusia memastikan pertanyaannya benar.
• Nilai advice adalah batas kepercayaan. Temuan high severity lahir dari satu nilai yang tidak divalidasi. Setiap input yang datang dari pihak yang tidak dipercaya adalah tempat pertama yang harus diperiksa.
• Regression test dari setiap temuan. Setiap masalah yang ditemukan selama pengembangan perkakas langsung diubah jadi regression test, bukan sekadar diperbaiki sekali.

Yang paling layak dicatat adalah pembagian perannya. Agen AI dipakai untuk hal yang memang sulit dijustifikasi secara komersial: membangun perkakas, menulis analysis pass, menerjemahkan bahasa assembly ke model formal. Penilaian akhir tetap di tangan manusia, yaitu memastikan teorema yang dibuktikan memang menyatakan properti yang benar. Kombinasi itu yang membuat proyek sampingan berubah jadi temuan keamanan yang berdampak.

Sumber

• Fredrik Dahlgren, "Auditing in the age of (good enough) AI", The Trail of Bits Blog, 18 September 2026: https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/
• Diskusi publik atas artikel tersebut di Hacker News, halaman depan 24 September 2026: https://news.ycombinator.com/item?id=44670000

Catatan: seluruh rincian teknis, angka temuan, dan hasil pembuktian dalam artikel ini bersumber dari tulisan Trail of Bits dan belum diverifikasi lewat pengujian independen. Detail spesifik soal kode Miden sebaiknya dikonfirmasi ke repositori resmi proyek.