Formal Security Analysis & Verification

Constant-Time Execution (Side-Channel Resistance)

PQC-IIoT is hardened against timing side-channel attacks. A key principle is that the execution time of cryptographic operations must be independent of secret inputs (private keys, shared secrets).

Trapdoor Sampling (Falcon)

The most critical component for timing attacks in Falcon is the Gaussian sampler used during signature generation. PQC-IIoT relies on the constant-time implementation provided by pqcrypto-falcon (based on the reference C implementation or optimized assembly).

Verification:

  • Execution Paths: Independent of the sign of coefficients.
  • Table Lookups: Access patterns to pre-computed tables (e.g., for FFT or Gaussian CDF) are uniform or data-independent.

Comparison Operations (Kyber)

During decryption (decapsulation), the comparison of re-encrypted ciphertexts (c vs c') must be constant-time to prevent chosen-ciphertext attacks (e.g., exploiting partial decryption failures).

#![allow(unused)]
fn main() {
// Pseudocode for constant-time comparison
fn verify(a: &[u8], b: &[u8]) -> bool {
    let mut result = 0;
    for (x, y) in a.iter().zip(b.iter()) {
        result |= x ^ y; // Bitwise OR accumulates differences
    }
    result == 0 // Check if accumulator is zero
}
}

Memory Safety (Rust Guarantees)

PQC-IIoT leverages Rust's type system to eliminate entire classes of memory safety vulnerabilities common in C/C++ implementations (e.g., buffer overflows, use-after-free).

Ownership & Borrowing

  • Zero-Copy Parsing: Use of &[u8] slices with strict lifetimes ensures memory is valid during parsing.
  • Race Condition Prevention: Send and Sync traits enforce thread safety at compile time, critical for the SecurityProvider trait shared across threads.

Bounds Checking

All array accesses in Rust are bounds-checked by default. For performance-critical loops (e.g., NTT), we rely on iterator combinators (zip, chunks) which elide bounds checks safely while guaranteeing correctness.

Property-Based Verification (Proptest)

For the Double Ratchet session management, we use Property-Based Verification to prove mathematical invariants that unit tests cannot capture. Using the proptest framework, we generate thousands of valid and edge-case inputs to verify:

1. Cryptographic Correctness

Theorem: For any plaintext $P$ and any shared root key $K$, $\text{Decrypt}(\text{Encrypt}(P)) \equiv P$.

  • Verification: 1000+ random payloads tested per run.

2. Out-of-Order Recovery (Sliding Window)

Theorem: The session MUST be able to decrypt message $N$ even if received before message $N-1$ (within the window limit).

  • Verification: Messages are shuffled and fed to the receiver to ensure state consistency.

3. Replay Protection

Theorem: A message $M$ decrypted at time $T$ MUST be rejected if re-submitted at $T+1$.

  • Verification: Attempting to re-decrypt the same ciphertext always results in an Error::CryptoError.

Model Checking (Kani)

We use the Kani Rust Verifier for static analysis of critical bootloader logic. This allows us to prove the absence of panics in the MBR and Partition Manager.

1. Partition Manager Safety

We prove that select_boot_partition never panics and always returns a valid partition type, regardless of the value of retry_count or the state of the NAND flash model.

2. Double Ratchet State Transitions

In the Galactic Apex (V4) tier, we model the ratchet's memory usage to prove it never exceeds allocated bounds, even under adversarial sliding window attacks.

Physical Resilience (Space-Grade Physics)

For proofs regarding Single Event Upsets (SEUs) and Radiation Hardening, see Space-Grade Physics, which details the $P_{sys} \approx 3 \cdot 10^{-18}$ probability model used in our Triple Modular Redundancy (TMR) implementation.

Fuzzing & Property-Based Testing

Beyond formal proofs, we empirically verify security properties using fuzzing.

Targets

  1. Packet Parsing: SecureMqttClient::poll is fuzzed with random byte streams to ensure no panic or memory exhaustion occurs on malformed packets.
  2. Ciphertext Malleability: hybrid::decrypt is fuzzed with bit-flipped ciphertexts to ensure the authentication tag (AES-GCM) or FO-transform check (Kyber) consistently rejects invalid inputs.

Corpus

A persistent corpus of valid and invalid packets is maintained to prevent regression of known edge cases.