CVE-2026-2644: minisat Buffer Overflow Vulnerability

CVE-2026-2644 Overview

CVE-2026-2644 is an out-of-bounds read vulnerability affecting niklasso minisat, a minimalistic SAT (Boolean Satisfiability) solver library. The vulnerability exists in the Solver::value function within the core/SolverTypes.h library, specifically in the DIMACS File Parser component. When processing specially crafted DIMACS input files containing the variable index value 2147483648 (which represents the maximum 32-bit signed integer boundary), the parser fails to properly validate input boundaries, resulting in an out-of-bounds memory read condition.

Critical Impact

Local attackers with access to the system can exploit this vulnerability by providing malicious DIMACS input files to trigger out-of-bounds memory reads, potentially causing denial of service or information disclosure.

Affected Products

• niklasso minisat versions up to and including 2.2.0
• Applications and systems integrating the minisat library for SAT solving operations
• Research and academic tools utilizing minisat as a SAT solver backend

Discovery Timeline

• 2026-02-18 - CVE-2026-2644 published to NVD
• 2026-02-18 - Last updated in NVD database

Technical Details for CVE-2026-2644

Vulnerability Analysis

This vulnerability is classified under CWE-119 (Improper Restriction of Operations within the Bounds of a Memory Buffer). The core issue resides in insufficient bounds checking when processing variable indices within DIMACS-formatted input files. The DIMACS format is a standard input format for SAT solvers, specifying problem clauses and variables.

When the Solver::value function in core/SolverTypes.h processes an argument with a variable index of 2147483648, it exceeds the expected bounds for signed 32-bit integer representation. This boundary value triggers an integer overflow condition that subsequently leads to an out-of-bounds memory read operation. The vulnerability requires local access to exploit, as the attacker must be able to supply a crafted DIMACS file to the minisat solver.

The project maintainers were notified through GitHub Issue #55 but have not yet responded to the disclosure.

Root Cause

The root cause is improper input validation in the DIMACS file parser when handling variable index parameters. The Solver::value function does not adequately check whether the provided variable index falls within the valid bounds of allocated memory structures. When processing the edge-case value of 2147483648 (0x80000000 in hexadecimal), the parser fails to recognize this as an invalid or overflow-inducing input, leading to memory access outside the intended buffer boundaries.

Attack Vector

The attack requires local access to the target system. An attacker must craft a malicious DIMACS file containing the specific variable index value 2147483648 and supply it to an application using the vulnerable minisat library. When the DIMACS parser processes this input, the out-of-bounds read is triggered.

The exploitation scenario involves creating a DIMACS CNF (Conjunctive Normal Form) file with a clause referencing the boundary variable index value. When minisat's Solver::value function attempts to retrieve the value for this variable index, it reads memory beyond the allocated bounds. This can result in application crashes (denial of service) or potentially expose sensitive memory contents depending on the application context.

For technical details regarding this vulnerability, refer to the GitHub Issue #55 Details and the VulDB Entry #346406.

Detection Methods for CVE-2026-2644

Indicators of Compromise

• Unexpected crashes or segmentation faults when minisat processes DIMACS input files
• Error logs showing memory access violations in core/SolverTypes.h or the Solver::value function
• DIMACS input files containing abnormally large variable index values near the 32-bit integer boundary
• Unusual file submissions containing the specific value 2147483648 as a variable index

Detection Strategies

• Deploy file integrity monitoring on systems utilizing minisat to detect introduction of potentially malicious DIMACS files
• Implement application-level logging to capture parser errors and boundary condition failures in SAT solver operations
• Use memory sanitizers (AddressSanitizer, Valgrind) during development and testing to detect out-of-bounds access attempts
• Monitor for crash dump patterns indicating memory access violations in minisat library components

Monitoring Recommendations

• Enable detailed logging for applications integrating minisat, particularly around file parsing operations
• Set up alerts for repeated application crashes or memory-related error conditions
• Review input files submitted to SAT solver applications for suspicious boundary values
• Implement runtime bounds checking where possible to detect exploitation attempts

How to Mitigate CVE-2026-2644

Immediate Actions Required

• Identify all applications and systems using niklasso minisat versions up to 2.2.0
• Restrict local access to systems running vulnerable minisat deployments to trusted users only
• Implement input validation on DIMACS files before processing, filtering inputs with variable indices exceeding safe bounds
• Consider temporarily disabling automated processing of untrusted DIMACS input files

Patch Information

At the time of publication, the minisat project has not released an official patch for this vulnerability. The project was informed of the issue via GitHub Issue #55 but has not yet responded. Users should monitor the minisat GitHub repository for future security updates and patches.

Workarounds

• Implement pre-processing validation to reject DIMACS files containing variable indices at or near the 32-bit integer boundary (≥ 2147483647)
• Apply manual source code patches to add bounds checking in the Solver::value function within core/SolverTypes.h
• Consider using alternative SAT solver implementations that have addressed similar boundary condition vulnerabilities
• Sandbox minisat execution environments to limit the impact of potential exploitation

# Example: Pre-processing validation to filter dangerous DIMACS files
# Check for boundary values before processing with minisat
grep -E '(^|[[:space:]])2147483648([[:space:]]|$)' input.cnf && echo "Warning: Potentially malicious variable index detected" && exit 1