Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.

论文提出了一种混合形式化验证方法，结合高层演绎推理和电路级推理，用于高度优化的加密汇编代码。该方法在 EasyCrypt 证明助手中扩展实现，通过使用等价性检查将安全保障传播到同一计算的不同优化或不同架构的实现中，从而降低低级别函数的证明工

历史摘要 · 未重新核验 · IEEE S&P