diff --git a/.github/workflows/security.yml b/.github/workflows/security.yml index 0f93405..0443944 100644 --- a/.github/workflows/security.yml +++ b/.github/workflows/security.yml @@ -163,6 +163,9 @@ jobs: # 360min = GitHub's hosted job cap. The inner timeout governs the actual # scheduled (1h) vs dispatched (<=5h, clamped below) duration. timeout-minutes: 360 + permissions: + contents: read + actions: read # list and download the previous run's corpus artifact strategy: fail-fast: false matrix: @@ -209,6 +212,43 @@ jobs: # nightly rustc rejects. Let cargo resolve fresh deps. run: cargo install cargo-fuzz + - name: Find previous fuzz corpus + id: corpus + # Each run resumes from the corpus the previous run uploaded, so coverage + # accumulates instead of restarting cold. An artifact, not the Actions cache: + # cache entries are evicted under size pressure and after 7 days unused, which + # a weekly run cannot outlast. Only this repository's runs on the same ref + # qualify, so a branch or fork run cannot seed this one. + env: + GH_TOKEN: ${{ github.token }} + TARGET: ${{ matrix.target }} + REF_NAME: ${{ github.ref_name }} + REPO_ID: ${{ github.repository_id }} + run: | + # Two steps, so a failed listing fails this step (set -e) instead of + # reading as "no artifact". --paginate walks every page: newer artifacts + # from other branches must not push this ref's corpus off page one. + artifacts=$(gh api --paginate "repos/${GITHUB_REPOSITORY}/actions/artifacts?name=fuzz-corpus-${TARGET}&per_page=100" \ + --jq '.artifacts[]') + run_id=$(jq -rs --arg ref "$REF_NAME" --argjson repo "$REPO_ID" ' + [.[] + | select(.expired | not) + | select(.workflow_run.head_branch == $ref and .workflow_run.head_repository_id == $repo)] + | sort_by(.created_at) | last | .workflow_run.id // empty' <<< "$artifacts") + if [ -z "$run_id" ]; then + echo "::warning::No fuzz-corpus-${TARGET} artifact from ${REF_NAME}; starting from an empty corpus" + fi + echo "run_id=${run_id}" >> "$GITHUB_OUTPUT" + + - name: Restore fuzz corpus + if: steps.corpus.outputs.run_id != '' + uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 + with: + name: fuzz-corpus-${{ matrix.target }} + path: fuzz/corpus/${{ matrix.target }} + run-id: ${{ steps.corpus.outputs.run_id }} + github-token: ${{ github.token }} + - name: Run deep fuzz # Scheduled runs use 1h/target; a manual workflow_dispatch can request a # longer duration (up to the 5h clamp below) via fuzz_seconds. @@ -237,6 +277,16 @@ jobs: # killed by timeout) remains tolerated. timeout "$((FUZZ_SECONDS + 180))" cargo fuzz run ${{ matrix.target }} -- -max_total_time="$FUZZ_SECONDS" || [ $? -eq 124 ] + - name: Save fuzz corpus + # always(): a run that found a crash still grew the corpus. + if: always() + uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 + with: + name: fuzz-corpus-${{ matrix.target }} + path: fuzz/corpus/${{ matrix.target }}/ + retention-days: 90 + if-no-files-found: warn + - name: Upload crash artifacts if: always() uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 diff --git a/SECURITY.md b/SECURITY.md index f183ae5..bb36075 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -112,13 +112,24 @@ isolate's floor for every subsequent request it serves. Deployments on constrained runtimes must bound payload size at the caller. Making these constants environment-aware or configurable is tracked as a follow-up. -**Test coverage.** The unit tests in `src/byte_storage.rs` call `extract` -directly and are the only merge-time enforcement of the bound. The -`compression_bomb` fuzz target (`fuzz/fuzz_targets/compression_bomb.rs`) is a -build-and-smoke check at pull-request time, and its weekly deep run restarts -from an empty corpus. The Kani harnesses never run on pull requests, never -execute `StorageEnvelope::extract`, and cannot detect a wrong predicate. Treat both as -smoke checks, not as verification of the bound. +**Test coverage.** The three checks live in one private function, +`check_decompression_bound`, which `extract` calls before it allocates. At merge +time, the unit tests in `src/byte_storage.rs` and the integration tests in +`tests/byte_storage_tests.rs` enforce the bound: deleting any one of the three +checks fails at least one of them. The `compression_bomb` fuzz target +(`fuzz/fuzz_targets/compression_bomb.rs`) computes one expected result for each +call it makes to `extract` and `retrieve` and requires that exact result. It +builds envelopes at the 512 MiB limits that only one check rejects, so deleting +any one check makes it fail. At pull-request time the target is only built and +smoke-run. Each scheduled or on-demand deep run uploads its corpus as an +artifact kept for 90 days, and the next run on the same branch starts from the +newest one. With no such artifact it warns and starts from an empty corpus. Two +Kani proofs, `verify_decompression_bound_size_caps` and +`verify_decompression_bound_ratio`, check `check_decompression_bound` over every +(compressed length, `original_size`) pair against limits written as literals, so +an inverted comparison or a changed constant fails them. Kani runs on the +schedule and on manual dispatch, not on pull requests. These Kani statements +cover only those two proofs. ### Envelope decode bounds diff --git a/fuzz/Cargo.toml b/fuzz/Cargo.toml index f1bde02..14e11ce 100644 --- a/fuzz/Cargo.toml +++ b/fuzz/Cargo.toml @@ -13,6 +13,7 @@ cargo-fuzz = true libfuzzer-sys = "0.4" arbitrary = { version = "1", features = ["derive"] } rmp-serde = "1" +lz4_flex = "0.12" [dependencies.cachekit-core] path = ".." diff --git a/fuzz/fuzz_targets/compression_bomb.rs b/fuzz/fuzz_targets/compression_bomb.rs index 4125760..dec016e 100644 --- a/fuzz/fuzz_targets/compression_bomb.rs +++ b/fuzz/fuzz_targets/compression_bomb.rs @@ -1,144 +1,238 @@ #![no_main] -use libfuzzer_sys::fuzz_target; -use cachekit_core::byte_storage::{ByteStorage, ByteStorageError, StorageEnvelope}; +//! Decompression-bound oracle for `StorageEnvelope::extract` and +//! `ByteStorage::retrieve`. +//! +//! Every call to `extract` or `retrieve` has exactly one expected result, +//! computed independently of the crate, and must return it. The size classes +//! each build an envelope that only one of the three bound checks rejects, so +//! deleting or weakening any one of them makes this target fail. + use arbitrary::Arbitrary; +use cachekit_core::byte_storage::{ByteStorage, ByteStorageError, StorageEnvelope}; +use libfuzzer_sys::fuzz_target; + +// Pinned as literals, not read from the crate: changing a limit must fail here. +const MAX_COMPRESSED_SIZE: usize = 512 * 1024 * 1024; +const MAX_UNCOMPRESSED_SIZE: usize = 512 * 1024 * 1024; +const MAX_COMPRESSION_RATIO: u64 = 1000; + +/// Smallest compressed length whose 1000:1 allowance exceeds the +/// `original_size` cap, so the cap alone can reject a declared size. +const MIN_LEN_FOR_ORIGINAL_CAP: usize = MAX_UNCOMPRESSED_SIZE / MAX_COMPRESSION_RATIO as usize + 1; #[derive(Arbitrary, Debug)] -struct CompressionBombTestCase { - /// Compressed data size (tiny to create extreme ratios) - compressed_size: u16, // 0-65535 bytes - /// Original size claim (potentially massive for bomb attacks) - original_size: u32, - /// Checksum (xxHash3-64 = 8 bytes) - checksum: [u8; 8], - /// Format string length - format_len: u8, - /// Actual compressed data pattern (for LZ4 valid/invalid inputs) - data_pattern: u8, +enum Case { + /// Arbitrary bytes and declared size: malformed LZ4, small ratios. + Raw { + compressed_data: Vec, + original_size: u32, + checksum: [u8; 8], + format: String, + }, + /// A valid stream from `StorageEnvelope::new`, then its declared size + /// replaced and/or its checksum altered. + Valid { + data: Vec, + declared_size: Option, + checksum_xor: [u8; 8], + }, + /// `compressed_data.len()` over its cap; nothing else rejects it. + CompressedOverCap { extra: u8, original_size: u16 }, + /// `compressed_data.len()` exactly at its cap: `extract` gets past the + /// bound and fails at decompression. + CompressedAtCap { original_size: u16, extra: u8 }, + /// `original_size` in (cap, 1000 × len]; nothing else rejects it. + OriginalOverCap { extra_len: u16, size: u32 }, + /// Both sizes within their caps, ratio over 1000:1. + RatioOver { len: u16, excess: u32 }, } -fuzz_target!(|test_case: CompressionBombTestCase| { - // Attack scenarios: - // 1. Decompression bomb: 1KB compressed -> claims 1GB uncompressed (1000x ratio) - // 2. Size limit bypass: Claims > 512MB output - // 3. LZ4 malformed data: Invalid compressed stream - // 4. Integer overflow: u32::MAX original_size +/// The bound, in `extract`'s check order. +fn expected_bound(compressed_len: usize, original_size: u32) -> Result<(), ByteStorageError> { + if compressed_len > MAX_COMPRESSED_SIZE || original_size as usize > MAX_UNCOMPRESSED_SIZE { + return Err(ByteStorageError::InputTooLarge); + } + if compressed_len == 0 || original_size as u64 > MAX_COMPRESSION_RATIO * compressed_len as u64 { + return Err(ByteStorageError::DecompressionBomb); + } + Ok(()) +} - let storage = ByteStorage::new(Some("fuzz".to_string())); +/// Expected `extract` result for an envelope whose payload is not known. +fn expected_extract(envelope: &StorageEnvelope) -> Result, ByteStorageError> { + expected_bound(envelope.compressed_data.len(), envelope.original_size)?; + let size = envelope.original_size as usize; + let out = lz4_flex::decompress(&envelope.compressed_data, size) + .map_err(|_| ByteStorageError::DecompressionFailed)?; + if cachekit_core::checksum(&out) != envelope.checksum { + return Err(ByteStorageError::ChecksumMismatch); + } + if out.len() != size { + return Err(ByteStorageError::SizeValidationFailed); + } + Ok(out) +} - // Generate compressed data with pattern - let compressed_data = vec![test_case.data_pattern; test_case.compressed_size as usize]; - - // Generate format string - let format = "f".repeat(test_case.format_len as usize); - - // Create potentially malicious envelope - let envelope = StorageEnvelope { - compressed_data: compressed_data.clone(), - checksum: test_case.checksum, - original_size: test_case.original_size, - format: format.clone(), - }; - - // **CRITICAL SECURITY PROPERTIES** (must verify ALL 4): - - // Property 1: Decompression NEVER panics (even on malformed LZ4 data) - let extract_result = envelope.extract(); - - // Property 2: Size limits enforced (512MB max output) - match &extract_result { - Ok(decompressed) => { - assert!( - decompressed.len() <= storage.max_uncompressed_size(), - "Decompression bomb bypassed size limit: {} bytes > {} bytes", - decompressed.len(), - storage.max_uncompressed_size() - ); - } - Err(err) => { - // Expected for malicious inputs - verify error type - if test_case.original_size as usize > storage.max_uncompressed_size() { - assert!( - matches!( - err, - ByteStorageError::InputTooLarge - | ByteStorageError::DecompressionBomb - | ByteStorageError::DecompressionFailed - ), - "Expected size limit error, got: {:?}", - err - ); - } - } +/// Expected `extract` result for a valid stream of `data` whose declared size +/// and checksum were then changed. `lz4_flex::decompress` fails when the +/// declared size is too small and returns only the decoded bytes when it is +/// too large, so the checksum still matches and the size check fires. +fn expected_valid( + data: &[u8], + envelope: &StorageEnvelope, + checksum_altered: bool, +) -> Result, ByteStorageError> { + expected_bound(envelope.compressed_data.len(), envelope.original_size)?; + let declared = envelope.original_size as usize; + if declared < data.len() { + return Err(ByteStorageError::DecompressionFailed); + } + if checksum_altered { + return Err(ByteStorageError::ChecksumMismatch); + } + if declared > data.len() { + return Err(ByteStorageError::SizeValidationFailed); + } + Ok(data.to_vec()) +} + +/// Debug form that prints the variant, not the payload bytes. +fn describe(result: &Result) -> String { + match result { + Ok(_) => "Ok(..)".to_string(), + Err(e) => format!("Err({e:?})"), } +} - // Property 3: Compression ratio limits enforced (1000x max expansion) - if !compressed_data.is_empty() && test_case.original_size > 0 { - let claimed_ratio = test_case.original_size as u64 / compressed_data.len() as u64; +fn assert_extract(envelope: &StorageEnvelope, expected: &Result, ByteStorageError>) { + let extracted = envelope.extract(); + assert!( + extracted == *expected, + "extract: expected {}, got {} (compressed_len={} original_size={})", + describe(expected), + describe(&extracted), + envelope.compressed_data.len(), + envelope.original_size + ); +} - if claimed_ratio > storage.max_compression_ratio() { - // Must reject suspicious ratios (or size limits caught it first) - assert!( - extract_result.is_err(), - "Decompression bomb bypassed ratio limit: {}x expansion", - claimed_ratio - ); +fn assert_retrieve( + storage: &ByteStorage, + envelope_bytes: &[u8], + expected: Result<(Vec, String), ByteStorageError>, +) { + let retrieved = storage.retrieve(envelope_bytes); + assert!( + retrieved == expected, + "retrieve: expected {}, got {} (envelope_len={})", + describe(&expected), + describe(&retrieved), + envelope_bytes.len() + ); +} - if let Err(err) = &extract_result { - // Security checks may fail in different order (size limit or ratio limit) - assert!( - matches!( - err, - ByteStorageError::DecompressionBomb - | ByteStorageError::InputTooLarge - | ByteStorageError::DecompressionFailed - ), - "Expected security violation error, got: {:?}", - err - ); - } - } +/// Both calls on an envelope small enough to serialize cheaply. +fn assert_outcome( + storage: &ByteStorage, + envelope: &StorageEnvelope, + expected: Result, ByteStorageError>, +) { + assert_extract(envelope, &expected); + let bytes = rmp_serde::to_vec(envelope).expect("envelope serializes"); + assert_retrieve( + storage, + &bytes, + expected.map(|data| (data, envelope.format.clone())), + ); +} + +/// `retrieve` on input over its length cap. Zeroed bytes stay lazily mapped, +/// so this costs no page writes, and they do not decode as an envelope: without +/// the length check the result is `DeserializationFailed`, not `InputTooLarge`. +fn assert_retrieve_over_cap(storage: &ByteStorage, extra: u8) { + let bytes = vec![0u8; MAX_COMPRESSED_SIZE + 1 + extra as usize]; + assert_retrieve(storage, &bytes, Err(ByteStorageError::InputTooLarge)); +} + +fn envelope(compressed_data: Vec, original_size: u32) -> StorageEnvelope { + StorageEnvelope { + compressed_data, + checksum: [0u8; 8], + original_size, + format: "fuzz".to_string(), } +} + +fuzz_target!(|case: Case| { + let storage = ByteStorage::new(Some("fuzz".to_string())); - // Property 4: ByteStorage.retrieve() provides additional layer of defense - // (Envelope serialization roundtrip testing) - if let Ok(envelope_bytes) = rmp_serde::to_vec(&envelope) { - // Test retrieve() with fuzzer-generated envelope - let retrieve_result = storage.retrieve(&envelope_bytes); - - match retrieve_result { - Ok((decompressed, _)) => { - // If retrieve succeeded, ALL security checks must have passed - assert!( - decompressed.len() <= storage.max_uncompressed_size(), - "retrieve() bypassed size limit" - ); - - // Ratio must be within limits (for non-empty compressed data) - if !compressed_data.is_empty() { - let actual_ratio = decompressed.len() as u64 / compressed_data.len() as u64; - assert!( - actual_ratio <= storage.max_compression_ratio(), - "retrieve() bypassed ratio limit: {}x", - actual_ratio - ); - } + match case { + Case::Raw { + compressed_data, + original_size, + checksum, + format, + } => { + let envelope = StorageEnvelope { + compressed_data, + checksum, + original_size, + format, + }; + let expected = expected_extract(&envelope); + assert_outcome(&storage, &envelope, expected); + } + Case::Valid { + data, + declared_size, + checksum_xor, + } => { + let mut envelope = + StorageEnvelope::new(&data, "fuzz".to_string()).expect("small input compresses"); + if let Some(size) = declared_size { + envelope.original_size = size; } - Err(_) => { - // Expected for malicious/malformed envelopes - // Error handling is working correctly + for (byte, xor) in envelope.checksum.iter_mut().zip(checksum_xor) { + *byte ^= xor; } + let expected = expected_valid(&data, &envelope, checksum_xor != [0u8; 8]); + assert_outcome(&storage, &envelope, expected); + } + Case::CompressedOverCap { + extra, + original_size, + } => { + let len = MAX_COMPRESSED_SIZE + 1 + extra as usize; + let envelope = envelope(vec![0u8; len], original_size as u32); + assert_extract(&envelope, &Err(ByteStorageError::InputTooLarge)); + assert_retrieve_over_cap(&storage, extra); + } + Case::CompressedAtCap { + original_size, + extra, + } => { + let envelope = envelope(vec![0u8; MAX_COMPRESSED_SIZE], original_size as u32); + assert_extract(&envelope, &expected_extract(&envelope)); + assert_retrieve_over_cap(&storage, extra); + } + Case::OriginalOverCap { extra_len, size } => { + let len = MIN_LEN_FOR_ORIGINAL_CAP + extra_len as usize; + let span = MAX_COMPRESSION_RATIO * len as u64 - MAX_UNCOMPRESSED_SIZE as u64; + let original_size = MAX_UNCOMPRESSED_SIZE as u64 + 1 + size as u64 % span; + let envelope = envelope(vec![0u8; len], original_size as u32); + assert_outcome(&storage, &envelope, Err(ByteStorageError::InputTooLarge)); + } + Case::RatioOver { len, excess } => { + let allowance = MAX_COMPRESSION_RATIO * len as u64; + let span = MAX_UNCOMPRESSED_SIZE as u64 - allowance; + let original_size = allowance + 1 + excess as u64 % span; + let envelope = envelope(vec![0u8; len as usize], original_size as u32); + assert_outcome( + &storage, + &envelope, + Err(ByteStorageError::DecompressionBomb), + ); } } - - // Property 5: No memory exhaustion - // Fuzzer tracks memory usage - excessive allocation will trigger OOM kill - // Defense-in-depth: Size limits prevent 1KB -> 10GB attacks - - // SUCCESS: All compression bomb attack vectors blocked - // - Extreme ratios rejected (1000x limit) - // - Oversized outputs rejected (512MB limit) - // - Malformed LZ4 data handled gracefully - // - No panics, crashes, or memory exhaustion }); diff --git a/src/byte_storage.rs b/src/byte_storage.rs index 974c915..b6b2d7d 100644 --- a/src/byte_storage.rs +++ b/src/byte_storage.rs @@ -105,33 +105,7 @@ impl StorageEnvelope { /// Extract and validate data from envelope #[cfg(all(feature = "compression", feature = "checksum"))] pub fn extract(&self) -> Result, ByteStorageError> { - // Security: Validate envelope structure first - if self.compressed_data.len() > MAX_COMPRESSED_SIZE { - return Err(ByteStorageError::InputTooLarge); - } - - if self.original_size as usize > MAX_UNCOMPRESSED_SIZE { - return Err(ByteStorageError::InputTooLarge); - } - - // Security: Check compression ratio for decompression bomb protection - // Uses integer arithmetic to prevent floating-point precision bypass attacks - let compressed_size = self.compressed_data.len() as u64; - - // Step 1: Zero check - empty compressed data with non-zero original is a bomb - if compressed_size == 0 { - return Err(ByteStorageError::DecompressionBomb); - } - - // Step 2: Checked multiplication - overflow = bomb (fail-safe) - let max_allowed_original = MAX_COMPRESSION_RATIO - .checked_mul(compressed_size) - .ok_or(ByteStorageError::DecompressionBomb)?; - - // Step 3: Compare original_size against computed maximum - if (self.original_size as u64) > max_allowed_original { - return Err(ByteStorageError::DecompressionBomb); - } + check_decompression_bound(self.compressed_data.len(), self.original_size)?; // Decompress (with validated sizes) let decompressed = lz4_flex::decompress(&self.compressed_data, self.original_size as usize) @@ -152,6 +126,46 @@ impl StorageEnvelope { } } +/// Decompression bound, checked by `extract` before it allocates the output. +/// +/// A separate function so the Kani proofs verify the predicate `extract` +/// actually runs, not a restatement of it. +#[cfg(all(feature = "compression", feature = "checksum"))] +fn check_decompression_bound( + compressed_len: usize, + original_size: u32, +) -> Result<(), ByteStorageError> { + // Size caps first + if compressed_len > MAX_COMPRESSED_SIZE { + return Err(ByteStorageError::InputTooLarge); + } + + if original_size as usize > MAX_UNCOMPRESSED_SIZE { + return Err(ByteStorageError::InputTooLarge); + } + + // Security: Check compression ratio for decompression bomb protection + // Uses integer arithmetic to prevent floating-point precision bypass attacks + let compressed_size = compressed_len as u64; + + // Step 1: Zero-length compressed data is always a bomb + if compressed_size == 0 { + return Err(ByteStorageError::DecompressionBomb); + } + + // Step 2: Checked multiplication - overflow = bomb (fail-safe) + let max_allowed_original = MAX_COMPRESSION_RATIO + .checked_mul(compressed_size) + .ok_or(ByteStorageError::DecompressionBomb)?; + + // Step 3: Compare original_size against computed maximum + if (original_size as u64) > max_allowed_original { + return Err(ByteStorageError::DecompressionBomb); + } + + Ok(()) +} + /// Raw byte storage engine (pure Rust core) /// Simple store/retrieve interface with no type awareness pub struct ByteStorage { @@ -560,6 +574,21 @@ mod tests { ); } + #[test] + fn test_extract_rejects_oversized_compressed_data() { + // WHY: only the compressed-length cap rejects this envelope. original_size + // is under its cap and the ratio is far below 1000:1, and retrieve's + // envelope-length check is bypassed by calling extract directly. + let envelope = StorageEnvelope { + compressed_data: vec![0u8; MAX_COMPRESSED_SIZE + 1], + checksum: [0u8; 8], + original_size: 1, + format: "test".to_string(), + }; + + assert_eq!(envelope.extract(), Err(ByteStorageError::InputTooLarge)); + } + #[test] fn test_envelope_size_validation() { let storage = ByteStorage::new(None); @@ -678,100 +707,49 @@ mod kani_proofs { assert_ne!(checksum_a, checksum_b); } - /// Verify decompression bomb protection (compression ratio limits) - /// Property: Malicious compression ratios exceeding 1000x are always rejected - /// Uses integer arithmetic to match production implementation - #[kani::proof] - #[kani::unwind(3)] - fn verify_decompression_bomb_protection() { - // Symbolic envelope parameters - let compressed_size: u64 = kani::any(); - let original_size: u64 = kani::any(); - - // Constrain to reasonable test ranges - kani::assume(compressed_size > 0 && compressed_size <= 1000); - kani::assume(original_size > 0); - - // Simulate the 3-step check from StorageEnvelope::extract() - // Step 1: Zero check already covered by assume - // Step 2: Checked multiplication - let max_allowed = MAX_COMPRESSION_RATIO.checked_mul(compressed_size); - - // Property: If original_size exceeds max_allowed, extraction must fail - if let Some(max) = max_allowed { - let would_reject = original_size > max; - let exceeds_ratio = original_size > MAX_COMPRESSION_RATIO * compressed_size; - assert_eq!(would_reject, exceeds_ratio); - } else { - // Overflow case: always reject (fail-safe) - assert!(true); // Overflow is always rejected - } - } - - /// Verify size limit enforcement on input - /// Property: Inputs exceeding MAX_UNCOMPRESSED_SIZE are always rejected - #[kani::proof] - #[kani::unwind(3)] - fn verify_input_size_limits() { - let size: usize = kani::any(); - - // Test boundary conditions around the limit - kani::assume(size <= MAX_UNCOMPRESSED_SIZE + 100); - - // Property: Size check logic is correct - let exceeds_limit = size > MAX_UNCOMPRESSED_SIZE; - let should_reject = size > MAX_UNCOMPRESSED_SIZE; + // The size/ratio proofs pin the limits as literals instead of reading the + // constants, so changing a constant or inverting a comparison in + // `check_decompression_bound` fails a proof. + const PINNED_MAX_COMPRESSED: u64 = 512 * 1024 * 1024; + const PINNED_MAX_UNCOMPRESSED: u64 = 512 * 1024 * 1024; + const PINNED_MAX_RATIO: u64 = 1000; - assert_eq!(exceeds_limit, should_reject); - } - - /// Verify size limit enforcement on compressed data - /// Property: Compressed data exceeding MAX_COMPRESSED_SIZE is rejected + /// Verify the size caps of the decompression bound + /// Property: `InputTooLarge` exactly when either size exceeds 512 MiB, for + /// every (compressed length, original_size) pair #[kani::proof] - #[kani::unwind(3)] - fn verify_compressed_size_limits() { - let compressed_size: usize = kani::any(); - - // Test boundary conditions - kani::assume(compressed_size <= MAX_COMPRESSED_SIZE + 100); + fn verify_decompression_bound_size_caps() { + let compressed_len: usize = kani::any(); + let original_size: u32 = kani::any(); - // Property: Size check logic is correct - let exceeds_limit = compressed_size > MAX_COMPRESSED_SIZE; - let should_reject = compressed_size > MAX_COMPRESSED_SIZE; + let over_cap = compressed_len as u64 > PINNED_MAX_COMPRESSED + || original_size as u64 > PINNED_MAX_UNCOMPRESSED; + let result = check_decompression_bound(compressed_len, original_size); - assert_eq!(exceeds_limit, should_reject); + assert_eq!( + over_cap, + matches!(result, Err(ByteStorageError::InputTooLarge)) + ); } - /// Verify compression ratio calculation is safe (integer arithmetic) - /// Property: Ratio check never panics and correctly identifies bombs + /// Verify the ratio limit of the decompression bound + /// Property: with both sizes within their caps, `DecompressionBomb` exactly + /// when the compressed length is zero or the ratio exceeds 1000:1, else Ok #[kani::proof] - #[kani::unwind(3)] - fn verify_compression_ratio_calculation_safety() { - let original_size: u64 = kani::any(); - let compressed_size: u64 = kani::any(); - - // Constrain to prevent division by zero and keep ranges manageable - kani::assume(compressed_size > 0); - kani::assume(compressed_size <= 10000); - kani::assume(original_size <= 100_000_000); // 100MB max for test - - // Property 1: checked_mul never panics (it returns None on overflow) - let result = MAX_COMPRESSION_RATIO.checked_mul(compressed_size); - - // Property 2: If multiplication succeeds, comparison is valid - if let Some(max_allowed) = result { - // The check `original_size > max_allowed` is always safe - let is_bomb = original_size > max_allowed; - - // Verify equivalence: is_bomb == (original_size > 1000 * compressed_size) - // This holds when no overflow occurred - if original_size <= max_allowed { - assert!(!is_bomb); - } else { - assert!(is_bomb); - } + fn verify_decompression_bound_ratio() { + let compressed_len: usize = kani::any(); + let original_size: u32 = kani::any(); + kani::assume(compressed_len as u64 <= PINNED_MAX_COMPRESSED); + kani::assume(original_size as u64 <= PINNED_MAX_UNCOMPRESSED); + + let is_bomb = + compressed_len == 0 || original_size as u64 > PINNED_MAX_RATIO * compressed_len as u64; + let result = check_decompression_bound(compressed_len, original_size); + + if is_bomb { + assert!(matches!(result, Err(ByteStorageError::DecompressionBomb))); + } else { + assert!(result.is_ok()); } - - // Property 3: Zero compressed_size is handled by separate check (not tested here) } }