CVE-2026-72714
Açıklama
Rocq Prover, evren denetimini yerel olarak devre dışı bırakan bir modül kapatıldığında evren grafiğinin evren denetim bayrağı kopyasını geri yüklemez. Bir modül içinde yerel Unset Universe Checking'in yalnızca modül bitene kadar sürmesi ve genel bayrağın geri yüklenmesi beklenir, ancak evren grafiği devre dışı bırakılmış halde kalan kendi kopyasını korur. İki görünüm sonra çelişir: Test Universe Checking denetimi etkin olarak bildirirken çekirdek evrenle tutarsız terimleri kabul etmeye devam eder. İki evren arasındaki kısıt artık uygulanmadığından Hurkens' paradoksu geçerli olur ve False kanıtı elde edilir; bundan her önerme çıkar. Kanıt, modül kapandıktan sonra hiçbir aksiyom, eklenti veya güvenli olmayan özellik kullanmaz ve Print Assumptions bunu global bağlam altında kapalı olarak bildirir, dolayısıyla ne varsayım denetimi ne de bayrak sorgusu gerçek çekirdek durumunu yansıtır. Kullanılabilir bir düzeltme yoktur.
Nasıl düzeltilir
Kaynaklarda bu zafiyet için düzeltilmiş sürüm ya da yama bağlantısı yok.
Etkilenen ürünler
| Ürün | Etkilenen sürümler | Düzeltildiği sürüm |
|---|---|---|
| rocq-prover rocq | v ≤ 9.2.0 | — |
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.