International Association
for Cryptologic Research

This talk will cover Amazon Web Service’s (AWS) experience implementing and deploying cryptographic algorithms (henceforth, by “algorithm” we mean “cryptographic algorithm”), implemented with carefully targeted micro-architectural optimizations and formally verified with Automated Reasoning (AR). We will survey the challenges we faced, their solutions, and innovations we have made, using our development of X25519 and Ed25519 implementations as examples throughout. First we will motivate the choice of those algorithms and the challenges that we faced. Secondly, we will introduce our solutions to those challenges: implementations of X25519 and Ed25519 optimized for both x86_64 and aarch64 micro-architectures; HOL Light, the AR engine used to formally verify correctness of the implementations; and the technology stack used at AWS for algorithm deployment. Thirdly, we will present performance data for our new implementations. Finally, we will present ongoing and future work at AWS combining AR and algorithm implementations. In summary, we will argue that combining AR and algorithm implementations is possible and can yield fruitful results, as well as explaining how AWS deploys algorithms at scale.