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

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

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.