CVE-2026-72714
Təsvir
Rocq Prover, yoxlamanı lokal olaraq deaktiv edən modul bağlanarkən universe graph-ın universe checking bayrağının surətini bərpa etmir. Modul daxilindəki Local Unset Universe Checking əməliyyatının yalnız modul bitənə qədər davam etməsi və qlobal bayrağın bərpa edilməsi gözlənilir, lakin universe graph öz surətini saxlayır və o, deaktiv qalır. Nəticədə iki görünüş arasında ziddiyyət yaranır: Test Universe Checking yoxlamanın aktiv olduğunu bildirir, lakin nüvə (kernel) universe ilə uyğun olmayan terminləri qəbul etməyə davam edir. İki universe arasındakı məhdudiyyət artıq tətbiq edilmədiyi üçün Hurkens paradoksu dövrəyə girir və False sübutunu verir ki, bundan istənilən təklif törəyir. Modul bağlandıqdan sonra sübut heç bir aksiom, plagin və ya təhlükəsiz olmayan funksiyalardan istifadə etmir və Print Assumptions onu qlobal kontekstdə bağlı kimi göstərir, buna görə də nə fərziyyə auditi, nə də bayraq sorğusu nüvənin faktiki vəziyyətini əks etdirmir. Həll yolu mövcud deyil.
Necə düzəltmək olar
Mənbələrdə bu zəiflik üçün düzəldilmiş versiya və ya yamaq keçidi yoxdur.
Təsirlənən məhsullar
| Məhsul | Təsirlənən versiyalar | Düzəldildiyi versiya |
|---|---|---|
| rocq-prover rocq | v ≤ 9.2.0 | — |
Versiyanızı yoxlayın
Məhsulu seçin və istifadə etdiyiniz versiyanı yazın; versiyanın təsirlənən aralıqda olub-olmadığını görün.
Attack Surface Management
Domenlərinizə bağlı aktivləri, onlarda işləyən texnologiyaları və məlum zəiflikləri bir siyahıda görün.