SaTC: CORE: Small: Scaling Correct-by-Construction Code Generation for Cryptography

SaTC：核心：小型：扩展密码学的构造正确代码生成

• 批准号: 2130671
• 负责人: Adam Chlipala
• 金额: $ 50万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-02-15 至 2025-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2130671&HistoricalAwards=false
• 关键词: SaTC; CORE; Small; Scaling; Correct

Cryptography secures communication in many parts of the modern world, from online shopping to private text messaging. Bugs in cryptographic software lead to information leakage and opportunities for bad actors to have undue influence on computer systems. Prior work by this research team began the Fiat Cryptography project, which generates fast and secure cryptographic code for intricate arithmetic algorithms, which previously had been painstakingly handcoded by experts. The new code-generation method has a rigorous mathematical proof of correctness (in a theorem-proving software package called Coq), which contrasts with the fallibility of the humans who had written similar code before. Today that tooling is used by all major web browsers. This project develops extensions to allow for even more real-world adoption, by covering more kinds of cryptographic code and improving performance and trustworthiness.The planned work has two main thrusts: expanding scope to higher-level code and lowering the system's guarantees to assembly instead of C. The first thrust involves moving beyond Fiat Cryptography's original specialization to straightline code, adding support for loops, function calls, precomputed tables, and mutable data structures. The intent is to retain the quality of starting from whiteboard-level purely functional programs and deriving fast imperative code from them automatically. However, recognizing the likely lack of a "one-size-fits-all" approach for such a wider range of programs, an extensible proof-generating compiler will be built, to which new code-derivation rules can be added if they are proved in Coq. The second project thrust studies how formal guarantees may be lowered to assembly code instead of C. Many important optimizations have been beyond the ability of compilers like GCC to apply automatically, but it is still desirable to establish correctness of those optimizations formally. To that end, a formally verified equivalence checker will be built, to certify that assembly programs compute the same mathematical functions as C-level programs generated by Fiat Cryptography. A collaboration with experts in genetic search should allow Fiat Cryptography to retain its push-button nature while still producing performance-competitive assembly code.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.

密码学保障了现代世界许多地方的通信安全，从在线购物到私人短信。 加密软件中的错误会导致信息泄露，并为不良行为者提供对计算机系统产生不当影响的机会。 该研究团队之前的工作开始了菲亚特密码学项目，该项目为复杂的算术算法生成快速、安全的密码代码，而这些算法以前是由专家精心手工编码的。 新的代码生成方法具有严格的正确性数学证明（在名为 Coq 的定理证明软件包中），这与以前编写类似代码的人类的易错性形成鲜明对比。 如今，所有主要网络浏览器都使用该工具。 该项目通过覆盖更多种类的加密代码并提高性能和可信度来开发扩展，以允许更多的现实世界采用。计划的工作有两个主要目标：将范围扩展到更高级别的代码并降低系统对汇编的保证第一个推动力涉及超越法定密码学最初的专业化，转向直线代码，添加对循环、函数调用、预计算表和可变数据结构的支持。 目的是保持从白板级纯函数式程序开始并自动从中派生快速命令式代码的质量。 然而，认识到对于如此广泛的程序可能缺乏“一刀切”的方法，将构建一个可扩展的证明生成编译器，如果新的代码派生规则被证明，则可以添加到该编译器中在柯克。 第二个项目主旨研究如何将形式保证降低到汇编代码而不是 C。许多重要的优化已经超出了 GCC 等编译器自动应用的能力，但仍然需要形式化地确定这些优化的正确性。 为此，将构建一个正式验证的等价检查器，以证明汇编程序计算的数学函数与菲亚特密码学生成的 C 级程序相同。 与基因搜索专家的合作应该使 Fiat Cryptography 能够保留其按钮性质，同时仍然生成具有性能竞争力的汇编代码。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响进行评估，被认为值得支持审查标准。

项目成果

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code

性能关键型应用程序的关系编译：功能模型到低级代码的可扩展证明生成翻译

• DOI: 10.1145/3519939.3523706
• 发表时间: 2022-06
• 期刊: PLDI 2022
• 作者: Pit;Philipoom, Jade;Jamner, Dustin;Erbsen, Andres;Chlipala, Adam
• 通讯作者: Chlipala, Adam

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives

CryptOpt：通过随机程序搜索加密原语进行验证编译

• DOI: 10.1145/3591272
• 发表时间: 2023-06-06
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Joel Kuepper;Andres Erbsen;Jason Gross;Owen Conoly;Chuyue Sun;Samuel Tian;David Wu;A. Chlipala;C. Chuengsatiansup;Daniel Genkin;Markus Wagner;Y. Yarom
• 通讯作者: Y. Yarom