What is it about?
We present a tool that can automatically search for fast implementations. We generate some correct implementation for a given input function. We then change the order of operations or change instructions. We run both versions and see which one is faster. Then discard the slow one and repeat. Finally, we verify that it is in fact implementing the input function.
Featured Image
Photo by Veri Ivanova on Unsplash
Why is it important?
As long as there exist implementations for cryptography, experts have been trying to improve performance without introducing bugs. Now with our tool chain, we can automate parts of this. In particular, we can now generate highly performant implementations automatically (including formal correctness checks) where developers did not have the patience or resources to write by hand.
Perspectives
With CryptOpt we could show that random local search is a viable method to find fast implementations, especially when it is unclear why one implementation is better than another (like in modern CPUs). We hope that this tool can be applied to many other domains than cryptography, or targeting other architectures like ARM, CUDA or Go Assembly.
Joel Kuepper
University of Adelaide
Read the Original
This page is a summary of: CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives, Proceedings of the ACM on Programming Languages, June 2023, ACM (Association for Computing Machinery),
DOI: 10.1145/3591272.
You can read the full text:
Resources
Contributors
The following have contributed to this page
