该论文研究了高保障密码学在现代处理器投机执行（Spectre）下的安全性。传统的高保障密码学通过程序验证和密码工程方法，提供内存安全、功能正确性、可证明安全性和无时序泄露的机器校验证明。然而，这些保证建立在顺序执行语义之上，与利用投机执行提高性能的现代处理器行为不匹配。Spectre式攻击利用投机执行漏洞，对高保障密码学的鲁棒性提出了质疑。论文基于Jasmin验证框架，提出了一种端到端的方法，用于在投机执行下证明密码软件的安全性。该方法扩展了现有验证技术，以覆盖投机执行路径，并保证即使在高性能处理器上也能抵御时序侧信道攻击。实验验证了该方法的有效性：实现了ChaCha20和Poly1305的高效、功能正确的汇编实现，这些实现既抵抗传统时序攻击，也抵抗投机执行攻击，且性能开销适中。主要贡献包括：1) 形式化描述了投机执行下的安全模型；2) 扩展Jasmin框架支持投机执行安全验证；3) 提供经过验证的密码原语实现。该工作对于构建下一代安全关键系统具有重要意义，证明了高保障密码学可以安全地部署在当今主流硬件上。