CVE-2026-72711
Açıklama
Lean 4 çekirdeği, opak bir bildirimin gövdesinin kapalı olup olmadığını kontrol etmemektedir. environment::add_opaque, tanım ve teorem yollarının gerçekleştirdiği check_no_metavar_no_fvar çağrısını atlamaktadır; bu nedenle yerel bağlamda bulunmayan serbest bir değişken içeren değer doğrudan reddedilmez. Bir metaprogram önce çekirdeğin False türünde geçici bir yerel değişken oluşturmasını sağlayıp türünü tür denetleyicinin çıkarım önbelleğine kaydedebilir, ardından aynı tür denetleyici örneğinde bu önbellek girişi kalıcıyken yerel bağlamı geri yükleyebilir ve son olarak değeri artık bağlı olmayan bu değişken olan opak bir bildirim sunabilir. Önbellek araması, yerel bağlama üyeliğini test edecek daldan önce yanıt verdiği için çekirdek, önbelleğe alınmış türü çıkarır ve herhangi bir önermenin takip edebileceği False türünde opak bir sabite izin verir. Bildirim; sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, yabancı kod veya değiştirilmiş bir .olean dosyası olmaksızın, maksimum çekirdek denetiminde standart denetlenmiş yol üzerinden kabul edilir ve sonuç herhangi bir aksiyom taşımaz. Eksik kapatma kontrolünün eklenmesiyle 4.32.2 sürümünde düzeltilmiştir.
Nasıl düzeltilir
- leanprover lean44.32.2 ya da sonraki bir sürüm
Etkilenen ürünler
| Ürün | Etkilenen sürümler | Düzeltildiği sürüm |
|---|---|---|
| leanprover lean4 | v < 4.32.2 | 4.32.2 |
Sürümünüzü kontrol edin
Ürünü seçin ve kullandığınız sürümü yazın; sürümün etkilenen aralıkta olup olmadığını görün.
Attack Surface Management
Alan adlarınıza bağlı varlıkları, bu varlıklarda çalışan teknolojileri ve bilinen zafiyetleri tek listede görün.