Search
Find a vulnerability
Search criteria
2 vulnerabilities found for z3 by microsoft
CVE-2020-19725 (GCVE-0-2020-19725)
Vulnerability from nvd – Published: 2023-08-22 00:00 – Updated: 2024-10-04 16:07
VLAI
EPSS
VEX
Summary
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.
Severity
No CVSS data available.
SSVC
Exploitation: poc
Automatable: no
Technical Impact: total
CISA Coordinator · CISA-ADP (v2.0.3)
Decision recorded 2024-10-04 16:06 UTC
CWE
- n/a
Assigner
References
1 reference
{
"containers": {
"adp": [
{
"providerMetadata": {
"dateUpdated": "2024-08-04T14:15:28.571Z",
"orgId": "af854a3a-2127-422b-91ae-364da2661108",
"shortName": "CVE"
},
"references": [
{
"tags": [
"x_transferred"
],
"url": "https://github.com/Z3Prover/z3/issues/3363"
}
],
"title": "CVE Program Container"
},
{
"metrics": [
{
"other": {
"content": {
"id": "CVE-2020-19725",
"options": [
{
"Exploitation": "poc"
},
{
"Automatable": "no"
},
{
"Technical Impact": "total"
}
],
"role": "CISA Coordinator",
"timestamp": "2024-10-04T16:06:49.362140Z",
"version": "2.0.3"
},
"type": "ssvc"
}
}
],
"providerMetadata": {
"dateUpdated": "2024-10-04T16:07:10.602Z",
"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
"shortName": "CISA-ADP"
},
"title": "CISA ADP Vulnrichment"
}
],
"cna": {
"affected": [
{
"product": "n/a",
"vendor": "n/a",
"versions": [
{
"status": "affected",
"version": "n/a"
}
]
}
],
"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."
}
],
"problemTypes": [
{
"descriptions": [
{
"description": "n/a",
"lang": "en",
"type": "text"
}
]
}
],
"providerMetadata": {
"dateUpdated": "2023-08-22T15:44:46.204Z",
"orgId": "8254265b-2729-46b6-b9e3-3dfca2d5bfca",
"shortName": "mitre"
},
"references": [
{
"url": "https://github.com/Z3Prover/z3/issues/3363"
}
]
}
},
"cveMetadata": {
"assignerOrgId": "8254265b-2729-46b6-b9e3-3dfca2d5bfca",
"assignerShortName": "mitre",
"cveId": "CVE-2020-19725",
"datePublished": "2023-08-22T00:00:00.000Z",
"dateReserved": "2020-08-13T00:00:00.000Z",
"dateUpdated": "2024-10-04T16:07:10.602Z",
"state": "PUBLISHED"
},
"dataType": "CVE_RECORD",
"dataVersion": "5.1"
}
CVE-2020-19725 (GCVE-0-2020-19725)
Vulnerability from cvelistv5 – Published: 2023-08-22 00:00 – Updated: 2024-10-04 16:07
VLAI
EPSS
VEX
Summary
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.
Severity
No CVSS data available.
SSVC
Exploitation: poc
Automatable: no
Technical Impact: total
CISA Coordinator · CISA-ADP (v2.0.3)
Decision recorded 2024-10-04 16:06 UTC
CWE
- n/a
Assigner
References
1 reference
{
"containers": {
"adp": [
{
"providerMetadata": {
"dateUpdated": "2024-08-04T14:15:28.571Z",
"orgId": "af854a3a-2127-422b-91ae-364da2661108",
"shortName": "CVE"
},
"references": [
{
"tags": [
"x_transferred"
],
"url": "https://github.com/Z3Prover/z3/issues/3363"
}
],
"title": "CVE Program Container"
},
{
"metrics": [
{
"other": {
"content": {
"id": "CVE-2020-19725",
"options": [
{
"Exploitation": "poc"
},
{
"Automatable": "no"
},
{
"Technical Impact": "total"
}
],
"role": "CISA Coordinator",
"timestamp": "2024-10-04T16:06:49.362140Z",
"version": "2.0.3"
},
"type": "ssvc"
}
}
],
"providerMetadata": {
"dateUpdated": "2024-10-04T16:07:10.602Z",
"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
"shortName": "CISA-ADP"
},
"title": "CISA ADP Vulnrichment"
}
],
"cna": {
"affected": [
{
"product": "n/a",
"vendor": "n/a",
"versions": [
{
"status": "affected",
"version": "n/a"
}
]
}
],
"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."
}
],
"problemTypes": [
{
"descriptions": [
{
"description": "n/a",
"lang": "en",
"type": "text"
}
]
}
],
"providerMetadata": {
"dateUpdated": "2023-08-22T15:44:46.204Z",
"orgId": "8254265b-2729-46b6-b9e3-3dfca2d5bfca",
"shortName": "mitre"
},
"references": [
{
"url": "https://github.com/Z3Prover/z3/issues/3363"
}
]
}
},
"cveMetadata": {
"assignerOrgId": "8254265b-2729-46b6-b9e3-3dfca2d5bfca",
"assignerShortName": "mitre",
"cveId": "CVE-2020-19725",
"datePublished": "2023-08-22T00:00:00.000Z",
"dateReserved": "2020-08-13T00:00:00.000Z",
"dateUpdated": "2024-10-04T16:07:10.602Z",
"state": "PUBLISHED"
},
"dataType": "CVE_RECORD",
"dataVersion": "5.1"
}