arcanum_verify/
lib.rs

1//! # Arcanum Verification Tools
2//!
3//! Tools for verifying security properties of cryptographic implementations.
4//!
5//! ## Timing Analysis
6//!
7//! Detect timing side-channels using statistical methods:
8//!
9//! - **dudect**: Statistical timing leak detection
10//! - **CI integration**: Automated timing regression tests
11//! - **Reports**: Human-readable timing analysis reports
12//!
13//! ## Model Checking
14//!
15//! Formal verification of memory safety and correctness:
16//!
17//! - **Kani**: Bounded model checking for Rust
18//! - **Memory safety**: Prove absence of buffer overflows
19//! - **Functional correctness**: Verify invariants
20//!
21//! ## Example
22//!
23//! ```ignore
24//! use arcanum_verify::prelude::*;
25//!
26//! // Test AES-GCM for timing leaks
27//! let result = TimingTest::new("aes_gcm_encrypt")
28//!     .iterations(100_000)
29//!     .run(|class| {
30//!         let key = match class {
31//!             Class::Left => [0x00u8; 32],
32//!             Class::Right => [0xFFu8; 32],
33//!         };
34//!         Aes256Gcm::encrypt(&key, &nonce, &plaintext, None)
35//!     });
36//!
37//! assert!(result.is_constant_time(), "Timing leak detected: {}", result);
38//! ```
39//!
40//! ## Security Properties Verified
41//!
42//! - **Constant-time execution**: No timing side-channels
43//! - **Memory zeroization**: Secrets cleared on drop
44//! - **No buffer overflows**: Bounds checking verified
45//! - **No use-after-free**: Memory safety guaranteed
46
47#![deny(unsafe_code)]
48#![warn(missing_docs, rust_2018_idioms)]
49
50#[cfg(feature = "timing")]
51pub mod timing;
52
53pub mod reports;
54
55mod errors;
56
57pub use errors::VerifyError;
58
59#[cfg(feature = "timing")]
60pub use timing::{Class, TimingResult, TimingTest};
61
62/// Prelude for convenient imports.
63pub mod prelude {
64    pub use crate::errors::VerifyError;
65
66    #[cfg(feature = "timing")]
67    pub use crate::timing::{Class, TimingResult, TimingTest};
68}
69
70/// Statistical utilities for timing analysis.
71pub mod stats {
72    #[cfg(feature = "timing")]
73    use crate::timing::OnlineStats;
74
75    /// Compute Welch's t-statistic for two samples.
76    ///
77    /// Used to determine if two timing distributions differ significantly.
78    /// A |t| > 4.5 indicates a probable timing leak.
79    pub fn welch_t_test(sample1: &[f64], sample2: &[f64]) -> f64 {
80        let n1 = sample1.len() as f64;
81        let n2 = sample2.len() as f64;
82
83        if n1 < 2.0 || n2 < 2.0 {
84            return 0.0;
85        }
86
87        let mean1: f64 = sample1.iter().sum::<f64>() / n1;
88        let mean2: f64 = sample2.iter().sum::<f64>() / n2;
89
90        let var1: f64 = sample1.iter().map(|x| (x - mean1).powi(2)).sum::<f64>() / (n1 - 1.0);
91        let var2: f64 = sample2.iter().map(|x| (x - mean2).powi(2)).sum::<f64>() / (n2 - 1.0);
92
93        let se = (var1 / n1 + var2 / n2).sqrt();
94
95        if se == 0.0 {
96            0.0 // Identical distributions
97        } else {
98            (mean1 - mean2) / se
99        }
100    }
101
102    /// Compute Welch's t-statistic from online statistics.
103    ///
104    /// Memory-efficient version that uses pre-computed statistics.
105    #[cfg(feature = "timing")]
106    pub fn welch_t_online(stats1: &OnlineStats, stats2: &OnlineStats) -> f64 {
107        let n1 = stats1.count() as f64;
108        let n2 = stats2.count() as f64;
109
110        if n1 < 2.0 || n2 < 2.0 {
111            return 0.0;
112        }
113
114        let mean1 = stats1.mean();
115        let mean2 = stats2.mean();
116        let var1 = stats1.variance();
117        let var2 = stats2.variance();
118
119        let se = (var1 / n1 + var2 / n2).sqrt();
120
121        if se == 0.0 { 0.0 } else { (mean1 - mean2) / se }
122    }
123
124    /// Threshold for timing leak detection.
125    ///
126    /// A t-value above this threshold indicates a probable timing leak.
127    /// 4.5 corresponds to roughly 3 in 100,000 false positive rate.
128    pub const TIMING_LEAK_THRESHOLD: f64 = 4.5;
129
130    /// More stringent threshold for high-security applications.
131    pub const TIMING_LEAK_THRESHOLD_STRICT: f64 = 3.0;
132}
arcanum_verify/lib.rs

arcanum_verify/
lib.rs
