Testing + Formal Methods

Overview

The boundary between testing and formal methods is increasingly blurred. Modern approaches combine the efficiency and practicality of testing with the rigor of formal specifications, producing hybrid techniques that offer the best of both worlds. This chapter covers fuzzing with formal methods, differential testing, metamorphic testing, property-based testing, QuickCheck, grammar-based fuzzing, coverage-guided fuzzing, symbolic fuzzing, kernel fuzzing with syzkaller, and how these techniques leverage formal specifications to find bugs that conventional testing misses.

The Testing Spectrum: From Random to Formal

graph LR
    RANDOM["Random Testing"] --> FUZZ["Fuzzing"]
    FUZZ --> CGF["Coverage-Guided<br/>Fuzzing"]
    CGF --> SYMFUZZ["Symbolic<br/>Fuzzing"]
    SYMFUZZ --> PBT["Property-Based<br/>Testing"]
    PBT --> DIFF["Differential<br/>Testing"]
    DIFF --> FORMAL["Full Formal<br/>Verification"]
    style RANDOM fill:#ffcdd2
    style FORMAL fill:#c8e6c9

Coverage-Guided Fuzzing

Core Mechanism

Coverage-guided fuzzing (CGF) is the dominant fuzzing technique in industry. It instruments the target program to track code coverage, then uses evolutionary algorithms to generate inputs that maximize coverage. Inputs that discover new code paths are prioritized for mutation and further exploration.

flowchart TD
    SEED["Seed Inputs"] --> MUTATE[Generate Mutant Input]
    MUTATE --> EXEC["Execute Target"]
    EXEC -->|New Coverage?| FEEDBACK[Update Corpus]
    EXEC -->|Crash?| REPORT[Report Bug]
    EXEC -->|No new coverage| MUTATE
    FEEDBACK --> MUTATE

Mutation Strategies

Instrumentation

Coverage-guided fuzzers track coverage using SanitizerCoverage (Sancov), which provides several coverage modes:

Major Tools

LibFuzzer Example

// target.cc
#include <stdint.h>
#include <stddef.h>

extern "C" int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
    if (size < 4) return 0;  // too short

    int32_t magic = *(int32_t *)data;
    if (magic == 0xDEADBEEF) {
        // Bug: buffer underflow when magic value matches
        if (size >= 100) {
            char buf[10];
            memcpy(buf, data + 90, 10);  // potential OOB if size < 100
        }
    }
    return 0;
}

// Build: clang++ -fsanitize=fuzzer,address target.cc -o fuzzer
// Run:   ./fuzzer -max_len=1024 -timeout=10

Symbolic Fuzzing

Combining Fuzzing with Symbolic Execution

Symbolic fuzzing (also called hybrid fuzzing or smart fuzzing) combines the speed of coverage-guided fuzzing with the analytical power of symbolic execution. When the fuzzer gets stuck (unable to discover new coverage through mutation), it invokes a symbolic execution engine to solve for inputs that would take uncovered branches.

flowchart TD
    FUZZER[Coverage-Guided Fuzzer] -->|Stuck?| SYMEXEC[Symbolic Execution]
    SYMEXEC --> SOLVE[SMT Solver]
    SOLVE --> NEW_INPUT[New Directed Input]
    NEW_INPUT --> FUZZER

Tools

Grammar-Based Fuzzing

Motivation

Many input formats have complex syntactic structure (JSON, XML, SQL, programming languages). Blind byte-level mutation (as in AFL/LibFuzzer) is inefficient for these formats because most random mutations produce syntactically invalid inputs that are rejected by the parser before reaching interesting code.

Grammar-based fuzzing uses a context-free grammar to generate syntactically valid inputs, focusing mutations on semantic content rather than syntactic structure.

Grammar-Guided Generation

<!-- Grammar for a simple HTTP request -->
request     ::= method SP uri SP version CRLF headers CRLF body
method      ::= "GET" | "POST" | "PUT" | "DELETE"
uri         ::= "/" path
path        ::= segment ("/" segment)*
segment     ::= alpha (alpha | digit)*
headers     ::= header (CRLF header)* CRLF
header      ::= name ":" SP value
body        ::= string | empty

Instead of randomly mutating bytes, the fuzzer mutuates the grammar’s non-terminals — generating diverse but syntactically valid requests that explore the parser and request handler logic.

Tools

Property-Based Testing

Concept

Property-based testing (PBT) specifies the expected behavior of a function as properties that should hold for all valid inputs, rather than testing specific input-output pairs. The testing framework automatically generates random inputs and checks the properties. When a property fails, the framework automatically shrinks the failing input to a minimal counterexample.

flowchart TD
    SPEC["Property: forall x ∈ S, P(x) holds"]
    SPEC --> GEN[Generate Random Input x]
    GEN --> EXEC["Execute Function f(x)"]
    EXEC --> CHECK{"P(f(x))?"}
    CHECK -->|Yes| GEN
    CHECK -->|No| SHRINK[Shrink Input to Minimal]
    SHRINK --> REPORT[Report Failing Test Case]

PBT vs Unit Testing

QuickCheck (Haskell)

QuickCheck, developed by Koen Claessen and John Hughes (1999), is the original property-based testing framework. It is built on the idea of defining testable properties and automatically generating random inputs.

import Test.QuickCheck

-- Property: reverse is involutive
prop_reverse_involution :: [Int] -> Bool
prop_reverse_involution xs = reverse (reverse xs) == xs

-- Property: sort is idempotent
prop_sort_idempotent :: [Int] -> Bool
prop_sort_idempotent xs = sort (sort xs) == sort xs

-- Property: length of reverse equals length of original
prop_reverse_length :: [Int] -> Bool
prop_reverse_length xs = length (reverse xs) == length xs

-- Property: map distributes over composition
prop_map_compose :: (Int -> Int) -> (Int -> Int) -> [Int] -> Bool
prop_map_compose f g xs = map (f . g) xs == map f (map g xs)

-- Run: quickCheck prop_reverse_involution
-- If it fails, QuickCheck shrinks the failing input automatically

QuickCheck in Other Languages

Hypothesis (Python) Example

from hypothesis import given, strategies as st, assume

# Property: sorted list contains same elements as original
@given(st.lists(st.integers()))
def test_sort_preserves_elements(lst):
    assert sorted(lst) == sorted(lst)  # trivial; better:
    assert multiset(sorted(lst)) == multiset(lst)

# Property: string round-trip through JSON
@given(st.dictionaries(
    keys=st.text(min_size=1),
    values=st.integers()
))
def test_json_roundtrip(data):
    import json
    serialized = json.dumps(data)
    deserialized = json.loads(serialized)
    assert deserialized == data

# Property: BST invariant after insertions
@given(st.lists(st.integers()))
def test_bst_invariant(values):
    bst = BST()
    for v in values:
        bst.insert(v)
    # Verify BST property: left < root < right for all nodes
    assert bst.is_valid_bst()

Common Property Patterns

Differential Testing

Concept

Differential testing finds bugs by comparing the outputs of two or more implementations of the same specification. If the outputs differ for the same input, at least one implementation has a bug. This technique is powerful because it requires no formal specification — the reference implementation itself serves as the oracle.

flowchart TD
    INPUT[Random Input X] --> IMP_A[Implementation A]
    INPUT --> IMP_B[Implementation B]
    IMP_A --> OUTPUT_A[Output A]
    IMP_B --> OUTPUT_B[Output B]
    OUTPUT_A --> COMPARE{A == B?}
    OUTPUT_B --> COMPARE
    COMPARE -->|No| BUG[Bug Found]
    COMPARE -->|Yes| NEXT[Generate Next Input]

Famous Applications

SQLite’s differential testing infrastructure (led by Richard Hipp) uses 600+ million generated SQL queries to compare SQLite against PostgreSQL, MySQL, and Oracle. This has found dozens of bugs over the years.

Metamorphic Testing

Concept

Metamorphic testing (MT) is used when the oracle problem makes it hard to determine the correct output for a given input. Instead of checking f(x) == expected, MT checks that a metamorphic relation holds between the outputs of related inputs.

Metamorphic relation: if x₁ → y₁ and x₂ = transform(x₁), then y₂ = transform(y₁)

This is especially useful for:

• Machine learning (no deterministic “correct” output)
• Scientific computing (numerical precision issues)
• Search engines (no single “correct” ranking)
• Compilers (optimizations should preserve semantics)

Common Metamorphic Relations

Example: Testing a Search Function

# Metamorphic relation: adding a document to a corpus
# should not change results for queries that don't match the new doc

def test_search_add_document():
    query = "quantum computing"
    results_before = search(corpus, query)
    corpus.add_document("A recipe for chocolate cake")
    results_after = search(corpus, query)
    # The irrelevant document should not affect results
    assert set(results_before) == set(results_after)

Kernel Fuzzing: Syzkaller

Overview

syzkaller is Google’s unsupervised coverage-guided kernel fuzzer. It generates system calls that exercise the Linux kernel, finding crashes, memory corruptions, and security vulnerabilities. Since its introduction, syzkaller has found hundreds of bugs in the Linux kernel, Android, and other OS kernels.

Architecture

flowchart TD
    subgraph "Host Machine"
        MANAGER[syz-manager] --> COV[syz-fuzzer<br/>Coverage Feedback]
        MANAGER --> PR[syz-prog2<br/>Syzlang Compiler]
        COV --> VM1[VM 1: syz-executor]
        COV --> VM2[VM 2: syz-executor]
        COV --> VMN[VM N: syz-executor]
        PR --> DESCR["System Call Descriptions<br/>(syzlang)"]
    end

syzlang: Describing System Calls

// syzlang description for socket operations
resource sock[int32]

socket$inet_tcp(domain const[AF_INET], type const[SOCK_STREAM], proto const[IPPROTO_TCP]) sock
bind$inet(fd sock, addr ptr[in, sockaddr_in], addrlen const[32]) int32
listen(fd sock, backlog int16) int32
accept4(fd sock, addr ptr[out, sockaddr_in], addrlen ptr[inout, int32], flags const[0]) sock

connect$inet(fd sock, addr ptr[in, sockaddr_in], addrlen const[32]) int32
send(fd sock, buf ptr[in, array[int8, 1000]], len int32[0:1000], flags const[0]) int32

Why Kernel Fuzzing is Different

Syzkaller Achievements

syzkaller has discovered:

• Hundreds of Linux kernel vulnerabilities (CVEs)
• Bugs in Android kernel ( Binder, ION, filesystem drivers)
• Bugs in network drivers (eBPF, TCP/IP stack)
• Bugs in filesystems (ext4, Btrfs, FUSE)
• Use-after-free and double-free bugs in kernel memory management

Other Kernel Fuzzers

Fuzzing + Formal Methods Integration

Formal Specifications as Fuzzing Oracles

The most powerful integration of fuzzing and formal methods uses formal specifications as test oracles for fuzzers:

// Instead of checking for crashes:
// fuzz_input → execute → check crash?

// With formal oracle:
// fuzz_input → execute → formal_oracle(input, output) → pass/fail?

CSmith: C Program Fuzzer

CSmith generates random but syntactically valid C programs designed to stress-test compiler optimizations. The generated programs are guaranteed to be well-defined (no undefined behavior), so any difference between two compilers is a compiler bug.

CSmith pipeline:
Generate random C program → Compile with GCC → Compile with Clang
→ Run both binaries → Compare outputs
→ If different: compiler bug!

Comparison of Fuzzing Approaches

Interview Questions

Q1: How does coverage-guided fuzzing work?

Coverage-guided fuzzing instruments the target program to track code coverage (typically edge coverage). It maintains a corpus of seed inputs and generates new inputs by mutating existing ones. Inputs that discover new coverage edges are added to the corpus. Over time, this evolutionary process drives exploration toward uncovered code, finding bugs in rarely exercised paths.

Q2: What is property-based testing and when is it better than unit tests?

Property-based testing specifies general properties that should hold for all valid inputs (e.g., sort(sort(x)) == sort(x)), rather than testing specific input-output pairs. It is better when: (1) the input space is too large for hand-written tests, (2) edge cases are hard to anticipate, (3) you want to verify algebraic properties, or (4) the framework provides automatic shrinking for minimal counterexamples.

Q3: How does differential testing find compiler bugs?

Differential testing compiles the same source program with multiple compilers (e.g., GCC and Clang) and compares the outputs. If the same well-defined program produces different outputs from different compilers, at least one has a bug. CSmith generates random C programs guaranteed to be well-defined, making output differences clear compiler bugs rather than undefined behavior.

Q4: What makes kernel fuzzing harder than user-space fuzzing?

Kernel fuzzing is harder because: (1) kernel crashes affect the entire system, requiring VM isolation; (2) the kernel has complex global state (devices, networking, processes); (3) the interface is system calls with hundreds of parameters and complex state machines; (4) state persists across calls, requiring long sequences of syscalls to reach deep code; (5) crashes may be unreproducible due to timing-dependent behavior.

Q5: What is the oracle problem and how does metamorphic testing address it?

The oracle problem occurs when there is no clear way to determine the correct output for a given input (common in ML, scientific computing, search). Metamorphic testing addresses this by defining relations between the outputs of related inputs instead of comparing against an expected output. For example, if f(x+1) - f(x) = 1 should hold, testing this relation doesn’t require knowing the exact value of f(x).

Related Topics

• Program Verification — Symbolic execution, formal analysis
• Verified Systems — Complementary to testing: proof vs testing
• Distributed Verification — Protocol fuzzing and verification
• Security — Fuzzing for security vulnerabilities
• Software Engineering — General testing practices