CVE-2020-19725

Published Aug 22, 2023

Last updated a year ago

Overview

Description: There is a use-after-free vulnerability in file pdd_simplifier.cpp in Z3 before 4.8.8. It occurs when the solver attempt to simplify the constraints and causes unexpected memory access. It can cause segmentation faults or arbitrary code execution.
Source: cve@mitre.org
NVD status: Analyzed

Risk scores

CVSS 3.1

Type: Primary
Base score: 7.8
Impact score: 5.9
Exploitability score: 1.8
Vector string: CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H
Severity: HIGH

Weaknesses

nvd@nist.gov: CWE-416

Hype score: Not currently trending

Configurations

[
  {
    "nodes": [
      {
        "negate": false,
        "cpeMatch": [
          {
            "criteria": "cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:*",
            "vulnerable": true,
            "matchCriteriaId": "6D8EF4B1-776B-4405-896B-9C0EC073D347",
            "versionEndExcluding": "4.8.8"
          }
        ],
        "operator": "OR"
      }
    ]
  }
]

References