fuzz: W3-1 — pin the indirect-reservation invariant; harness over-assertion fixed, reproducers committed
The running validate_pair campaign found the first wave-3 crash
(artifact crash-e40d...): the harness invariant 'validate_bytes Ok ⇒
every offset-map leaf's range.end ≤ buffer.len()' is WRONG for
offset-indirect entries. In aligned mode a maxLength reservation
contributes its full window to the layout (menu 2's total is 68), while
the {data_offset, data_length} pair is absolute — the data may live
anywhere in the buffer and the all-zero pair {0,0} over a 64-byte
buffer validates and reads fine. The wave-1 data_access bounds
partition is the real contract; the new invariant exempted the read
side but over-asserted the window. Harness-bug, not engine-bug.
- invariant now splits: non-indirect leaves keep the full window
assertion; offset-indirect leaves assert only the read_ok ⇒ pair
agreement (the pointed-to window sits inside the buffer)
- the exact artifact bytes pinned as a regression test
(validated_buffer_may_be_shorter_than_the_indirect_reservation_window)
and as corpus seed-044; the generator emits the same shape
deterministically (44→45 seeds)
- PairInput fields made pub for out-of-crate triage probes
Verification: corpus replay 30/30 green; clippy -D warnings clean.
This commit is contained in:
1 parent
aef8d9f6ab
commit
9ca9922fd4
3 files changed
+58
-8
No files matched your search
Binary file not shown.
@@ -632,6 +632,14 @@ def validate_pair_seeds():
|
||||
w(pair(menu_lane(4), True, shape("raw"), union(0, 0x33)))
|
||||
w(pair(menu_lane(0), True, shape("raw"), sandwich_packed(b"hi")))
|
||||
|
||||
# W3-1 reproducer (the first wave-3 campaign crash): menu 2,
|
||||
# aligned, padded shape, empty body. The all-zero 64-byte buffer is
|
||||
# SHORTER than the layout's total (the maxLength reservation
|
||||
# contributes 64 at the entry, end 68) while the all-zero indirect
|
||||
# pair {0,0} reads fine — the validated-buffer/entry-window split
|
||||
# the W3-1 invariant pin documents.
|
||||
w(pair(menu_lane(2), True, shape("padded"), b""))
|
||||
|
||||
# Aligned truncation sweep over the fixed-shape menu 7 body.
|
||||
for n in range(1, len(be)):
|
||||
w(pair(menu_lane(7), True, shape("trunc", n), be))
|
||||
|
||||
@@ -126,10 +126,10 @@ pub enum Shape {
|
||||
/// hostile buffer body.
|
||||
#[derive(Debug, Arbitrary)]
|
||||
pub struct PairInput {
|
||||
lane: DocLane,
|
||||
mode: bool,
|
||||
shape: Shape,
|
||||
buffer: Vec<u8>,
|
||||
pub lane: DocLane,
|
||||
pub mode: bool,
|
||||
pub shape: Shape,
|
||||
pub buffer: Vec<u8>,
|
||||
}
|
||||
|
||||
pub fn fuzz_validate_pair(data: &[u8]) {
|
||||
@@ -361,16 +361,37 @@ fn drive_pair(engine: &AlkTypeEngine, doc: &Value, root: &str, buffer: &[u8]) {
|
||||
) {
|
||||
continue;
|
||||
}
|
||||
// W3-1 (pinned contract, not engine behavior to
|
||||
// change): an offset-indirect entry's range is
|
||||
// the pair/reservation window (a declared
|
||||
// maxLength contributes its full size), but the
|
||||
// {data_offset, data_length} pair points
|
||||
// absolutely into the whole buffer — the data
|
||||
// may live anywhere in the buffer and the
|
||||
// buffer may be shorter than the reservation
|
||||
// (the wave-1 data_access bounds partition is
|
||||
// the contract: the pointed-to window sits
|
||||
// inside the buffer, nothing about the
|
||||
// reservation). For every other encoding a
|
||||
// successful read implies range.end ≤ len.
|
||||
let indirect =
|
||||
entry.meta.encoding == alktype::VariableEncoding::OffsetIndirect;
|
||||
if !indirect {
|
||||
assert!(
|
||||
entry.range.end <= buffer.len(),
|
||||
"a validated non-indirect leaf {path} \
|
||||
[{}, {}) sits inside the buffer ({} bytes)",
|
||||
entry.range.start,
|
||||
entry.range.end,
|
||||
buffer.len()
|
||||
);
|
||||
}
|
||||
match engine.read_field(buffer, path) {
|
||||
Ok(_) => {}
|
||||
Err(e) => panic!(
|
||||
"validate_bytes Ok ⇒ read_field({path}) Ok, got {e:?}"
|
||||
),
|
||||
}
|
||||
assert!(
|
||||
entry.range.end <= buffer.len(),
|
||||
"a validated leaf sits inside the buffer"
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -844,4 +865,25 @@ mod corpus_replay {
|
||||
&buffers::sandwich_packed(b"hi"),
|
||||
));
|
||||
}
|
||||
|
||||
/// W3-1's contract pin: an aligned offset-indirect leaf's entry
|
||||
/// window (a maxLength reservation) may exceed the validated
|
||||
/// buffer — the pair is absolute and the data it names must sit in
|
||||
/// the buffer, nothing about the reservation. The exact crashing
|
||||
/// shape: menu 2, aligned, Padded transform, empty body — a 64-byte
|
||||
/// zero buffer whose layout total is 68, validate_bytes Ok, the
|
||||
/// all-zero pair {0,0} reading empty.
|
||||
#[test]
|
||||
fn validated_buffer_may_be_shorter_than_the_indirect_reservation_window() {
|
||||
fuzz_validate_pair(&enc::pair(
|
||||
enc::lane_menu(2),
|
||||
true,
|
||||
enc::shape_field(enc::SHAPE_PADDED),
|
||||
&[],
|
||||
));
|
||||
// And the exact artifact bytes replay through the entry.
|
||||
let crash: [u8; 11] =
|
||||
[0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x00, 0xD3, 0x04];
|
||||
fuzz_validate_pair(&crash);
|
||||
}
|
||||
}
|
||||
Reference in new issue
Block a user