主要观点：硬件和软件系统易受漏洞影响，尤其是定时泄漏难以消除，本论文提出新的形式验证方法来排除此类漏洞并构建正确、安全且无泄漏的系统。
关键信息：

• 时间泄漏原因：包括非恒定时间代码、编译器生成的定时变化和微架构侧通道等。
• 提出理论：信息保留细化（IPR）理论用于捕捉非泄漏，在 Parfait 框架中实现了 IPR 验证方法并应用于验证硬件安全模块（HSMs）。
• 验证成果：使用 Parfait 在 Ibex 和 PicoRV32 硬件平台上实现并验证了多个 HSM，如 ECDSA 证书签名 HSM 和密码哈希 HSM，证明其泄漏不超过规定行为的 40 行规范。
  重要细节：
• 论文答辩时间：2024 年 7 月 15 日下午 2 点 ET（需注册参加）。
• 参与方式：公开，包括现场和 Zoom 会议，Zoom 需注册（https://forms.gle/VuSExjbmENaMcBHT7），现场 RSVP appreciated（https://forms.gle/pM72i12iiKmBt4Ej6）。
• 阅读资料：https://pdos.csail.mit.edu/papers/aathalye-thesis.pdf 。