Let's DOIT: Using Intel's extended HW/SW contract for secure compilation of crypto code

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ARRANS OLMOS Santiago BARTHE Gilles GRÉGOIRE Benjamin JANČÁR Ján LAPORTE Vincent OLIVEIRA Tiago SCHWABE Peter

Year of publication 2025
Type Article in Proceedings
Conference IACR Transactions on Cryptographic Hardware and Embedded Systems
MU Faculty or unit

Faculty of Informatics

Citation
web https://tches.iacr.org/index.php/TCHES/article/view/12229
Doi http://dx.doi.org/10.46586/tches.v2025.i3.644-667
Keywords data-operand-independent timing; Jasmin; high-assurance; constant-time code
Description It is a widely accepted standard practice to implement cryptographic software in such a way that secret inputs do not influence the cycle count. Software following this paradigm is often referred to as "constant-time" software and typically involves following three rules: 1) never branch on a secret-dependent condition, 2) never access memory at a secret-dependent location, and 3) avoid variable-time arithmetic operations on secret data. The third rule requires knowledge about what those variable-time arithmetic instructions are, or, vice-versa, which operations are safe to use on secret inputs. For a long time, this knowledge was based on either documentation or microbenchmarks, but critically, there were never any guarantees for future microarchitectures. This changed with the introduction of the data-operand-independent-timing (DOIT) mode on Intel CPUs and, to some extent, the data-independent-timing (DIT) mode on Arm CPUs. Both Intel and Arm document a subset of their respective instruction sets that is intended to not leak information about their inputs through timing, also on future microarchitectures, if the CPU is switched to run in a dedicated DOIT (or DIT) mode. In this paper we present a principled solution that leverages DOIT to enable cryptographic software that is future-proof constant-time, in the sense that it ensures that only instructions from the DOIT subset are used to operate on secret data, even during speculative execution after a mispredicted branch or function-return location. For this solution, we build on top of existing security type systems in the Jasmin framework for high-assurance cryptography. We then use our solution to evaluate to what extent existing cryptographic software that was build to be "constant-time" is already secure also in this stricter paradigm implied by DOIT and what the performance impact is to move from constant-time to future-proof constant-time.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info