Bug 2523138

Summary:	CVE-2020-37268 rocq: Coq and Rocq Provers: Logical inconsistency bypass via Print Assumptions omission [fedora-all]
Product:	[Fedora] Fedora	Reporter:	Vladimir Vasilev <vvasilev>
Component:	rocq	Assignee:	Jerry James <loganjerry>
Status:	CLOSED ERRATA	QA Contact:
Severity:	medium	Docs Contact:
Priority:	medium
Version:	rawhide	CC:	loganjerry
Target Milestone:	---	Keywords:	Security, SecurityTracking
Target Release:	---
Hardware:	Unspecified
OS:	Unspecified
Whiteboard:	{"flaws": ["e353cd6f-10bb-465a-84b5-7c59def47724"]}
Fixed In Version:	rocq-9.3.0-2.fc45 rocq-9.3.0-1.fc44	Doc Type:	---
Doc Text:		Story Points:	---
Clone Of:		Environment:
Last Closed:	2026-10-06 00:18:04 UTC	Type:	---
Regression:	---	Mount Type:	---
Documentation:	---	CRM:
Verified Versions:		Category:	---
oVirt Team:	---	RHEL 7.3 requirements from Atomic Host:
Cloudforms Team:	---	Target Upstream Version:
Embargoed:
Bug Depends On:
Bug Blocks:	2523098

Description Vladimir Vasilev 2026-08-24 20:51:46 UTC

Disclaimer: Community trackers are created by Red Hat Product Security team on a best effort basis. Package maintainers are required to ascertain if the flaw indeed affects their package, before starting the update process.

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.

Comment 1 Fedora Update System 2026-10-03 21:26:32 UTC

FEDORA-2026-403bcf6fd8 (0install-2.18-16.fc45, alt-ergo-2.4.3-5.fc45, and 207 more) has been submitted as an update to Fedora 45.
https://bodhi.fedoraproject.org/updates/FEDORA-2026-403bcf6fd8

Comment 2 Fedora Update System 2026-10-04 03:07:06 UTC

FEDORA-2026-403bcf6fd8 has been pushed to the Fedora 45 testing repository.
Soon you'll be able to install the update with the following command:
`sudo dnf upgrade --enablerepo=updates-testing --refresh --advisory=FEDORA-2026-403bcf6fd8`
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2026-403bcf6fd8

See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.

Comment 3 Fedora Update System 2026-10-05 22:21:37 UTC

FEDORA-2026-62bbabcf11 (flocq-4.2.2-3.fc44, gappalib-coq-1.11.0-1.fc44, and 4 more) has been submitted as an update to Fedora 44.
https://bodhi.fedoraproject.org/updates/FEDORA-2026-62bbabcf11

Comment 4 Fedora Update System 2026-10-06 00:18:04 UTC

FEDORA-2026-403bcf6fd8 (0install-2.18-16.fc45, alt-ergo-2.4.3-5.fc45, and 207 more) has been pushed to the Fedora 45 stable repository.
If problem still persists, please make note of it in this bug report.

Comment 5 Fedora Update System 2026-10-06 01:57:21 UTC

FEDORA-2026-62bbabcf11 has been pushed to the Fedora 44 testing repository.
Soon you'll be able to install the update with the following command:
`sudo dnf upgrade --enablerepo=updates-testing --refresh --advisory=FEDORA-2026-62bbabcf11`
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2026-62bbabcf11

See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.

Comment 6 Fedora Update System 2026-10-07 01:40:44 UTC

FEDORA-2026-62bbabcf11 (flocq-4.2.2-3.fc44, gappalib-coq-1.11.0-1.fc44, and 4 more) has been pushed to the Fedora 44 stable repository.
If problem still persists, please make note of it in this bug report.