Use-after-free vulnerability in Z3's pdd_simplifier.cpp allows for arbitrary code execution

CVE-2020-19725 · HIGH Severity

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

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.

Learn more about our Web Application Penetration Testing UK.