Executive Summary

CVE-2026-2644 is a heap-buffer-overflow vulnerability in the MiniSat SAT solver, specifically in the function Solver::value within the DIMACS File Parser component.

The issue arises when MiniSat parses a crafted DIMACS input file containing an excessively large variable index, such as 2147483648 (2^31), which exceeds the maximum signed 32-bit integer limit (2,147,483,647).

This causes an integer overflow that wraps the variable index to a negative number (-2147483648). Since MiniSat stores variable indices as signed 32-bit integers, the negative index is used to access the assigns array, leading to an out-of-bounds read (buffer underflow) on the heap.

This vulnerability is confirmed by AddressSanitizer reports showing a read violation one byte before the allocated heap region, and it can be triggered by running MiniSat with a specially crafted DIMACS file containing the large variable index.

Useful 0 Not Useful 0

Impact Analysis

This vulnerability can cause out-of-bounds heap reads leading to heap buffer underflow, which may result in software crashes or instability.

Because the issue affects software availability, an attacker with local access could exploit this vulnerability to disrupt the normal operation of MiniSat.

The exploit requires local access and is considered easy to perform, with a proof-of-concept publicly available.

Useful 0 Not Useful 0

Compliance Impact

I don't know

Useful 0 Not Useful 0

Detection Guidance

[{'type': 'paragraph', 'content': 'This vulnerability can be detected by running MiniSat with AddressSanitizer (ASAN) enabled and providing a specially crafted DIMACS input file containing an excessively large variable index such as 2147483648. The ASAN tool will report a heap-buffer-overflow during execution, indicating the presence of the vulnerability.'}, {'type': 'paragraph', 'content': 'To detect the issue, you can build MiniSat in Release mode with ASAN enabled and then run it with a crafted DIMACS file containing the large variable index. The ASAN output will show a read violation one byte before the allocated heap region, confirming the vulnerability.'}, {'type': 'paragraph', 'content': 'Example steps to detect the vulnerability:'}, {'type': 'list_item', 'content': 'Build MiniSat with ASAN enabled (e.g., using Clang with -fsanitize=address).'}, {'type': 'list_item', 'content': 'Create a DIMACS file with a line containing the large variable index, e.g., "2147483648 3 -1 0".'}, {'type': 'list_item', 'content': 'Run MiniSat with the crafted DIMACS file as input.'}, {'type': 'list_item', 'content': 'Observe ASAN reports for heap-buffer-overflow errors related to Solver::value function.'}] [1, 3]

Useful 0 Not Useful 0

Mitigation Strategies

Immediate mitigation steps are limited because no official fix or response has been provided by the project maintainers.

It is recommended to restrict local access to the MiniSat software to trusted users only, as the attack requires local execution.

Consider replacing the affected MiniSat version (up to 2.2.0) with an alternative SAT solver that is not vulnerable.

Avoid processing untrusted or crafted DIMACS input files that could trigger the vulnerability.

Useful 0 Not Useful 0