本文针对高保证密码学（High-Assurance Cryptography）在现代处理器投机执行（Speculative Execution）时代下的安全保证问题展开研究。传统上，高保证密码学通过程序验证与密码工程方法，为密码软件提供内存安全、功能正确性、可证明安全性以及无时序泄漏等机器可验证的保证，但这些保证通常基于顺序执行语义建立。然而，现代处理器为了提升性能普遍采用投机执行，导致实际执行行为与顺序语义不一致，加之著名的Spectre系列攻击利用投机执行漏洞，使得高保证密码学所承诺的安全属性受到质疑。本文旨在消除这些疑虑，证明高保证密码学的优势在投机执行环境下依然成立，且仅需付出适度的性能开销。作者在Jasmin验证框架之上构建了一种端到端的方法，用于在投机执行语义下证明密码软件的安全属性。该方法扩展了原有验证框架的能力，使其能够建模投机执行带来的微架构侧信道风险。通过在Jasmin中实现ChaCha20和Poly1305两种高效密码算法，作者生成了功能正确且高效的汇编实现，并利用形式化验证证明了这些实现不仅对传统时序攻击安全，而且对投机执行攻击（如Spectre）同样安全。实验结果表明，所提出的方法能够在不显著牺牲性能的前提下，为密码软件提供针对投机执行的高保证安全性。该研究的核心贡献在于：第一，首次将高保证密码学的验证目标扩展到投机执行语义，填补了形式化验证与微架构安全之间的空白；第二，提供了可复用的验证方法论和工具链，使密码工程师能够系统性地设计和验证抗投机执行攻击的密码实现；第三，通过实例验证了该方法的实用性和可扩展性。本文适合密码学与形式化验证领域的研究人员、安全架构师以及需要开发高安全性密码库的工程师阅读，尤其对关注侧信道攻击防御的蓝队人员具有参考价值。