Cryptology ePrint Archive: Report 2020/1104

High-Assurance Cryptography Software in the Spectre Era

Gilles Barthe and Sunjay Cauligi and Benjamin Gregoire and Adrien Koutsos and Kevin Liao and Tiago Oliveira and Swarn Priya and Tamara Rezk and Peter Schwabe

Abstract: High-assurance cryptography leverages methods from program verification and cryptography engineering to deliver efficient cryptographic software with machine-checked proofs of memory safety, functional correctness, cryptographic security, and side-channel protection. Traditionally, these guarantees are established under a sequential execution semantics. However, this semantics is not aligned with the behavior of modern processors that make use of speculative execution to improve performance. This mismatch, combined with the high-profile Spectre-style attacks that exploit speculative execution, may naturally cast doubts on the robustness of high-assurance cryptography guarantees. In this paper, we dispel these doubts by showing that the benefits of high-assurance cryptography extend to speculative execution, at the cost of a modest performance overhead. We build atop the Jasmin verification framework an end-to-end approach for proving properties of cryptographic software under speculative execution, and validate our approach experimentally with efficient, functionally correct, side-channel protected assembly implementations of ChaCha20 and Poly1305.

Category / Keywords: implementation / high-assurance cryptography, verification, side-channel resistance, speculative execution

Date: received 13 Sep 2020

Contact author: kevliao at mit edu

Available format(s): PDF | BibTeX Citation

Version: 20200915:112808 (All versions of this report)

Short URL: ia.cr/2020/1104


[ Cryptology ePrint archive ]