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

点击翻译按钮获取中文摘要

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.