Miniz Source Code and Formal Verification

This directory contains the complete source code of the Miniz compression library and formal verification test files.

Verification Tool Requirements

Installing CBMC

CBMC (C Bounded Model Checker) is the primary tool for formal verification.

Clang Static Analyzer

Clang Static Analyzer is a tool for static code analysis that can detect memory safety issues, null pointer dereferences, and other problems.

How to Run Verification

Static Code Analysis (Clang Static Analyzer)

Static analysis can quickly detect potential issues in code, such as memory safety and null pointer dereferences.

Basic Static Analysis

Log file location: Static analysis results are saved in the submission/verification/results/static-analysis/ directory.

# Run from the submission directory
mkdir -p verification/results/static-analysis

# Method 1: Using scan-build (recommended, generates HTML report)
scan-build -o verification/results/static-analysis \
    clang -c miniz.c miniz_tinfl.c miniz_tdef.c miniz_zip.c

# Method 2: Using clang --analyze (simple and fast)
clang --analyze miniz.c miniz_tinfl.c miniz_tdef.c miniz_zip.c

Static Analysis Parameter Description

• scan-build: Frontend tool for Clang static analyzer, used to generate detailed HTML reports
• -o <directory>: Specify output directory, analysis results will be saved in this directory
• clang -c: Compile source files (without linking), static analyzer will perform analysis during compilation
• --analyze: Directly use clang for static analysis (output to terminal)

Types of Issues Detected by Static Analysis

Clang Static Analyzer can detect:

• Null pointer dereference
• Memory leaks
• Array out of bounds
• Uninitialized variable usage
• Dead code
• API usage errors

How to Run Formal Verification (CBMC)

1. Compression/Decompression Roundtrip Verification

Verify the correctness of compression and decompression roundtrip.

Log file location: All log files are saved in the submission/verification/compress_tests/results/ directory.

cd verification/compress_tests
mkdir -p results

# Basic roundtrip verification (mz_compress)
cbmc verify_roundtrip_with_spec.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --trace \
    2>&1 | tee results/cbmc_roundtrip.log

# Compression level verification (mz_compress2)
cbmc verify_compress2_with_spec.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 5 \
    --trace \
    2>&1 | tee results/cbmc_compress2.log

Note: The state space of compression algorithms is large, verification may take a long time.

2. CRC32 Checksum Verification

Verify the correctness of CRC32 checksum calculation.

Log file location: All log files are saved in the submission/verification/crc32_tests/results/ directory.

cd verification/crc32_tests
mkdir -p results

cbmc verify_crc32_with_spec.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 10 \
    --trace \
    2>&1 | tee results/cbmc_crc32.log

3. Adler32 Checksum Verification

Verify the correctness of Adler32 checksum calculation.

Log file location: All log files are saved in the submission/verification/adler32_tests/results/ directory.

cd verification/adler32_tests
mkdir -p results

# Basic verification
cbmc verify_adler32_with_spec.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 20 \
    --trace \
    2>&1 | tee results/cbmc_adler32.log

4. Compression Bound Verification

Verify the correctness of the mz_compressBound function.

Log file location: All log files are saved in the submission/verification/compress_bound_tests/results/ directory.

cd verification/compress_bound_tests
mkdir -p results

cbmc verify_compress_bound_with_spec.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 5 \
    --trace \
    2>&1 | tee results/cbmc_compress_bound.log

5. Error Handling Path Verification

Verify the behavior of the library under various error conditions, including null pointers, insufficient buffers, invalid data, etc.

Running All Error Handling Tests

Log file location: All log files are saved in the submission/verification/error_handling_tests/results/ directory.

cd verification/error_handling_tests
mkdir -p results

# Test 1: Null pointer handling
cbmc test_null_pointers.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 3 \
    --trace \
    2>&1 | tee results/test_null_pointers.log

# Test 2: Insufficient buffer
cbmc test_insufficient_buffer.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 3 \
    --trace \
    2>&1 | tee results/test_insufficient_buffer.log

# Test 3: Invalid input data
cbmc test_invalid_data.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 3 \
    --trace \
    2>&1 | tee results/test_invalid_data.log

# Test 4: Invalid compression level
cbmc test_invalid_levels.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 3 \
    --trace \
    2>&1 | tee results/test_invalid_levels.log

# Test 5: Combined error conditions
cbmc test_combined_errors.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 3 \
    --trace \
    2>&1 | tee results/test_combined_errors.log

CBMC Command Parameter Description

• --function main: Specify the function to verify (usually main)
• --bounds-check: Check array bounds and pointer arithmetic
• --pointer-check: Check pointer validity and dereference safety
• --unwind N: Unroll loops at most N times (larger values mean more thorough verification but slower)
• --trace: Generate counterexample path if verification fails

Verification Result Interpretation

• All verification test log files are saved in the results/ subdirectory of their respective test directories under the submission directory
• Example: submission/verification/error_handling_tests/results/test_null_pointers.log
• If running commands from the submission directory, the relative path is: verification/error_handling_tests/results/test_null_pointers.log
• If log files cannot be found, ensure that the results/ directory has been created before running verification commands

Verification Depth Adjustment

Quick Verification (Recommended for Error Handling Tests)

Use smaller --unwind values (e.g., 3-5):

cd verification/error_handling_tests
mkdir -p results
cbmc test_null_pointers.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 3 \
    --trace \
    2>&1 | tee results/test_null_pointers.log

Deep Verification (For Functional Correctness Tests)

Use larger --unwind values (e.g., 10-20):

cd verification/adler32_tests
mkdir -p results
cbmc verify_adler32_with_spec.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 20 \
    --trace \
    2>&1 | tee results/cbmc_adler32.log

Verification Scope

Static Code Analysis (Clang Static Analyzer)

• Null pointer dereference detection
• Memory leak detection
• Array out of bounds detection
• Uninitialized variable usage detection
• Dead code detection
• API usage error detection

Error Handling Verification (CBMC)

• Null pointer handling
• Insufficient buffer handling
• Invalid input data handling
• Invalid compression level handling
• Combined error conditions

Functional Correctness Verification (CBMC)

• Compression/decompression roundtrip correctness
• Data integrity
• Length consistency
• CRC32 checksum correctness
• Adler32 checksum correctness
• Compression bound calculation correctness

Notes

1. Verification time: Some verifications (especially compression algorithms) may take a long time, please be patient.

2. Memory usage: Deep verification may consume a lot of memory. If you encounter insufficient memory, reduce the --unwind value.

3. Path references: All verification test files use relative paths ../../miniz.c to reference source code. Ensure commands are run from the correct directory.

4. Results directory: Before running verification, ensure that the corresponding results/ directory has been created.

5. Source code completeness: Ensure all source code files (miniz.c, miniz_tdef.c, miniz_tinfl.c, miniz_zip.c) are in the root directory.

Start Examples

The following are complete verification workflow examples (assuming the current directory is submission):

Example 1: Running Static Analysis

# 1. Create results directory
mkdir -p verification/results/static-analysis

# 2. Run static analysis
scan-build -o verification/results/static-analysis \
    clang -c miniz.c miniz_tinfl.c miniz_tdef.c miniz_zip.c

# 3. View results (macOS)
open verification/results/static-analysis/*/index.html

Example 2: Running CBMC Formal Verification

# 1. Enter error handling test directory
cd verification/error_handling_tests
mkdir -p results

# 2. Run null pointer test
cbmc test_null_pointers.c ../../miniz.c \
    --function main \
    --bounds-check \
    --pointer-check \
    --unwind 3 \
    --trace \
    2>&1 | tee results/test_null_pointers.log

# 3. Check results
grep "VERIFICATION" results/test_null_pointers.log

# 4. View log file (log file is saved in submission/verification/error_handling_tests/results/ directory)
cat results/test_null_pointers.log

Source Code File Description

• miniz.h / miniz.c: Main library files, containing zlib-compatible API
• miniz_common.h: Common type definitions and constants
• miniz_tdef.h / miniz_tdef.c: Compressor (deflate) implementation
• miniz_tinfl.h / miniz_tinfl.c: Decompressor (inflate) implementation
• miniz_zip.h / miniz_zip.c: ZIP archive read/write functionality
• miniz_export.h: Export symbol definitions

Team Members

• Yankun Li (yl6022)
• Zhenghang Zhao (zz3410)