Lean, programın doğruluğunu kanıtladı ama içinde hata bulundu

 (kirancodes.me)
1 puan yazan GN⁺ 14 일 전 | 1 yorum | WhatsApp'ta paylaş
  • Biçimsel olarak doğrulanmış bir zlib uygulaması fuzzing'e tabi tutulduğunda, Lean 4 çalışma zamanındaki lean_alloc_sarray içinde bir heap buffer overflow bulundu
  • Yapay zeka fuzzer'ı Claude, AFL++ ve AddressSanitizer gibi araçlarla 100 milyondan fazla test çalıştırıldıktan sonra, 4 crash ve 1 bellek açığı doğrulandı
  • Tespit edilen sorunlar ikiye ayrılıyor: çalışma zamanı taşması ve Archive.lean içindeki Out-of-Memory tabanlı hizmet reddi (DoS)
  • Doğrulanmış sıkıştırma/açma algoritmaları güvenliydi, ancak doğrulanmamış arşiv ayrıştırıcısı ve çalışma zamanı katmanında açıklar vardı
  • Sonuç olarak biçimsel doğrulama güçlü olsa da, Trusted Computing Base (TCB) güvence altına alınmadan tüm sistemin güvenliği garanti edilemiyor

Lean doğrulamasını geçmiş bir programda bulunan hata

  • Lean ile biçimsel olarak doğrulanmış bir zlib uygulaması fuzzing'e tabi tutulduğunda, Lean 4 çalışma zamanında bir heap buffer overflow bulundu
    • Doğrulanmış uygulama kodunda bellek açığı yoktu
    • Ancak Lean çalışma zamanındaki lean_alloc_sarray fonksiyonunda taşma oluşuyor ve bu tüm Lean 4 sürümlerini etkiliyor
  • Yapay zeka tabanlı fuzzer Claude ile AFL++, AddressSanitizer, Valgrind, UBSan gibi araçlar kullanılarak 100 milyondan fazla fuzzing çalışması yapıldı
    • lean-zipin sıkıştırma, açma ve arşiv işleme dahil 6 saldırı yüzeyine karşı 16 paralel fuzzer çalıştırıldı
    • 19 saat içinde 4 crash girdisi ve 1 bellek açığı bulundu
  • İki ana hata doğrulandı
    • Lean çalışma zamanındaki lean_alloc_sarray içinde heap buffer overflow
    • lean-zipin Archive.lean modülünde Out-of-Memory tabanlı hizmet reddi (DoS)
  • Biçimsel doğrulamanın sınırları ortaya çıktı
    • lean-zipin sıkıştırma/açma algoritmaları tamamen doğrulanmış olsa da, arşiv ayrıştırıcısı (Archive.lean) doğrulanmadığı için DoS açığı içeriyor
    • Çalışma zamanı hatası, Trusted Computing Base içindeki bir sorun olduğundan tüm Lean programlarını etkiliyor
  • Sonuç olarak, Lean'in biçimsel doğrulaması uygulama kodunun güvenilirliğini kanıtladı, ancak doğrulama kapsamı dışındaki bileşenlerde hâlâ açıklar bulunuyor
    • Doğrulama yalnızca uygulandığı kapsam içinde güçlüdür ve temel güven katmanının güvenliğinin sağlanması şarttır

Fuzzing deneyine genel bakış

  • Hedef kod tabanı, lean-zipin doğrulanmış zlib uygulamasıydı
    • Tüm theorem ve specification'lar, dokümantasyon ve C FFI binding'leri kaldırılarak yalnızca saf Lean kodu bırakıldı
    • Claude'un kodun doğrulanmış olduğunu fark etmemesi sağlanarak önyargı önlendi

  • Deney ortamı

    • 16 paralel fuzzer; ZIP, gzip, DEFLATE, tar, tar.gz ve compression dahil 6 saldırı yüzeyinde çalıştırıldı
    • AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck ve flawfinder birlikte kullanıldı
    • 48 elle hazırlanmış exploit dosyası dahil toplam 105.823.818 çalıştırma yapıldı, 359 seed dosyası kullanıldı
    • 19 saat içinde 4 crash girdisi ve 1 bellek açığı bulundu

Hata 1: Lean çalışma zamanında heap buffer overflow

  • Açıklı fonksiyon: lean_alloc_sarray
    • Tüm ByteArray, FloatArray gibi skaler dizileri ayıran fonksiyon
    • sizeof(lean_sarray_object) + elem_size * capacity hesabında tamsayı taşması oluşabiliyor

  • Sorunun nedeni

    • capacity, SIZE_MAX değerine yaklaştığında toplama işlemi taşarak küçük bir tampon ayrılıyor
    • Ardından çağıran taraf n bayt okumaya çalışınca heap buffer overflow meydana geliyor

  • Tetiklenme koşulu

    • lean_io_prim_handle_read içinde nbytes çok büyük bir değer olduğunda oluşuyor
    • compressedSize değeri 0xFFFFFFFFFFFFFFFF olan 156 baytlık bir ZIP64 başlığıyla yeniden üretilebiliyor
    • Lean 4'ün tüm sürümlerini etkiliyor; en güncel nightly dahil
    • Yeniden üretim kodu örneği
    def main : IO Unit := do
  IO.FS.writeFile "test.bin" "hello"
  let h ← IO.FS.Handle.mk "test.bin" .read
  let n : USize := (0 : USize) - (1 : USize)
  let _ ← h.read n
    • Bu kod çalıştırıldığında lean_alloc_sarray içinde taşma oluşuyor
    • Düzeltme PR'ı gönderilmiş durumda

Hata 2: lean-zip arşiv ayrıştırıcısında hizmet reddi (DoS)

  • Açıklı fonksiyon: readExact (Archive.lean)
    • ZIP merkezi dizinindeki compressedSize alanını doğrulama yapmadan doğrudan kullanıyor
    • h.read çağrısında anormal derecede büyük bir boyut istenerek aşırı bellek ayırma ve OOM oluşuyor

  • Sorunun yeniden üretimi

    • 156 baytlık bir ZIP dosyası birkaç exabyte büyüklüğünde olduğunu iddia ettiğinde süreç INTERNAL PANIC: out of memory ile sonlanıyor
    • Sistem unzip aracı başlık boyutunu doğruluyor, ancak lean-zip bunu yapmıyor

Biçimsel doğrulamanın gözden kaçırdıkları

  • DoS açığının nedeni

    • Archive.lean modülü doğrulanmamış bir alan
    • Sıkıştırma/açma hattı (ör. DEFLATE, Huffman, CRC32) tamamen doğrulanmış ve sorunsuz
    • Açık, doğrulama uygulanmayan bölümde ortaya çıkıyor

  • Çalışma zamanı taşmasının özü

    • Lean çalışma zamanı Trusted Computing Base (TCB) içinde yer alıyor
    • Tüm Lean ispatları çalışma zamanının doğruluğunu varsayıyor
    • Bu nedenle çalışma zamanı hatası tüm Lean programlarının güvenliğini etkiliyor

Doğrulanmış kodun sağlamlığı

  • 105 milyon çalıştırmanın sonucu

    • Lean'in ürettiği C kodunda heap overflow, use-after-free, stack overflow, UB, dizi sınırı aşımı hiç görülmedi
    • Claude'un değerlendirmesine göre bu kod tabanı “en bellek güvenli kod tabanlarından biri” olarak analiz edildi

  • Lean'in tip sisteminin etkisi

    • dependent types ve well-founded recursion yapısı sayesinde C/C++ tabanlı zlib uygulamalarında sık görülen açıklar (CVE sınıfları) yapısal olarak engelleniyor

  • Sonuç

    • Doğrulanmış kod bölgesi oldukça sağlamdı ve fuzzer'ın hata bulması zordu
    • Ancak doğrulanmamış bölümlerde ve çalışma zamanı katmanında hâlâ açıklar bulunuyor
    • Doğrulama, uygulandığı kapsam ve güven temelinin güvenliğiyle sınırlıdır

Temel ders

  • Biçimsel doğrulama, uygulandığı kod alanı içinde çok güçlü olsa da, doğrulanmamış çevresel bileşenler veya çalışma zamanı katmanı tüm sağlamlığı tehdit edebilir
  • Trusted Computing Base'in güvenliğinin sağlanması zorunludur; doğrulanmış sistemlerde bile “gözcüleri kim gözetleyecek? (Quis custodiet ipsos custodes)” sorusu baki kalır

İlgili bağlantılar

İlgili okumalar

1 yorum

 
GN⁺ 14 일 전
Hacker News yorumları

  • Bu yazının başlığı ve çerçevesi biraz garip geldi
    Aslında yazar, kanıtlanmış kodun içinde hiçbir bug ya da hata bulamadığını açıkça söylüyor
    Bulunan iki bug, ispat kapsamının dışındaydı; biri eksik spesifikasyon, diğeri ise C++ çalışma zamanındaki heap overflow idi
    Lean’in runtime’ında bug bulunduğunu, doğrulamayı yapan kernel’de değil, özellikle vurgulamak isterim
    Lean dokümantasyonu bağlantısı bakılabilir

    • Doğrulanmış bir sistemde buglardan söz ederken tüm binary’yi hesaba katmak gerektiğini düşünüyorum
      Bir buffer overflow yüzünden Bitcoin kaybederseniz, bug’ın runtime’da olması pek teselli etmez
      Ayrıca program çöküyorsa, çoğu kullanıcı bunu bug olarak görür
      Lean’i gerçek production ortamında kullanan da epey kişi vardır
    • Sadece başlığa bakınca Lean kernel’inde bug var sandım ama aslında bulunan sorunlar Lean runtime’ında ve lean-zip’teymiş
      Kernel değilse, bunun ispatın güvenilirliğine büyük bir etkisi yok
    • lean-zip’teki eksik spesifikasyon, doğrulama felsefesi açısından önemli bir sorun
      “Hello world” programını doğruluyor olsanız bile, sadece çıktıyı değil yan etkileri de spesifiye etmeniz gerekir
      Runtime ile kernel arasındaki sınırda bellek bozulması olursa, ispatın güvenilirliği düşebilir
      Sonuçta asıl mesele, “neyin doğrulanması gerektiğini” net tanımlamaktır
    • Bu sitedeki yazı listesine bakınca giderek daha clickbait hale gelmesi eğlenceliydi
      İlgili yazı listesi
    • Lean runtime’daki bir bug’ı lean-zip’in bug’ı diye adlandırmak, JRE’deki bir bug’ı Java uygulamasının bug’ı diye adlandırmaya benziyor
      Yazarın bilerek yanlış anlamaya yönlendirdiği izlenimi veriyor

  • Ben de kanıtlanmış kod ile benzer bir deneyim yaşadım
    Benim durumumda sorun overflow’dan çok spesifikasyon hatası (spec bug) idi
    Spesifikasyon yanlışsa, kod ve ispat kusursuz olsa bile amaçlanan davranıştan farklı çalışır
    Sonuçta doğrulamanın zorluğu, insan niyetini tam olarak ifade edebilmekte yatıyor
    Yapay zekanın doğrulamayı kusursuz biçimde çözeceğine inanmak yanlış bir güven duygusu verebilir

    • Benim de benzer bir deneyimim var
      Lean, TLA+, Z3 gibi araçlarla ispatlanabilir spesifikasyonlar sadeleştirilmiş olur ve çok sayıda varsayım gerektirir
      Yine de bu çok güçlü bir araç
      Karmaşık algoritmalardaki bugları daraltıp spesifikasyon sınırlarını daha net görmeyi sağlıyor
      Yapay zeka sayesinde bu tür ispat işleri çok daha kolaylaştı
    • Aklıma hep gelen soru şu: “Doğrulama sisteminin kendisine nasıl güvenebiliriz?”
      Programı doğrulayan başka bir programın da sonuçta bug’ları olabilir
      Tam bir öz-doğrulamanın imkansız olması, bana Heisenberg’in belirsizlik ilkesini hatırlatıyor
      Sonuçta doğrulama, “ikinci bağımsız bir implementasyon” ile güven düzeyini artırma süreci
    • Kodumdaki bug’lar ikiye ayrılıyor
      (1) amaçlanan davranıştan farklı çalışma
      (2) amaçlandığı gibi çalışsa da amacın yanlış olması
      İspat yardımcıları (1)’i engeller ama (2)’yi engelleyemez
      Yani tasarımın sağlamlığı ispatlanamaz
      seL4 gibi her şeyi doğrulamak ise fazla pahalı ve zaman alıcı
    • Spesifikasyonun kendisini doğrulamanın bir yoluna ihtiyaç olduğunu düşünüyorum
      Biçimsel mantık + adversarial thinking birleştirilerek, programın ne yapması ve ne yapmaması gerektiğini eksiksiz listeleyen bir yaklaşım ideal olurdu

  • Başlık clickbait gibi hissettirdi
    Kanıtlanmış kısımda bug yokken neden böyle yazıldığını anlamadım
    HN’de olgulara dayalı yazılar görmek istiyorum; bu ise zaman kaybıydı

    • Doğrulanmış yazılımda “yalnızca ispatı ihlal eden bug’a bug deriz” demek adil mi?
      “Bug yok” diye tanıtılıyor ama gerçekte bu, “yalnızca spesifikasyonun kusursuz ifade edildiği kapsam içinde” anlamına geliyor
      Mükemmel derecede doğru olsa bile gerçek dünyada ölü halde doğru olabilir — yani teoride doğru ama pratikte bozuk olabilir
    • Başlık teknik olarak doğru olsa da, lean-zip’in doğrulanmamış kodunda oluşan sorunu sanki kanıtlanmış bölümün bug’ıymış gibi sunuyor
    • Sonuçta “kanıtlanmış kısmın kapsamını netleştirin” mesajı ilginç ve yerinde
    • İkinci bug sanki dayanağı olmadan uydurulmuş gibi görünüyor
      Ne kod referansı var ne de gerçek koda bakınca aynı sonuca varılıyor; aksine bir yanlış anlama olduğu anlaşılıyor
    • Sonuçta lean-zip sadece bir Zlib binding’i

  • Bu sorun dağıtık sistem doğrulamasında da sık görülüyor
    İspat yalnızca belirli koşulların içinde, yani çalışma sınırları dahilinde geçerli olur; ilginç başarısızlıklar da bu sınırda ortaya çıkar
    TLA+’da da aynı şekilde, gerçek dünya varsayımların dışına çıkarsa ispat anlamsız hale gelir
    Benim istediğim şey, çalışma sınırlarının makine tarafından açıkça belirtilmesi ve runtime’da bunların izlenmesi

    • Ben de doğrudan CPU’nun donanım bug’ını bulmuştum
      Ama bug’ların çoğu donanımdan değil, insanların dokümantasyonu okumamasından kaynaklanıyor
      Yalnızca biçimsel modelleme bile bug sayısını muazzam ölçüde azaltabilir

  • Bu, tahmin edilebilir şekilde iyi bir haber
    Yani LLM’nin biçimsel doğrulamadan geçen kod üretebildiği anlamına geliyor
    Gelecekte bug’lar giderek donanım katmanına kayacak
    Sonunda donanım spesifikasyonlarının biçimselleştirilmesi gerekecek
    Üreticiler bunu açıklamazsa toplulukla çatışma çıkabilir
    Uzun vadede iki yola ayrılacağız: zafiyetlerin yok oluşu ya da kasıtlı yerleştirme

  • İlk başta yazarın kanıtlanmış kısmı test etmediğini düşündüm
    Ama okudukça, bug’ın ispat kapsamı dışında bulunduğu anlaşılıyor
    Bu yüzden başlık biraz abartılı bir ifade gibi geldi

    • Yazının yazarı bizzat ortaya çıkıyor
      Doğrulanmış bir sistemin bug’ı denecekse hedefin tüm binary olması gerektiğini savunuyor
      Gerçekten de Archive.lean içindeki sıkıştırma başlığı ayrıştırma bölümünde çökme yaratan bir girdi bulduğunu söylüyor

  • Donald Knuth’un ünlü sözü aklıma geldi
    “Yukarıdaki kodda bug olabilir; dikkatli olun. Ben sadece onun doğru olduğunu kanıtladım, çalıştırmadım.” uyarısıydı bu

  • Parser’ın doğrulanmamış olması büyük bir hata gibi görünüyor
    Binary format parsing her zaman riskli bir alandır

  • Asıl nokta, AI ajanının bir fuzzer ile işbirliği yaparak Lean’de heap buffer overflow bulmuş olması
    Bu oldukça büyük bir başarı

    • Bence gerçekten faydalı bir keşif

  • Claude’un “bu, analiz ettiğim kodlar arasında en bellek güvenli codebase’lerden biri” demesi etkileyiciydi
    Ama bu, sanki Claude’un analiz ettiği ilk kodmuş gibi bir şaka gibi geliyor

    • RL ile kapsamlı biçimde eğitilmiş Claude’un ilk kez kod analiz etmiş olması mümkün değil
      Zaten bu kadar iyi olmasının sebebi de bu
    • Belki de Claude, bizim bilmediğimiz bir şeyi gizlice yapıyordur 😄