Stack buffer overflow in decode_packet via unchecked length multiplication
A stripped 2.4 MB ELF binary contained a function that copied
attacker-controlled bytes into a 1024-byte stack buffer using a
length derived from input * 2. No bound check existed
between the multiplication and the memcpy. Aletheia
falsified the bound assumption, produced a witness, and replayed it
to a confirmed crash — without ever running the binary on the
host.
Discovery
While exploring decode_packet at 0x401230, the concolic engine recorded four path constraints. The fourth was treated as the frontier and negated:
0x401234 input_size < 1024 [taken] 0x401240 input_size > 0 [taken] 0x40125c copied_size = input_size * 2 [taken] 0x401270 copied_size < buf_capacity [NEGATED]
Witness
Z3 (QF_ABV) returned SAT in 18 ms with a satisfying assignment. These bytes are the proof:
arg0 = 0xAA 0xBB 0x00 0x00 arg1 = 0x01 size = 0xFFFE
Decompiled
Type recovery from the SSA form named the buffer, recovered the integer width, and surfaced the missing bound check:
void decode_packet(int input_size, char *src) { char buf[1024]; int copied_size = input_size * 2; if (input_size > 0) { memcpy(buf, src, copied_size); // ← sink, no bound check } }
Replay
The witness was injected into the fuzz harness and replayed concretely (not symbolically). The crash matches the predicted violation address:
$ ./harness < witness.bin [harness] reading 7 bytes [harness] decode_packet(input_size=0xFFFE, src=…) [harness] *** stack smashing detected *** Segmentation fault · Aborted (core dumped)
Aletheia stops here with a Witness in hand: a concrete input vector, the violation address, the source location (buffer.c:42 from DWARF), and a CWE classification. The fuzzer accepts the witness as a high-priority corpus seed and resumes coverage.
Recommendation
Bound the copy length explicitly against sizeof(buf) before the memcpy:
if (copied_size >= sizeof(buf)) return -1; memcpy(buf, src, copied_size);
The integer overflow on input_size * 2 also warrants a separate bound on the multiplication itself — Aletheia raised that as a secondary CWE-190 finding (not shown).