Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Testing and Safety Tooling

This guide covers advanced testing and safety tools for General Bots development, including formal verification, undefined behavior detection, and memory safety analysis.

Overview

General Bots prioritizes safety and correctness. While Rust’s type system catches many errors at compile time, additional tooling can detect subtle bugs and verify critical code paths.

Standard Testing

Unit Tests

cargo test

Run tests for a specific package:

cargo test -p botserver
cargo test -p botlib

Integration Tests

cargo test --test integration

Miri - Undefined Behavior Detection

Miri is an interpreter for Rust’s mid-level intermediate representation (MIR) that detects undefined behavior.

When to Use Miri

  • Testing unsafe code blocks
  • Detecting memory leaks in complex data structures
  • Finding data races in concurrent code
  • Validating pointer arithmetic

Running Miri

# Install Miri
rustup +nightly component add miri

# Run tests under Miri
cargo +nightly miri test

# Run specific test
cargo +nightly miri test test_name

# Run with isolation disabled (for FFI)
cargo +nightly miri test -- -Zmiri-disable-isolation

Miri Limitations

  • Slow execution - 10-100x slower than native
  • No FFI - Cannot call C libraries
  • No I/O - Cannot perform actual I/O operations
  • Nightly only - Requires nightly Rust

Miri is valuable for testing:

  • botlib data structures and parsing logic
  • BASIC interpreter core in botserver
  • Custom serialization/deserialization code

Not suitable for:

  • HTTP handlers (requires I/O)
  • Database operations (requires FFI)
  • Full integration tests

Kani - Formal Verification

Kani is a model checker that mathematically proves code properties.

When to Use Kani

  • Verifying critical algorithms
  • Proving absence of panics
  • Checking invariants in state machines
  • Validating security-critical code

Running Kani

# Install Kani
cargo install --locked kani-verifier
kani setup

# Verify a function
cargo kani --function critical_function

# Verify with specific harness
cargo kani --harness verify_limits

Writing Kani Proofs

#![allow(unused)]
fn main() {
#[cfg(kani)]
mod verification {
    use super::*;

    #[kani::proof]
    fn verify_loop_limit_check() {
        let iterations: u32 = kani::any();
        let max: u32 = kani::any();
        
        // Assume valid inputs
        kani::assume(max > 0);
        
        let result = check_loop_limit(iterations, max);
        
        // Prove: if iterations < max, result is Ok
        if iterations < max {
            assert!(result.is_ok());
        }
    }

    #[kani::proof]
    fn verify_rate_limiter_never_panics() {
        let count: u64 = kani::any();
        let limit: u64 = kani::any();
        
        kani::assume(limit > 0);
        
        // This should never panic regardless of inputs
        let _ = count.checked_div(limit);
    }
}
}

Kani Limitations

  • Bounded verification - Cannot verify unbounded loops
  • Slow - Model checking is computationally expensive
  • Limited async support - Async code requires special handling

Kani is valuable for:

  • Verifying botlib::limits enforcement
  • Proving rate limiter correctness
  • Validating authentication logic invariants
  • Checking BASIC parser edge cases

AddressSanitizer (ASan)

AddressSanitizer detects memory errors at runtime.

Running with ASan

# Build and test with AddressSanitizer
RUSTFLAGS="-Z sanitizer=address" cargo +nightly test

# For a specific package
RUSTFLAGS="-Z sanitizer=address" cargo +nightly test -p botserver

What ASan Detects

  • Use-after-free
  • Buffer overflows
  • Stack buffer overflow
  • Global buffer overflow
  • Use after return
  • Memory leaks

ASan Configuration

# Set ASan options
export ASAN_OPTIONS="detect_leaks=1:abort_on_error=1:symbolize=1"

# Run tests
RUSTFLAGS="-Z sanitizer=address" cargo +nightly test

ThreadSanitizer (TSan)

Detects data races in multi-threaded code.

RUSTFLAGS="-Z sanitizer=thread" cargo +nightly test

TSan Considerations

  • Requires --target x86_64-unknown-linux-gnu
  • Incompatible with ASan (run separately)
  • Higher memory overhead

MemorySanitizer (MSan)

Detects uninitialized memory reads.

RUSTFLAGS="-Z sanitizer=memory" cargo +nightly test

MSan Requirements

  • Must compile all dependencies with MSan
  • Most practical for pure Rust code
  • Requires nightly toolchain

Ferrocene - Safety-Critical Rust

Ferrocene is a qualified Rust compiler for safety-critical systems.

When to Consider Ferrocene

Ferrocene is relevant if General Bots is deployed in:

  • Medical devices
  • Automotive systems
  • Aerospace applications
  • Industrial control systems
  • Any context requiring ISO 26262, IEC 61508, or DO-178C compliance

Ferrocene vs Standard Rust

AspectStandard RustFerrocene
QualificationNoneISO 26262, IEC 61508
DocumentationCommunityFormal qualification docs
SupportCommunityCommercial support
CostFreeCommercial license
TraceabilityLimitedFull requirement traceability

Should General Bots Use Ferrocene?

For typical SaaS deployment: No

Ferrocene is overkill for:

  • Web applications
  • Business automation
  • General chatbot deployments

Consider Ferrocene if:

  • Deploying GB in safety-critical environments
  • Customer requires formal certification
  • Regulatory compliance mandates qualified tooling

Alternative: Standard Rust + Testing

For most deployments, comprehensive testing provides sufficient confidence:

# Full test suite
cargo test --all

# With coverage
cargo tarpaulin --out Html

# Fuzzing critical parsers
cargo fuzz run parse_basic_script

Development (Every Commit)

cargo test
cargo clippy -- -D warnings

Pre-Release

# Full test suite
cargo test --all

# Miri for unsafe code
cargo +nightly miri test -p botlib

# AddressSanitizer
RUSTFLAGS="-Z sanitizer=address" cargo +nightly test

# ThreadSanitizer (for concurrent code)
RUSTFLAGS="-Z sanitizer=thread" cargo +nightly test

Critical Code Changes

# Kani for formal verification
cargo kani --function critical_function

# Extended fuzzing
cargo fuzz run target_name -- -max_total_time=3600

CI/CD Integration

Example GitHub Actions workflow:

name: Safety Tests

on:
  push:
    branches: [main]
  pull_request:

jobs:
  miri:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@nightly
        with:
          components: miri
      - run: cargo miri test -p botlib

  sanitizers:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@nightly
      - run: RUSTFLAGS="-Z sanitizer=address" cargo test

  kani:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: model-checking/kani-github-action@v1
      - run: cargo kani --tests

Summary

ToolPurposeWhen to Use
cargo testUnit/integration testsAlways
miriUndefined behaviorUnsafe code changes
kaniFormal verificationCritical algorithms
ASanMemory errorsPre-release, CI
TSanData racesConcurrent code changes
FerroceneSafety certificationRegulated industries only

See Also