CryptOpt: Verified compilation with randomized program search for cryptographic primitives

Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
[doi] [Google Scholar] [DBLP] [Citeseer] [url]

Proc. ACM Program. Lang. 7(PLDI)
Association for Computing Machinery
New York, NY, USA
jun 2023
Note(s): cryptography, verification

Generates very fast crypto code using random mutation, hill-climbing and verification of the final result. To avoid finding a local maximum, they run with 100(?) random seeds, perform 1000(?) optimization steps then pick the winner so far and perform 100,000 more optimization steps.

Critically relies on being able to run with “typical input” so the random mutation approach is mostly limited to applications like crypto where timing does not vary with input value.