FMitF: Track II: Automated Verification for Assembly Implementations of Cryptography Libraries

主流的加密库，如OpenSSL和BoringSSL，包含数千行手动优化的汇编代码，以实现高性能。不幸的是，这些系统中的bug相当普遍。该项目开发了一种技术和工具CASM-Verify，用于自动检查高度优化的加密算法汇编实现与这些算法的未优化参考版本的等价性，以确保在优化过程中不会引入错误。该项目的新颖之处在于将等价检验问题分解为几个小的子问题，使用具体和符号评估的结合。该项目旨在通过可用的等价性检查工具来提高广泛使用的加密库的安全性。该项目还将教育研究生和本科生以及各种正式工具和技术的实践者。作为该项目一部分开发的软件采用给定的参考和优化实现，并在随机生成的输入上具体执行这两种实现，并识别可能等效的变量。随后，利用可满足模理论解算器进行符号验证，以确定所识别的变量是否确实等价。此外，它使用一组内存访问优化将原始查询分解为小的子查询。为了使主流开发人员能够使用这些思想，本项目探索了以下方向：(1)支持Qhasm和Jasmin语言用于高速加密，(2)支持大整数算法的推理，以及(3)验证汇编实现的恒定时间属性。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Mainstream libraries for cryptography, like OpenSSL and BoringSSL, contain several thousand lines of manually optimized assembly code for high performance. Bugs in these systems are unfortunately somewhat common. This project develops techniques and a tool, CASM-Verify, to automatically check the equivalence of highly optimized assembly implementations of cryptographic algorithms against unoptimized reference versions of these algorithms in order to ensure that bugs are not introduced during the optimization process. The project's novelty is in decomposing the equivalence checking problem into several small sub-problems using a combination of concrete and symbolic evaluation. The project aims to improve the assurance of widely used cryptography libraries with usable equivalence checking tools. The project also will educate graduate and undergraduate students and practitioners on various formal tools and techniques.The software developed as part of this project takes a given a reference and an optimized implementation, and concretely execute the two implementations on randomly generated inputs and identifies likely equivalent variables. Subsequently, it uses symbolic verification using satisfiability modulo theory solvers to determine whether the identified variables are indeed equivalent. Further, it decomposes the original query into small sub-queries using a collection of optimizations for memory accesses. To enable the usage of these ideas by mainstream developers, this project explores the following directions: (1) support Qhasm and Jasmin languages for high-speed cryptography, (2) support reasoning about large integer arithmetic, and (3) verify constant-time properties of assembly implementations.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.