Application Security

Property-Based Testing for Security: Defining Invariants That Must Never Break

Property-based testing defines invariants about program behavior and generates thousands of test cases automatically. For security code, the right properties can catch vulnerabilities that example-based tests miss.

James
Security Architect
5 min read

Traditional unit tests verify specific examples: "when I pass input X, I expect output Y." Property-based tests verify properties: "for ALL valid inputs, this property holds." The difference matters enormously for security, where a single edge case can be catastrophic.

Consider an authentication system. Example-based tests might check that a valid password is accepted and an invalid password is rejected. But what about passwords with Unicode characters? Null bytes? Extremely long strings? Empty strings? Strings that look like SQL injection? Property-based testing generates all of these automatically, guided by the properties you define.

What Are Security Properties

A security property is an invariant that must hold regardless of input. Some examples:

Authentication properties. Authentication should be symmetric: if encrypt(key, plaintext) produces ciphertext, then decrypt(key, ciphertext) produces plaintext. Authentication should reject all inputs that do not match valid credentials. Password comparison should take constant time regardless of where the mismatch occurs.

Authorization properties. Access control decisions should be deterministic: the same user, resource, and context should always produce the same decision. Escalation should be impossible: no sequence of valid API calls should grant a user permissions they were not explicitly assigned.

Input validation properties. Validated input should always be safe for its intended use. Encoding and decoding should be inverses: decode(encode(data)) equals data. Sanitized output should never contain prohibited patterns.

Cryptographic properties. Encryption should be indistinguishable from random. Signing and verification should be consistent. Key derivation should produce different keys for different inputs.

Property-Based Testing Frameworks

Hypothesis (Python). The most popular property-based testing framework for Python. It generates complex data structures, handles edge cases like Unicode, NaN, and empty collections, and shrinks failing examples to minimal reproductions.

fast-check (JavaScript/TypeScript). Property-based testing for JavaScript. Supports async operations, React components, and complex data generators. Integrates with Jest and other test frameworks.

QuickCheck (Haskell, ports to many languages). The original property-based testing framework. Its influence is visible in every subsequent framework. Ports exist for Erlang, Rust, Java, and other languages.

proptest (Rust). Property-based testing for Rust with composable strategies for generating test data. Integrates with cargo test and supports shrinking.

jqwik (Java). Property-based testing for Java that integrates with JUnit 5. Supports stateful testing and complex data generation.

Security Properties in Practice

Input validation roundtrip. If your application validates and sanitizes input, the roundtrip property ensures consistency:

from hypothesis import given
import hypothesis.strategies as st

@given(st.text())
def test_sanitized_input_is_safe(input_text):
    sanitized = sanitize(input_text)
    assert is_safe_for_html(sanitized)
    assert is_safe_for_sql(sanitized)

This generates thousands of strings -- including Unicode, control characters, and injection payloads -- and verifies that sanitization works for all of them.

Encoding consistency. For any encoding scheme (Base64, URL encoding, HTML entities), the roundtrip property should hold:

@given(st.binary())
def test_base64_roundtrip(data):
    encoded = base64_encode(data)
    decoded = base64_decode(encoded)
    assert decoded == data

Access control completeness. For every resource and action, the access control function should return a definitive allow or deny:

@given(user=user_strategy(), resource=resource_strategy(), action=action_strategy())
def test_access_control_complete(user, resource, action):
    result = check_access(user, resource, action)
    assert result in (AccessResult.ALLOW, AccessResult.DENY)
    # Never throws, never returns None, never hangs

Token validation strictness. Authentication tokens should only validate if they were properly generated:

@given(st.binary())
def test_random_tokens_always_rejected(random_bytes):
    token = random_bytes.hex()
    assert not validate_auth_token(token)

Advanced Patterns

Stateful testing. Property-based testing frameworks support stateful testing, where a sequence of operations is generated and properties are checked after each step. For security, this can test that a sequence of API calls never leads to privilege escalation, that session state is consistent after any sequence of operations, and that concurrent access does not create race conditions.

Oracle testing. When a reference implementation exists, property-based testing can verify that your implementation matches:

@given(st.text(), st.text())
def test_crypto_matches_reference(key, plaintext):
    our_result = our_encrypt(key, plaintext)
    reference_result = reference_encrypt(key, plaintext)
    assert our_result == reference_result

Metamorphic testing. When you do not know the exact expected output, you can test relationships between inputs and outputs. For a search function: searching for "term" should return a superset of results for "term AND extra_condition." This catches bugs where additional constraints incorrectly expand the result set.

Shrinking and Debugging

When a property-based test finds a failing case, the framework automatically shrinks it to the smallest input that still causes the failure. This is invaluable for security bugs because the minimal failing input reveals the exact boundary condition that the code handles incorrectly.

A property-based test might initially find that a 500-character Unicode string bypasses input validation. After shrinking, it might reduce to a single specific character, revealing that the validation function does not handle that character class.

Integrating into Security Testing

Property-based tests should run alongside unit tests in CI/CD. Configure the framework to run enough examples for confidence (Hypothesis defaults to 100 examples per test, but security properties should use more -- 1000 or 10000). Store the failing example database so that previously-found edge cases are always re-tested. Run property-based tests with sanitizers (ASan, UBSan) when testing native code.

How Safeguard.sh Helps

Safeguard.sh extends property-based testing principles to the supply chain level. While property-based testing validates that your code's security invariants hold, Safeguard.sh validates that your dependency chain's integrity invariants hold -- that packages come from expected sources, that versions match expectations, and that no unauthorized changes have been introduced. Both approaches are grounded in the same philosophy: define what must be true, and verify it continuously.

Never miss an update

Weekly insights on software supply chain security, delivered to your inbox.