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.

Boldyreva et al. (Eurocrypt 2012) defined a fine-grained security model capturing ciphertext fragmentation attacks against symmetric encryption schemes. The model was extended by Albrecht et al. (CCS 2016) to include an integrity notion. The extended security model encompasses important security goals of SSH that go beyond confidentiality and integrity to include length hiding and denial-of-service resistance properties. Boldyreva et al. also defined and analysed the InterMAC scheme, while Albrecht et al. showed that InterMAC satisfies stronger security notions than all currently available SSH encryption schemes. In this work, we take the InterMAC scheme and make it fully ready for use in practice. This involves several steps. First, we modify the InterMAC scheme to support encryption of arbitrary length plaintexts and we replace the use of Encrypt-then-MAC in InterMAC with modern noncebased authenticated encryption. Second, we describe a reference implementation of the modified InterMAC scheme in the form of the library libInterMAC. We give a performance analysis of libInterMAC. Third, to test the practical performance of libInterMAC, we implement several InterMAC-based encryption schemes in OpenSSH and carry out a performance analysis for the use-case of file transfer using SCP. We measure the data throughput and the data overhead of using InterMAC-based schemes compared to existing schemes in OpenSSH. Our analysis shows that, for some network set-ups, using InterMAC-based schemes in OpenSSH only moderately affects performance whilst providing stronger security guarantees compared to existing schemes.