Formal Hardware/Software Models for Cache Locking Enabling Fast and Secure Code

Constant-time programming is the de facto standard to protect security-sensitive software against cache-based timing attacks. This software countermeasure is effective but may incur a significant performance overhead and require a substantial rewrite of the code. In this work, we study a secure cache-locking hardware mechanism which eases the writing of secure code and has little execution overhead. To reason about the security of software, we propose a high-level leakage model such that accesses to locked memory addresses do not generate any observable leakage. To ensure the adequacy of this leakage model, we also propose a concrete hardware leakage model for a RISC-V microcontroller where the secure code may be interrupted, at any time, by some arbitrary malicious code. Using the Observational Non-Interference setting, we show formally that the security of the software model is preserved at the hardware level. We evaluate the effectiveness and performance of this mechanism, notably on block ciphers. We also propose and evaluate a new constant-time sorting algorithm.