CVE-2020-37268: Rocq/Coq Print Assumptions omits unsafe universe checking inlined through Parameter Inline (0 = 1 demonstrated)

CVE-2020-37268: Rocq/Coq Print Assumptions omits unsafe universe checking inlined through Parameter Inline (0 = 1 demonstrated) — unfixed since 2020

Reported by oss-security

Summary by Cyber Security News26 Oct 2026, 01:23 CET

About this summary. This is a short excerpt from the description that oss-security published with its article. Cyber Security News did not report or verify the underlying story. Read the original: https://seclists.org/oss-sec/2026/q4/385

Posted by Jonathan Brossard on Oct 25 1. Summary A soundness-audit bypass in the Rocq (formerly Coq) module system allows construction of a proof of False that Print Assumptions reports as closed under the global context — no axioms, no unsafe flags visible. When a module type declares Parameter Inline and functor application inlines the parameter's body, the metadata recording that the original definition was produced under Unset Universe Checking is dropped

Read the full article at oss-security →

Source attribution: headline and facts are from oss-security (seclists.org). Summary method: excerpt of the source description. See our source attribution policy.

Related coverage

Node.js security release pre-alert

Open-source file sync tool rsync 3.5.2 fixes a CPU exhaustion flaw

Ghostunnel: Open-source TLS proxy with mutual authentication

Rails security releases: 8.0.5.2 and 8.1.4.1

Fixed Detectors, Moving Code: How Well Do Static Security Analyzers Hold Up over a Decade of C/C++ Evolution?

When Debate Amplifies Risk: Social-Bias Vulnerabilities in Multi-Agent Safety Deliberation