CVE-2020-19725

Severity Score

7.8

*CVSS v3.1

Exploit Likelihood

*EPSS

Affected Versions

*CPE

Public Exploits

*Multiple Sources

Exploited in Wild

*KEV

Decision

Attend

*SSVC

Descriptions

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.

Existe una vulnerabilidad use-after-free en el archivo pdd_simplifier.cpp en Z3 antes de la versión 4.8.8. Ocurre cuando el solucionador intenta simplificar las restricciones y provoca un acceso inesperado a la memoria. Puede causar fallos de segmentación o ejecución arbitraria de código.

*Credits: N/A

CVSS Scores

NISTv3.1 7.8

Attack Vector

Local

Attack Complexity

Low

Privileges Required

None

User Interaction

Required

Scope

Unchanged

Confidentiality

High

Integrity

High

Availability

High

* Common Vulnerability Scoring System

SSVC

Decision:Attend

Exploitation

Poc

Automatable

Tech. Impact

Total

* Organization's Worst-case Scenario

Timeline

2020-08-13 CVE Reserved
2023-08-22 CVE Published
2024-09-23 EPSS Updated
2024-10-04 CVE Updated
2024-10-04 First Exploit
---------- Exploited in Wild
---------- KEV Due Date

CWE

CWE-416: Use After Free

CAPEC

References (1)

URL	Tag	Source

URL	Date	SRC
https://github.com/Z3Prover/z3/issues/3363	2024-10-04

URL	Date	SRC

URL	Date	SRC

Affected Vendors, Products, and Versions

Vendor		Product				Version		Other		Status
Vendor	Product	Version	Other	Status	<-- -->	Vendor	Product	Version	Other	Status
Microsoft Search vendor "Microsoft"		Z3 Search vendor "Microsoft" for product "Z3"				< 4.8.8 Search vendor "Microsoft" for product "Z3" and version " < 4.8.8"		-		Affected