论文标题
有效验证优化代码：正确的高速X25519
Efficient Verification of Optimized Code: Correct High-speed X25519
论文作者
论文摘要
高度优化的代码对程序级验证提出了一个问题：程序员可以采用各种聪明的技巧，这些技巧是不平凡的。对于低功率设备上的密码学，至关重要的是，实现在功能上是正确，安全和有效的。这些通常是用手工精制的机器代码制成的，可以尽可能避免常规控制流动。 我们已正式验证了此类代码：在8位AVR微控制器上实现椭圆曲线加密的库。所选的实施是当前最有效的微体系结构。它由超过3000行的组装说明组成。在早期工作的基础上，我们使用Why3平台使用自动掠夺者对代码进行建模并证明验证条件。我们希望该方法可以重新使用和适应性，并且可以进行验证。此外，发现并纠正了原始实现的错误，同时降低了其内存足迹。这表明，对尖端代码的实际验证不仅可能是可能的，而且实际上可以提高其效率 - 显然是必要的。
Code that is highly optimized poses a problem for program-level verification: programmers can employ various clever tricks that are non-trivial to reason about. For cryptography on low-power devices, it is nonetheless crucial that implementations be functionally correct, secure, and efficient. These are usually crafted in hand-optimized machine code that eschew conventional control flow as much as possible. We have formally verified such code: a library which implements elliptic curve cryptography on 8-bit AVR microcontrollers. The chosen implementation is the most efficient currently known for this microarchitecture. It consists of over 3000 lines of assembly instructions. Building on earlier work, we use the Why3 platform to model the code and prove verification conditions, using automated provers. We expect the approach to be re-usable and adaptable, and it allows for validation. Furthermore, an error in the original implementation was found and corrected, at the same time reducing its memory footprint. This shows that practical verification of cutting-edge code is not only possible, but can in fact add to its efficiency -- and is clearly necessary.
