Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Speaking to Silicon • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
How much does your hardware leak? Every computation leaves physical traces — execution time varies with secret data, power consumption correlates with register values, electromagnetic fields radiate internal state. This project formalizes information-theoretic side-channel security in Lean 4: leakage is mutual information I(Secret; Observable) over finite probability spaces. A device is secure when this quantity is bounded. The data processing inequality proves that post-processing observables cannot increase leakage, and composition theorems handle multiple observations.
Side-Channel Leakage Model
| Channel | Physical Observable | Leakage Measure |
|---|---|---|
| Timing | Execution duration | I(key; cycles) |
| Power | Current draw | I(key; trace) |
| EM | Electromagnetic field | I(key; spectrum) |
Key Verified Results
mutual_info_nonnegMutual information is non-negative
Entropy.lean
data_processing_ineqPost-processing cannot increase leakage
Leakage.lean
composition_boundMulti-observation leakage bounded by sum
Composition.lean
constant_time_zero_leakConstant-time execution implies zero timing leakage
Leakage.lean