Verification of Side-Channel Resilience and Probabilistic Equivalence Checking (Delivered in English)
- LecturerDr. Marc Gourjon (Max Planck Institute for Security and Privacy)
Host: Bo-Yin Yang - Time2025-10-08 (Wed.) 10:30 ~ 12:30
- LocationAuditorium 106 at IIS new Building
Abstract
Side-channel attacks pose a fundamental threat to the security of software and cryptographic schemes. Implementing effective countermeasures remains notoriously error-prone. Verification efforts have traditionally focused on algorithmic primitives, leaving a gap between formal guarantees and concrete implementations.
In the first part of the talk, I will present contributions to formally verifying the security of side-channel-protected software. I will introduce fine-grained models that capture physical and device-specific leakage behavior at the assembly level. These models enable the construction of automated verification tools that bring practical resilience within reach. Then, I will explain how these models can be automatically checked for accuracy, that is, whether they completely capture all leakage of a processor.
In the remainder, I will turn to the foundations of such tools: proof systems for reasoning about the equivalence or independence of probabilistic terms. This part will involve ongoing work addressing structural limitations in current approaches. Probabilistic equivalence checking also has applications beyond side-channel security; I look forward to exploring further connections in discussion with you.
In the first part of the talk, I will present contributions to formally verifying the security of side-channel-protected software. I will introduce fine-grained models that capture physical and device-specific leakage behavior at the assembly level. These models enable the construction of automated verification tools that bring practical resilience within reach. Then, I will explain how these models can be automatically checked for accuracy, that is, whether they completely capture all leakage of a processor.
In the remainder, I will turn to the foundations of such tools: proof systems for reasoning about the equivalence or independence of probabilistic terms. This part will involve ongoing work addressing structural limitations in current approaches. Probabilistic equivalence checking also has applications beyond side-channel security; I look forward to exploring further connections in discussion with you.