Trail of Bits’ten Fredrik Dahlgren, 18 Eylül 2026 tarihli yazıda AI’nin güvenlik denetiminde yalnızca “ajanla kod tarama”dan ibaret olmadığını anlatıyor. Ekip, Miden zkVM denetimine hazırlanırken ajanlara altı ay boyunca özel araçlar ve biçimsel modeller kurdurduklarını; bunların hem gerçek güvenlik bulgularına hem de makineyle doğrulanmış kanıtlara yol açtığını yazıyor. (Bu yazı, sitedeki 1Password AI yama benchmark eleştirisinden ayrı bir konu.)
Miden neden zordu?
Miden, kendi assembly dili (MASM) olan yeni bir sıfır-bilgi VM’i; neredeyse hiç geliştirici aracı yoktu. Yığın makinesi mimarisi nedeniyle girdiler/çıktılar örtük; imzasız prosedürler ve tanımsız çağrı kuralları statik analizi zorlaştırıyor. Miden ekibi 2025 sonlarında çekirdek kütüphanenin bir kısmını lansman öncesi incelettirdi.
Ajanlarla inşa edilen araçlar
Hazırlık süresinde ajanlar sıfırdan bir LSP sunucusu (sözdizimi, goto-definition, referanslar, satır içi yığın etkileri), bir decompiler, bir statik analiz motoru ve VM yürütücüsünün Lean modelini üretti. Bu araçlar, örneğin doğrulanmamış prover girdilerinin kötü niyetli bir prover’ın Falcon imzalarını sahteleyip Miden hesap sahiplerinden fon çalmasına izin verebileceği gibi gerçek güvenlik sorunlarını buldu. Lean çalışması Miden çekirdek kütüphanesinin büyük bir bileşenini kapsayan 95 makine doğrulamalı doğruluk kanıtı üretti; birim testlerin kaçırdığı iki ince hata da bulundu.
Mesaj
Dahlgren’e göre iki yıl önce bu derinlik mümkün olmazdı. Güvenlik firmalarının ajan yazıları çoğunlukla kod incelemesine odaklanırken Trail of Bits, inceleme başlamadan önce özel araç ve biçimsel model üretmenin denetim kalitesini yükselttiğini savunuyor.
Kaynak: Trail of Bits – Auditing in the age of (good enough) AI
Henüz yorum yok. İlk yorumu siz yapın!