LEANGUARD: Araç Kullanan Ajanlar İçin Lean ile Doğrulanmış Güvenlik Korkulukları

Araç Kullanan Ajanlarda Politika İhlali Sorunu ve LeanGuard Mimarisi#

Araç kullanan (tool-using) dil modeli ajanları, çalışma sırasında sıklıkla alan politikalarının (domain policies) açıkça yasakladığı eylemleri yürütebilmektedir. Bu güvenlik ve güvenilirlik açığını kapatmak için geliştirilen LeanGuard, önerilen her araç çağrısını (tool call) henüz hedef ortama ulaşmadan önce Lean4 dilinde yazılmış bir politikaya karşı denetleyen bir çalışma zamanı (runtime) katmanı sunar.

LeanGuard mimarisinin temel çalışma prensipleri şunlardır:

• Zamansal Mantık ve Durum Önermeleri: Politikalar, mevcut durum önermelerini (state predicates) yürütme geçmişi üzerindeki kapsamlı geçmiş zamanlı zamansal operatörlerle (scoped past-time temporal operators) birleştirir.
• Güvenli Kapanma (Fail-Closed) ve Matematiksel Kanıt: Değerlendirme süreci fail-closed (hata durumunda işlemi reddetme) prensibiyle çalışır ve karar prosedürünün LeanLTL semantiği ile eşdeğer olduğu matematiksel olarak kanıtlanmıştır.

Reddedilen Çağrıları Düzeltme Mekanizmaları#

LeanGuard tarafından engellenen bir araç çağrısı iki farklı yaklaşımla düzeltilebilir:

• Geri Bildirim (Feedback) Yöntemi: Ajana ihlal edilen kural ve bir ipucu (hint) geri gönderilerek modelin kendi çağrısını düzeltmesi sağlanır.
• Kanıt Güdümlü Onarım (Proof-Guided Repair): Modele tekrar başvurmaya gerek kalmaksızın, Lean metaprogramlama yetenekleri kullanılarak kullanıcının niyetini koruyan yakın bir alternatif çağrı aranır ve politikanın bu yeni çağrıya izin verdiği matematiksel olarak kanıtlanır.

Deneysel Sonuçlar ve Performans Bulguları#

Makaledeki test sonuçları, biçimsel doğrulama (formal verification) tabanlı korkulukların üretim ortamındaki etkisini net biçimde ortaya koymaktadır:

• Tau-Bench Testleri: Beş farklı Qwen modeli (0.8B ile 27B arası) üzerinde yapılan testlerde, korumasız ajanlar Lean politikasının yasakladığı en az 33 çağrıyı yürütürken, LeanGuard hiçbir yasaklı çağrıya izin vermemiştir. Üstelik geri bildirim mekanizması kullanıldığında görev başarı oranında anlamlı bir düşüş yaşanmamıştır.
• DTap ve Prompt Injection Koruması: LeanGuard, doğrudan prompt-injection saldırılarının başarı oranını %57,9'dan %5,9'a düşürmüştür. İyi niyetli (benign) görevlerin yazma işlemi gerektirmediği telekom senaryolarında ise normal görev başarısı hiç değişmemiştir.
• Geri Bildirim ve Hızlı Onarım Verimliliği: Geri bildirim mekanizması, salt reddetmeye (bare denial) kıyasla tekrarlanan engellenmiş çağrıları azaltmış ve beş modelin dördünde görev başarısını artırmıştır. Yeniden oynatılan reddedilmelerde ise kanıt güdümlü onarım, argüman değerlerinden kaynaklanan 252 reddin 88'i için kabul edilebilir bir düzenlemeyi medyan 2 ms gibi çok düşük bir sürede kanıtlamıştır.

Yazılım Geliştirme ve Mühendislik Çıkarımları#

Modern yazılım mühendisliğinde Tool Calling ve Multi-Step Agent'lar geliştirirken ve Production'da Agent Güvenilirliği sağlarken yalnızca prompt tabanlı kısıtlamalara güvenmek yetersizdir:

• Deterministik Çalışma Zamanı Katmanı: LLM çıktıları olasılıksal olduğu için kritik API çağrılarının önüne deterministik ve fail-closed çalışan bir doğrulama katmanı eklenmelidir.
• Yapılandırılmış Hata Dönüşleri: Bir araç çağrısı engellendiğinde ajana sadece "reddedildi" demek yerine hangi kuralın ihlal edildiğini açıklayan geri bildirimler dönmek, döngüsel hataları önler ve görev başarısını korur.
• Düşük Gecikmeli Otomatik Onarım: Parametre kaynaklı hataları LLM'e yeniden sormak yerine kural tabanlı veya biçimsel doğrulama yöntemleriyle milisaniyeler içinde (örneğin 2 ms) onarmak, hem token maliyetini hem de sistem gecikmesini ciddi ölçüde azaltır.