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.
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
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 |
25 Aug 2023, 02:46
| Type | Values Removed | Values Added |
|---|---|---|
| CVSS |
v2 : v3 : |
v2 : unknown
v3 : 7.8 |
| First Time |
Microsoft
Microsoft z3 |
|
| References | (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 |
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
- z3
CWE
CWE-416
Use After Free
