CVE-2026-72703

सारांश

Rocq Prover में guard checker एक nested mutual fixpoint के parameter को uniform मानता है, बिना उस fixpoint के विभिन्न bodies के बीच होने वाले calls की जाँच किए। kernel/inductive.ml में find_uniform_parameters केवल self-recursive calls की जाँच करता है, इसलिए जब कोई body स्वयं को call नहीं करता, तो function यह निष्कर्ष निकालता है कि प्रत्येक parameter uniform है। इस प्रकार एक body से दूसरे body तक cross-call के माध्यम से बढ़ने वाला parameter उस subterm specification को बनाए रखता है जो उसे enclosing fixpoint से विरासत में मिली थी, और उस specification द्वारा guarded एक recursive call स्वीकार कर लिया जाता है, भले ही argument structurally smaller न हो। एक non-terminating definition को structurally decreasing के रूप में स्वीकार कर लिया जाता है, जिससे एक ऐसा term प्राप्त होता है जिसका मान उसके स्वयं के successor के बराबर होता है और इस प्रकार False का proof मिलता है, जिससे कोई भी proposition सिद्ध हो सकता है। इस proof के लिए किसी axioms, plugins या unsafe flags की आवश्यकता नहीं होती और Print Assumptions इसे global context के अंतर्गत closed बताता है। यह Coq 8.20 में पेश किया गया और Rocq 9.2.0 में ठीक किया गया।

स्रोत

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — Rocq Guard Checker अनचेक्ड क्रॉस-कॉल्स के माध्यम से नॉन-टर्मिनेटिंग फिक्सपॉइंट स्वीकार करता है