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

FMITF：轨道 II：密码库汇编实现的自动验证

• 批准号: 1917897
• 负责人: Santosh Nagarakatte
• 金额: $ 10万
• 依托单位: Rutgers University New Brunswick
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-08-01 至 2022-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1917897&HistoricalAwards=false
• 关键词: FMitF; Track; II; Automated; Verification

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.

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

项目成果

Approximating trigonometric functions for posits using the CORDIC method

使用 CORDIC 方法近似三角函数

• DOI: 10.1145/3387902.3392632
• 发表时间: 2020
• 期刊: CF '20: Proceedings of the 17th ACM International Conference on Computing Frontiers
• 作者: Lim, Jay P;Shachnai, Matan;Nagarakatte, Santosh
• 通讯作者: Nagarakatte, Santosh

Parallel Shadow Execution to Accelerate the Debugging of Numerical Errors

并行影子执行加速数值错误的调试

• DOI: 10.1145/3468264.3468585
• 发表时间: 2021
• 期刊: 2021 The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE
• 作者: Chowdhary, Sangeeta;Nagarakatte, Santosh
• 通讯作者: Nagarakatte, Santosh

One polynomial approximation to produce correctly rounded results of an elementary function for multiple representations and rounding modes

• DOI: 10.1145/3498664
• 发表时间: 2022-01
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Jay P. Lim;Santosh Nagarakatte

Debugging and detecting numerical errors in computation with posits

• DOI: 10.1145/3385412.3386004
• 发表时间: 2020-06
• 期刊: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
• 作者: Sangeeta Chowdhary;Jay P. Lim;Santosh Nagarakatte

An approach to generate correctly rounded math libraries for new floating point variants

• DOI: 10.1145/3434310
• 发表时间: 2021-01
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Jay P. Lim;Mridul Aanjaneya;John L. Gustafson;Santosh Nagarakatte