CVE-2024-37795 identifies a vulnerability in CVC5 Solver version 1.1.3, a widely used SMT (Satisfiability Modulo Theories) solver employed in formal verification, automated theorem proving, and symbolic computation. The flaw arises from improper input validation when parsing the SMT-LIB input format, specifically the 'set-logic' command. A crafted input file with specific formatting errors causes the solver to dereference invalid memory, resulting in a segmentation fault and subsequent denial of service. This vulnerability is classified under CWE-125 (Out-of-bounds Read), indicating that the software reads memory outside the intended buffer boundaries. The CVSS v3.1 score of 7.5 (high) reflects the ease of remote exploitation without authentication or user interaction, and the impact is limited to availability disruption without compromising confidentiality or integrity. No patches were available at the time of publication, and no active exploits have been reported. However, the vulnerability poses a risk to environments relying on CVC5 for critical automated reasoning tasks, where service interruptions could delay or halt verification workflows.

The primary impact of CVE-2024-37795 is denial of service, which can disrupt automated reasoning and formal verification processes that depend on CVC5 Solver. Organizations using this solver in software development, hardware verification, or security-critical systems may experience workflow interruptions, delayed testing, or system instability. While the vulnerability does not allow code execution or data leakage, the loss of availability can have cascading effects in environments where continuous verification is essential, such as safety-critical systems, financial services, or aerospace. Attackers could exploit this remotely to cause repeated crashes, potentially leading to resource exhaustion or operational downtime. The lack of authentication and user interaction requirements increases the risk of automated exploitation attempts, especially in exposed network environments or shared infrastructure.

To mitigate CVE-2024-37795, organizations should monitor for and apply official patches or updates from the CVC5 development team as soon as they become available. In the absence of patches, implement strict input validation and sanitization on SMT-LIB files before processing to detect and reject malformed 'set-logic' commands. Running the solver within sandboxed or containerized environments can limit the impact of crashes and prevent broader system instability. Additionally, restrict network access to the solver service to trusted users and systems only, reducing exposure to remote attacks. Incorporate monitoring and alerting for solver crashes or abnormal terminations to enable rapid incident response. Finally, consider fallback mechanisms or redundancy in verification workflows to maintain continuity during solver outages.