Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,3 +1,7 @@
.DS_Store
Cargo.lock
target/
fuzz/artifacts/
fuzz/corpus/
fuzz/coverage/
fuzz/target/
3 changes: 3 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
# Changelog

## Unreleased
- added proptest coverage for prefix/suffix invariants and introduced a fuzz target for mutating `Bytes` operations
- extended `verify.sh` to install cargo-fuzz and execute deterministic fuzz runs alongside Kani proofs
- added Kani proofs ensuring `is_subslice` accepts only slices from the original allocation
- add Kani proof checking `Bytes::downcast_to_owner` for matching and mismatched owners
- added Kani verification harnesses for `Bytes::pop_front` and `Bytes::pop_back`
- avoid flushing empty memory maps in `Section::freeze` to prevent macOS errors
Expand Down
1 change: 1 addition & 0 deletions INVENTORY.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
## Desired Functionality
- Add Kani proofs for winnow view helpers.
- Add test covering freezing an empty section to guard against flush errors on macOS.
- Explore how to model `ByteArea` for Kani or fuzzing without depending on OS-backed memory maps.

## Discovered Issues
- None at the moment.
15 changes: 11 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -175,10 +175,17 @@ Run `./scripts/preflight.sh` from the repository root before committing. The
script formats the code and executes all tests using Python 3.12 for the `pyo3`
feature.

Kani proofs are executed separately with `./scripts/verify.sh`, which should be
run on a dedicated system. The script will install the Kani verifier
automatically. Verification can take a long time and isn't needed for quick
development iterations.
Kani proofs and deterministic fuzz smoke tests are executed with
`./scripts/verify.sh`, which should be run on a dedicated system. The script
installs the Kani verifier, `cargo-fuzz`, and the nightly toolchain before
running `cargo kani --workspace --all-features` followed by a bounded
`cargo +nightly fuzz run`. Override the fuzz target or arguments by setting
`FUZZ_TARGET` or `FUZZ_ARGS` in the environment. Verification can take a long
time and isn't needed for quick development iterations.

For exploratory fuzzing use `cargo fuzz run bytes_mut_ops`. The fuzz target
mirrors a simple vector model to ensure helpers like `take_prefix` and
`pop_front` remain consistent when exercised by randomized sequences.

## Glossary

Expand Down
21 changes: 21 additions & 0 deletions fuzz/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
[package]
name = "anybytes-fuzz"
version = "0.0.0"
edition = "2021"
publish = false

[package.metadata]
cargo-fuzz = true

[dependencies]
libfuzzer-sys = "0.4"
anybytes = { path = ".." }

[dev-dependencies]
arbitrary = { version = "1", features = ["derive"] }

[[bin]]
name = "bytes_mut_ops"
path = "fuzz_targets/bytes_mut_ops.rs"
test = false
doc = false
103 changes: 103 additions & 0 deletions fuzz/fuzz_targets/bytes_mut_ops.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,103 @@
#![no_main]

use anybytes::Bytes;
use arbitrary::{Arbitrary, Result as ArbResult, Unstructured};
use libfuzzer_sys::fuzz_target;

#[derive(Debug)]
enum Operation {
TakePrefix(u16),
TakeSuffix(u16),
PopFront,
PopBack,
}

impl<'a> Arbitrary<'a> for Operation {
fn arbitrary(u: &mut Unstructured<'a>) -> ArbResult<Self> {
let tag = u.int_in_range::<u8>(0..=3)?;
let op = match tag {
0 => Operation::TakePrefix(u.arbitrary()?),
1 => Operation::TakeSuffix(u.arbitrary()?),
2 => Operation::PopFront,
_ => Operation::PopBack,
};
Ok(op)
}
}

#[derive(Debug)]
struct FuzzCase {
data: Vec<u8>,
ops: Vec<Operation>,
}

impl<'a> Arbitrary<'a> for FuzzCase {
fn arbitrary(u: &mut Unstructured<'a>) -> ArbResult<Self> {
let len = u.int_in_range::<usize>(0..=64)?;
let mut data = Vec::with_capacity(len);
for _ in 0..len {
data.push(u.arbitrary()?);
}

let ops_len = u.int_in_range::<usize>(0..=64)?;
let mut ops = Vec::with_capacity(ops_len);
for _ in 0..ops_len {
ops.push(u.arbitrary()?);
}

Ok(Self { data, ops })
}
}

fuzz_target!(|case: FuzzCase| {
let mut bytes = Bytes::from(case.data.clone());
let mut model = case.data;

for op in case.ops {
match op {
Operation::TakePrefix(n) => {
let len = n as usize;
let result = bytes.take_prefix(len);
if len <= model.len() {
let expected: Vec<u8> = model.drain(..len).collect();
let prefix = result.expect("prefix should exist");
assert_eq!(prefix.as_ref(), expected.as_slice());
assert_eq!(bytes.as_ref(), model.as_slice());
} else {
assert!(result.is_none());
assert_eq!(bytes.as_ref(), model.as_slice());
}
}
Operation::TakeSuffix(n) => {
let len = n as usize;
let result = bytes.take_suffix(len);
if len <= model.len() {
let split = model.len() - len;
let expected = model.split_off(split);
let suffix = result.expect("suffix should exist");
assert_eq!(suffix.as_ref(), expected.as_slice());
assert_eq!(bytes.as_ref(), model.as_slice());
} else {
assert!(result.is_none());
assert_eq!(bytes.as_ref(), model.as_slice());
}
}
Operation::PopFront => {
let expected = if model.is_empty() {
None
} else {
Some(model.remove(0))
};
let got = bytes.pop_front();
assert_eq!(got, expected);
assert_eq!(bytes.as_ref(), model.as_slice());
}
Operation::PopBack => {
let expected = model.pop();
let got = bytes.pop_back();
assert_eq!(got, expected);
assert_eq!(bytes.as_ref(), model.as_slice());
}
}
}
});
20 changes: 20 additions & 0 deletions scripts/verify.sh
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,26 @@ cargo install rustfmt || true
# Install the Kani verifier as needed; this is also idempotent.
cargo install --locked kani-verifier || true

# Install cargo-fuzz to run libFuzzer targets. This subcommand is optional
# during development so we ignore installation failures here as well.
cargo install cargo-fuzz || true

# Ensure the nightly toolchain is present for cargo-fuzz and required LLVM tools
rustup toolchain install nightly || true
rustup component add llvm-tools-preview --toolchain nightly || true

# Run all Kani proofs in the workspace
cargo kani --workspace --all-features

# Execute fuzz targets with deterministic settings so verification stays
# reproducible. The default run count can be overridden by setting FUZZ_ARGS.
FUZZ_TARGET="${FUZZ_TARGET:-bytes_mut_ops}"
FUZZ_ARG_STRING="${FUZZ_ARGS:-}"
if [[ -n "$FUZZ_ARG_STRING" ]]; then
IFS=' ' read -r -a FUZZ_ARG_ARRAY <<< "$FUZZ_ARG_STRING"
else
FUZZ_ARG_ARRAY=(-seed=1 -runs=50000)
fi

cargo +nightly fuzz run "$FUZZ_TARGET" -- "${FUZZ_ARG_ARRAY[@]}"

39 changes: 39 additions & 0 deletions src/bytes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -718,4 +718,43 @@ mod verification {
};
assert_eq!(returned.as_ref(), data.as_slice());
}

#[kani::proof]
#[kani::unwind(16)]
pub fn check_is_subslice_accepts_ranges() {
let data: Vec<u8> = Vec::bounded_any::<16>();
let bytes = Bytes::from_source(data.clone());

let start: usize = kani::any();
let end: usize = kani::any();
kani::assume(start <= end);
kani::assume(end <= data.len());

let slice = &bytes.as_ref()[start..end];
assert!(is_subslice(bytes.as_ref(), slice));
}

#[kani::proof]
#[kani::unwind(16)]
pub fn check_is_subslice_rejects_disjoint_ranges() {
let data: Vec<u8> = Vec::bounded_any::<16>();
let other: Vec<u8> = Vec::bounded_any::<8>();

let base_len = data.len();
kani::assume(base_len > 0);
let base_ptr = data.as_ptr();

let other_len = other.len();
kani::assume(other_len > 0);
let other_ptr = other.as_ptr();

let base_start = base_ptr as usize;
let base_end = base_start + base_len;
let other_start = other_ptr as usize;
let other_end = other_start + other_len;
kani::assume(other_end <= base_start || other_start >= base_end);

let bytes = Bytes::from_source(data);
assert!(!is_subslice(bytes.as_ref(), other.as_slice()));
}
}
29 changes: 29 additions & 0 deletions src/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,35 @@ proptest! {
prop_assert_eq!(&b[..], &a[..b.len()]);
prop_assert!(b.is_empty() || a.as_ptr() == b.as_ptr());
}

#[test]
fn test_take_prefix_matches_split(data in proptest::collection::vec(any::<u8>(), 0..64)) {
for len in 0..=data.len() {
let mut bytes = Bytes::from(data.clone());
let prefix = bytes.take_prefix(len).expect("prefix within bounds");
prop_assert_eq!(prefix.as_ref(), &data[..len]);
prop_assert_eq!(bytes.as_ref(), &data[len..]);
}

let mut bytes = Bytes::from(data.clone());
prop_assert!(bytes.take_prefix(data.len() + 1).is_none());
prop_assert_eq!(bytes.as_ref(), data.as_slice());
}

#[test]
fn test_take_suffix_matches_split(data in proptest::collection::vec(any::<u8>(), 0..64)) {
for len in 0..=data.len() {
let mut bytes = Bytes::from(data.clone());
let suffix = bytes.take_suffix(len).expect("suffix within bounds");
let split = data.len() - len;
prop_assert_eq!(suffix.as_ref(), &data[split..]);
prop_assert_eq!(bytes.as_ref(), &data[..split]);
}

let mut bytes = Bytes::from(data.clone());
prop_assert!(bytes.take_suffix(data.len() + 1).is_none());
prop_assert_eq!(bytes.as_ref(), data.as_slice());
}
}

#[test]
Expand Down