PT-2023-11533 · Z3 · Z3

Hadowblad3 · Published 2023-08-22 · Updated 2023-08-25 · CVE-2020-19725

Positive Technologies (AI Summary)

CVSS v3.1

7.8

High

Base vector

AV:L/AC:L/PR:N/UI:R/S:U/C:H/I:H/A:H

Name of the Vulnerable Software and Affected Versions Z3 versions prior to 4.8.8

Description The issue is related to a use-after-free vulnerability in the file pdd simplifier.cpp. It occurs when the solver attempts to simplify constraints, leading to unexpected memory access. This can result in segmentation faults or arbitrary code execution.

Recommendations For versions prior to 4.8.8, update to version 4.8.8 or later to resolve the issue.

Exploit

Fix

Use After Free

Weakness Enumeration

CWE-416

Related Identifiers

AZL-27991

AZL-37067

CVE-2020-19725

Affected Products

Z3

References · 8

• 🔥 https://github.com/Z3Prover/z3/issues/3363 · Exploit
• https://cve.org/CVERecord?id=CVE-2020-19725 · Security Note
• https://osv.dev/vulnerability/AZL-37067 · Vendor Advisory
• https://nvd.nist.gov/vuln/detail/CVE-2020-19725 · Security Note
• https://osv.dev/vulnerability/AZL-27991 · Vendor Advisory
• https://osv.dev/vulnerability/CVE-2020-19725 · Vendor Advisory
• https://ubuntu.com/security/CVE-2020-19725 · Vendor Advisory
• https://osv.dev/vulnerability/UBUNTU-CVE-2020-19725 · Vendor Advisory