CVE-2026-72705

सारांश

Rocq Prover में guard checker एक fixpoint के अपने ही arguments के माध्यम से किए गए recursive calls का पालन नहीं करता। एक fixpoint स्वयं को दूसरे fixpoint के पास higher-order argument के रूप में पास कर सकता है, जो फिर उसे ऐसे मान पर लागू करता है जो structural argument का subterm नहीं है। recursive function को एक साधारण definition के पास पास करना अस्वीकार कर दिया जाता है क्योंकि checker definition को unfold करता है और call को देख लेता है, लेकिन इसे एक fixpoint के पास पास करना स्वीकार कर लिया जाता है क्योंकि fixpoint arguments के माध्यम से higher-order recursive calls को track नहीं किया जाता। यह ऐसे type को स्वीकार कर लेता है जो definitionally रूप से अपने ही negation के बराबर है, इसलिए self-application विशुद्ध रूप से definitional code में False उत्पन्न करता है, बिना tactics, axioms, plugins या unsafe flags के, और Print Assumptions परिणाम को global context के अंतर्गत closed बताता है। Rocq 9.2.0 में इसे ठीक कर दिया गया है।

स्रोत

• rocq-cve-poc-21683PoC

  CVE-2026-72705 — Rocq Guard Checker उच्च-क्रम तर्क के रूप में पारित Fixpoint को स्वीकार करता है