CVE-2020-19725

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.

CVSS v3 7.8 HIGH

7.8^/10

CVSS v3 : HIGH

V3 Legend

Vector :

Exploitability : 1.8 / Impact : 5.9

Attack Vector LOCAL

Attack Complexity LOW

Privileges Required NONE

User Interaction REQUIRED

Confidentiality Impact HIGH

Integrity Impact HIGH

Availability Impact HIGH

Scope UNCHANGED

References

Link	Resource
https://github.com/Z3Prover/z3/issues/3363	Exploit Issue Tracking Patch Third Party Advisory
https://github.com/Z3Prover/z3/issues/3363	Exploit Issue Tracking Patch Third Party Advisory

Configurations

Configuration 1 (hide)

cpe:2.3:a:microsoft:z3:*:*:*:*:*:*:*:*

History

21 Nov 2024, 05:09

Type	Values Removed	Values Added
References	~~() https://github.com/Z3Prover/z3/issues/3363 - Exploit, Issue Tracking, Patch, Third Party Advisory~~	() https://github.com/Z3Prover/z3/issues/3363 - Exploit, Issue Tracking, Patch, Third Party Advisory

25 Aug 2023, 02:46

Type	Values Removed	Values Added
First Time		Microsoft Microsoft z3
References	~~(MISC) https://github.com/Z3Prover/z3/issues/3363 -~~	(MISC) https://github.com/Z3Prover/z3/issues/3363 - Exploit, Issue Tracking, Patch, Third Party Advisory
CPE		cpe:2.3:a:microsoft:z3::::::::
CWE		CWE-416
CVSS	v2 : ~~unknown~~ v3 : ~~unknown~~	v2 : unknown v3 : 7.8

22 Aug 2023, 19:16

Type	Values Removed	Values Added
New CVE

Information

Published : 2023-08-22 19:16

Updated : 2024-11-21 05:09

NVD link : CVE-2020-19725

Mitre link : CVE-2020-19725

CVE.ORG link : CVE-2020-19725

JSON object : View

Products Affected

microsoft

CWE

CWE-416

Use After Free

{"id": "CVE-2020-19725", "metrics": {"cvssMetricV31": [{"type": "Primary", "source": "nvd@nist.gov", "cvssData": {"scope": "UNCHANGED", "version": "3.1", "baseScore": 7.8, "attackVector": "LOCAL", "baseSeverity": "HIGH", "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H", "integrityImpact": "HIGH", "userInteraction": "REQUIRED", "attackComplexity": "LOW", "availabilityImpact": "HIGH", "privilegesRequired": "NONE", "confidentialityImpact": "HIGH"}, "impactScore": 5.9, "exploitabilityScore": 1.8}]}, "published": "2023-08-22T19:16:04.567", "references": [{"url": "https://github.com/Z3Prover/z3/issues/3363", "tags": ["Exploit", "Issue Tracking", "Patch", "Third Party Advisory"], "source": "cve@mitre.org"}, {"url": "https://github.com/Z3Prover/z3/issues/3363", "tags": ["Exploit", "Issue Tracking", "Patch", "Third Party Advisory"], "source": "af854a3a-2127-422b-91ae-364da2661108"}], "vulnStatus": "Modified", "weaknesses": [{"type": "Primary", "source": "nvd@nist.gov", "description": [{"lang": "en", "value": "CWE-416"}]}], "descriptions": [{"lang": "en", "value": "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."}, {"lang": "es", "value": "Existe una vulnerabilidad use-after-free en el archivo pdd_simplifier.cpp en Z3 antes de la versi\u00f3n 4.8.8. Ocurre cuando el solucionador intenta simplificar las restricciones y provoca un acceso inesperado a la memoria. Puede causar fallos de segmentaci\u00f3n o ejecuci\u00f3n arbitraria de c\u00f3digo. "}], "lastModified": "2024-11-21T05:09:22.383", "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"}]}], "sourceIdentifier": "cve@mitre.org"}

7.8 /10