CVE-2020-37268 (GCVE-0-2020-37268)
Vulnerability from cvelistv5
Published
2026-08-24 20:08
Modified
2026-08-25 15:10
Severity ?
6.8 (Medium) - CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N
6.3 (Medium) - CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
CWE
Summary
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.
References
Impacted products
Vendor Product Version
rocq-prover rocq Version: 8.11   <
Create a notification for this product.
Show details on NVD website

To clipboard 

{
  "containers": {
    "adp": [
      {
        "metrics": [
          {
            "other": {
              "content": {
                "id": "CVE-2020-37268",
                "options": [
                  {
                    "Exploitation": "poc"
                  },
                  {
                    "Automatable": "no"
                  },
                  {
                    "Technical Impact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-08-25T15:10:38.394659Z",
                "version": "2.0.3"
              },
              "type": "ssvc"
            }
          }
        ],
        "providerMetadata": {
          "dateUpdated": "2026-08-25T15:10:45.964Z",
          "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
          "shortName": "CISA-ADP"
        },
        "references": [
          {
            "tags": [
              "exploit"
            ],
            "url": "https://github.com/rocq-prover/rocq/issues/12155"
          }
        ],
        "title": "CISA ADP Vulnrichment"
      }
    ],
    "cna": {
      "affected": [
        {
          "defaultStatus": "unaffected",
          "packageURL": "pkg:github/rocq-prover/rocq",
          "product": "rocq",
          "repo": "https://github.com/rocq-prover/rocq",
          "vendor": "rocq-prover",
          "versions": [
            {
              "lessThanOrEqual": "9.2.0",
              "status": "affected",
              "version": "8.11",
              "versionType": "custom"
            }
          ]
        }
      ],
      "credits": [
        {
          "lang": "en",
          "type": "finder",
          "value": "Jason Gross"
        },
        {
          "lang": "en",
          "type": "reporter",
          "value": "Jonathan Brossard (MOABI)"
        }
      ],
      "datePublic": "2020-04-22T00:00:00.000Z",
      "descriptions": [
        {
          "lang": "en",
          "value": "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."
        }
      ],
      "metrics": [
        {
          "cvssV4_0": {
            "attackComplexity": "LOW",
            "attackRequirements": "NONE",
            "attackVector": "LOCAL",
            "baseScore": 6.8,
            "baseSeverity": "MEDIUM",
            "privilegesRequired": "NONE",
            "subAvailabilityImpact": "NONE",
            "subConfidentialityImpact": "NONE",
            "subIntegrityImpact": "NONE",
            "userInteraction": "PASSIVE",
            "vectorString": "CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N",
            "version": "4.0",
            "vulnAvailabilityImpact": "NONE",
            "vulnConfidentialityImpact": "NONE",
            "vulnIntegrityImpact": "HIGH"
          },
          "format": "CVSS"
        },
        {
          "cvssV3_1": {
            "attackComplexity": "LOW",
            "attackVector": "LOCAL",
            "availabilityImpact": "NONE",
            "baseScore": 6.3,
            "baseSeverity": "MEDIUM",
            "confidentialityImpact": "NONE",
            "integrityImpact": "HIGH",
            "privilegesRequired": "NONE",
            "scope": "CHANGED",
            "userInteraction": "REQUIRED",
            "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
            "version": "3.1"
          },
          "format": "CVSS"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-778",
              "description": "Insufficient Logging",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-08-24T20:08:28.079Z",
        "orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
        "shortName": "VulnCheck"
      },
      "references": [
        {
          "tags": [
            "product"
          ],
          "url": "https://github.com/rocq-prover/rocq"
        },
        {
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/rocq-prover/rocq/issues/12155"
        },
        {
          "tags": [
            "technical-description"
          ],
          "url": "https://github.com/rocq-prover/rocq/blob/master/dev/doc/critical-bugs.md"
        },
        {
          "tags": [
            "exploit"
          ],
          "url": "https://github.com/endrazine/rocq-cve-poc-12155"
        },
        {
          "name": "VulnCheck Advisory: Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline",
          "tags": [
            "third-party-advisory"
          ],
          "url": "https://www.vulncheck.com/advisories/coq-and-rocq-prover-print-assumptions-omits-unsafe-universe-checking-inlined-through-parameter-inline"
        }
      ],
      "title": "Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline",
      "x_generator": {
        "engine": "vulncheck-endgame"
      }
    }
  },
  "cveMetadata": {
    "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
    "assignerShortName": "VulnCheck",
    "cveId": "CVE-2020-37268",
    "datePublished": "2026-08-24T20:08:28.079Z",
    "dateReserved": "2026-08-19T11:37:41.053Z",
    "dateUpdated": "2026-08-25T15:10:45.964Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2",
  "vulnerability-lookup:meta": {
    "vulnrichment": {
      "containers": "{\"adp\": [{\"title\": \"CISA ADP Vulnrichment\", \"metrics\": [{\"other\": {\"type\": \"ssvc\", \"content\": {\"id\": \"CVE-2020-37268\", \"role\": \"CISA Coordinator\", \"options\": [{\"Exploitation\": \"poc\"}, {\"Automatable\": \"no\"}, {\"Technical Impact\": \"partial\"}], \"version\": \"2.0.3\", \"timestamp\": \"2026-08-25T15:10:38.394659Z\"}}}], \"references\": [{\"url\": \"https://github.com/rocq-prover/rocq/issues/12155\", \"tags\": [\"exploit\"]}], \"providerMetadata\": {\"orgId\": \"134c704f-9b21-4f2e-91b3-4a467353bcc0\", \"shortName\": \"CISA-ADP\", \"dateUpdated\": \"2026-08-25T15:10:19.813Z\"}}], \"cna\": {\"title\": \"Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline\", \"credits\": [{\"lang\": \"en\", \"type\": \"finder\", \"value\": \"Jason Gross\"}, {\"lang\": \"en\", \"type\": \"reporter\", \"value\": \"Jonathan Brossard (MOABI)\"}], \"metrics\": [{\"format\": \"CVSS\", \"cvssV4_0\": {\"version\": \"4.0\", \"baseScore\": 6.8, \"attackVector\": \"LOCAL\", \"baseSeverity\": \"MEDIUM\", \"vectorString\": \"CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N\", \"userInteraction\": \"PASSIVE\", \"attackComplexity\": \"LOW\", \"attackRequirements\": \"NONE\", \"privilegesRequired\": \"NONE\", \"subIntegrityImpact\": \"NONE\", \"vulnIntegrityImpact\": \"HIGH\", \"subAvailabilityImpact\": \"NONE\", \"vulnAvailabilityImpact\": \"NONE\", \"subConfidentialityImpact\": \"NONE\", \"vulnConfidentialityImpact\": \"NONE\"}}, {\"format\": \"CVSS\", \"cvssV3_1\": {\"scope\": \"CHANGED\", \"version\": \"3.1\", \"baseScore\": 6.3, \"attackVector\": \"LOCAL\", \"baseSeverity\": \"MEDIUM\", \"vectorString\": \"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N\", \"integrityImpact\": \"HIGH\", \"userInteraction\": \"REQUIRED\", \"attackComplexity\": \"LOW\", \"availabilityImpact\": \"NONE\", \"privilegesRequired\": \"NONE\", \"confidentialityImpact\": \"NONE\"}}], \"affected\": [{\"repo\": \"https://github.com/rocq-prover/rocq\", \"vendor\": \"rocq-prover\", \"product\": \"rocq\", \"versions\": [{\"status\": \"affected\", \"version\": \"8.11\", \"versionType\": \"custom\", \"lessThanOrEqual\": \"9.2.0\"}], \"packageURL\": \"pkg:github/rocq-prover/rocq\", \"defaultStatus\": \"unaffected\"}], \"datePublic\": \"2020-04-22T00:00:00.000Z\", \"references\": [{\"url\": \"https://github.com/rocq-prover/rocq\", \"tags\": [\"product\"]}, {\"url\": \"https://github.com/rocq-prover/rocq/issues/12155\", \"tags\": [\"issue-tracking\"]}, {\"url\": \"https://github.com/rocq-prover/rocq/blob/master/dev/doc/critical-bugs.md\", \"tags\": [\"technical-description\"]}, {\"url\": \"https://github.com/endrazine/rocq-cve-poc-12155\", \"tags\": [\"exploit\"]}, {\"url\": \"https://www.vulncheck.com/advisories/coq-and-rocq-prover-print-assumptions-omits-unsafe-universe-checking-inlined-through-parameter-inline\", \"name\": \"VulnCheck Advisory: Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline\", \"tags\": [\"third-party-advisory\"]}], \"x_generator\": {\"engine\": \"vulncheck-endgame\"}, \"descriptions\": [{\"lang\": \"en\", \"value\": \"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.\"}], \"problemTypes\": [{\"descriptions\": [{\"lang\": \"en\", \"type\": \"CWE\", \"cweId\": \"CWE-778\", \"description\": \"Insufficient Logging\"}]}], \"providerMetadata\": {\"orgId\": \"83251b91-4cc7-4094-a5c7-464a1b83ea10\", \"shortName\": \"VulnCheck\", \"dateUpdated\": \"2026-08-24T20:08:28.079Z\"}}}",
      "cveMetadata": "{\"cveId\": \"CVE-2020-37268\", \"state\": \"PUBLISHED\", \"dateUpdated\": \"2026-08-25T15:10:45.964Z\", \"dateReserved\": \"2026-08-19T11:37:41.053Z\", \"assignerOrgId\": \"83251b91-4cc7-4094-a5c7-464a1b83ea10\", \"datePublished\": \"2026-08-24T20:08:28.079Z\", \"assignerShortName\": \"VulnCheck\"}",
      "dataType": "CVE_RECORD",
      "dataVersion": "5.2"
    }
  }
}


Log in or create an account to share your comment.




Tags
Taxonomy of the tags.




Sightings

Author Source Type Date

Nomenclature

  • Seen: The vulnerability was mentioned, discussed, or seen somewhere by the user.
  • Confirmed: The vulnerability is confirmed from an analyst perspective.
  • Published Proof of Concept: A public proof of concept is available for this vulnerability.
  • Exploited: This vulnerability was exploited and seen by the user reporting the sighting.
  • Patched: This vulnerability was successfully patched by the user reporting the sighting.
  • Not exploited: This vulnerability was not exploited or seen by the user reporting the sighting.
  • Not confirmed: The user expresses doubt about the veracity of the vulnerability.
  • Not patched: This vulnerability was not successfully patched by the user reporting the sighting.