Verification of Side-Channel Resilience and Probabilistic Equivalence Checking (以英文演講)
- 講者Marc Gourjon 博士 (Max Planck Institute for Security and Privacy)
邀請人：楊柏因 - 時間2025-10-08 (Wed.) 10:30 ~ 12:30
- 地點資訊所新館106演講廳
摘要
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.