LLM Destekli Formal Doğrulama nftables'ta İki Kritik Hata Buldu
Basis, LLM destekli formal doğrulama ile Linux'un nftables optimizasyoncusunda 2022'den beri süregelen iki kritik hata keşfetti.
Basis araştırmacıları, Linux'ta neredeyse her sistemde trafiği filtreleyen nftables güvenlik duvarı derleyicisi ve optimizasyoncusunu, Rocq teorem kanıtlayıcısını kullanarak LLM destekli formal doğrulama ile incelediler. Amaç, optimizasyoncunun kullanıcı tanımlı kuralların anlamını koruduğunu kanıtlamaktı.
Bu çalışma, 2022'den beri her Linux sürümünde bulunan iki hatayı ortaya çıkardı. Birincisi, hatalı bir bit maskesi birleştirme optimizasyonuydu; kısıtlayıcı kuralları sessizce daha izin verici hale getiriyordu — "SYN biti açık olan her paket" kuralını "sadece SYN biti açık olan paketler" haline dönüştürerek istenmeyen trafiğin fark edilmeden geçmesine yol açabiliyordu. İkinci hata ise örtüşen adres aralıklarını yanlış biçimde bir karar tablosunda birleştirerek çekirdek tarafından reddedilen geçersiz kural kümeleri üretiyordu.
Ekibin doğrulanmış yeniden uygulaması her iki sorundan da arınmış olarak kanıtlandı; takip testi ise daha ciddi hatanın basit bir LLM tabanlı hata taramasıyla büyük olasılıkla fark edilmeyeceğini gösterdi — bu da güvenlik duvarları gibi kritik altyapılarda formal kanıtların ad-hoc LLM taramalarına kıyasla sağladığı ek değeri ortaya koyuyor.