Let's DOIT: Using Intel's extended HW/SW contract for secure compilation of crypto code
Authors | |
---|---|
Year of publication | 2025 |
Type | Article in Proceedings |
Conference | IACR Transactions on Cryptographic Hardware and Embedded Systems |
MU Faculty or unit | |
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: |