Goal Reached Thanks to every supporter — we hit 100%!

Goal: 1000 CNY · Raised: 1359 CNY

100%
Buy Us a Coffee

CVE-2020-37268— Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline

Quick assessment

Affected
rocq-prover rocq
Exploitation
No confirmed in-the-wild exploitation; assess based on exposure
Recommended action
Check the vendor advisory and references for a fixed version. If immediate upgrade is impossible, restrict exposure and increase monitoring.

Rocq Prover是Rocq Prover组织的一个形式化证明辅助软件。 Rocq Prover 8.11版本至9.2.0版本存在日志信息泄露漏洞，该漏洞源于Print Assumptions未报告通过Parameter Inline内联参数时在禁用宇宙检查下生成的定义，可能导致模块实现利用宇宙不一致证明任意命题并绕过审计。

CVSS 6.3 · Medium EPSS 0.18% · P7

Possible ATT&CK Techniques 1 AI

T1190 · Exploit Public-Facing Application

Affected Version Matrix 1

VendorProduct Version RangeStatus
rocq-prover rocq 8.11≤ 9.2.0 affected
Get alerts for future matching vulnerabilities Log in to subscribe

I. Basic Information for CVE-2020-37268

Vulnerability Information
Have questions about the vulnerability? See if Shenlong's analysis helps!
View Shenlong Deep Dive ↗

Although we use advanced large model technology, its output may still contain inaccurate or outdated information.Shenlong tries to ensure data accuracy, but please verify and judge based on the actual situation.

Vulnerability Title
Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline
Source: CVE Program / CVE List V5
Vulnerability Description
Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built under Unset Universe Checking, so the resulting constant carries no trace of the unsafe operation. A module implementation can therefore prove False using a universe inconsistency, expose it through an inlined parameter, and have Print Assumptions report the dependent proof as closed under the global context. Because Print Assumptions is the in-process audit used to confirm that a development rests on no unexpected assumptions, a dependency built this way passes that audit while proving arbitrary propositions. The standalone checker coqchk does reject the resulting compiled file. The project records this in dev/doc/critical-bugs.md under non-fixed bugs and rates the risk as moderate when coqchk is not used.
Source: CVE Program / CVE List V5
CVSS Information
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
Source: CVE Program / CVE List V5
Vulnerability Type
不充分的日志记录
Source: CVE Program / CVE List V5
Vulnerability Title
Rocq Prover 日志信息泄露漏洞
Source: CNNVD (China National Vulnerability Database)
Vulnerability Description
Rocq Prover是Rocq Prover组织的一个形式化证明辅助软件。 Rocq Prover 8.11版本至9.2.0版本存在日志信息泄露漏洞，该漏洞源于Print Assumptions未报告通过Parameter Inline内联参数时在禁用宇宙检查下生成的定义，可能导致模块实现利用宇宙不一致证明任意命题并绕过审计。
Source: CNNVD (China National Vulnerability Database)
CVSS Information
N/A
Source: CNNVD (China National Vulnerability Database)
Vulnerability Type
N/A
Source: CNNVD (China National Vulnerability Database)

Affected Products

Vendor Product Affected Versions CPE Subscribe
rocq-prover rocq 8.11 ~ 9.2.0 -

II. Public POCs for CVE-2020-37268

# POC Description Source Link Shenlong Link
AI-Generated POC Premium

No public POC found.

Login to generate AI POC

III. Intelligence Information for CVE-2020-37268

请登录查看更多情报信息。

Vendor Advisories for CVE-2020-37268 (1)

Proof of Concept for CVE-2020-37268 (1)

Other References for CVE-2020-37268 (2)

Same Patch Batch · rocq-prover · 2026-08-24 · 5 CVEs total

CVE-2026-72705 6.3 MEDIUM Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
CVE-2026-72714 6.3 MEDIUM Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
CVE-2026-72703 6.3 MEDIUM Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked
CVE-2026-72704 6.3 MEDIUM Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport

IV. Related Vulnerabilities

Same product: rocq
Same vendor: rocq-prover
Same weakness: CWE-778

V. Comments for CVE-2020-37268

No comments yet

Leave a comment