Arcanum Verification Tools

Tools for verifying security properties of cryptographic implementations.

Timing Analysis

Detect timing side-channels using statistical methods:

• dudect: Statistical timing leak detection
• CI integration: Automated timing regression tests
• Reports: Human-readable timing analysis reports

Model Checking

Formal verification of memory safety and correctness:

• Kani: Bounded model checking for Rust
• Memory safety: Prove absence of buffer overflows
• Functional correctness: Verify invariants

Example

use arcanum_verify::prelude::*;

// Test AES-GCM for timing leaks
let result = TimingTest::new("aes_gcm_encrypt")
    .iterations(100_000)
    .run(|class| {
        let key = match class {
            Class::Left => [0x00u8; 32],
            Class::Right => [0xFFu8; 32],
        };
        Aes256Gcm::encrypt(&key, &nonce, &plaintext, None)
    });

assert!(result.is_constant_time(), "Timing leak detected: {}", result);

Security Properties Verified

• Constant-time execution: No timing side-channels
• Memory zeroization: Secrets cleared on drop
• No buffer overflows: Bounds checking verified
• No use-after-free: Memory safety guaranteed