Libra: Architectural Support For Principled, Secure And Efficient Balanced Execution On High-End Processors (Extended Version)
Hans Winderix, Marton Bognar, Lesly-Ann Daniel, Frank Piessens
TL;DR
This work tackles the CFL threat by challenging the assumption that secret-dependent control flow must be eliminated on modern high-end processors. It introduces Libra, a principled hardware-software contract that enables secure balanced execution by combining software-based folding of secret-dependent regions with targeted hardware support, including a folded memory layout and a level-offset ISA. The authors formalize the semantics, prove the folding transformation correct and secure, and characterize which hardware optimizations leak information, offering concrete design guidelines. Implemented on an out-of-order RISC-V core, Libra achieves balanced-execution overhead on par with insecure balanced code and outperforms state-of-the-art linearization by up to 19.3%, with modest hardware cost. The work provides a practical path to secure, efficient performance for high-end processors without disabling core microarchitectural features, advancing secure compilation for side-channel defenses and informing hardware designers.
Abstract
Control-flow leakage (CFL) attacks enable an attacker to expose control-flow decisions of a victim program via side-channel observations. Linearization (i.e., elimination) of secret-dependent control flow is the main countermeasure against these attacks, yet it comes at a non-negligible cost. Conversely, balancing secret-dependent branches often incurs a smaller overhead, but is notoriously insecure on high-end processors. Hence, linearization has been widely believed to be the only effective countermeasure against CFL attacks. In this paper, we challenge this belief and investigate an unexplored alternative: how to securely balance secret-dependent branches on higher-end processors? We propose Libra, a generic and principled hardware-software codesign to efficiently address CFL on high-end processors. We perform a systematic classification of hardware primitives leaking control flow from the literature, and provide guidelines to handle them with our design. Importantly, Libra enables secure control-flow balancing without the need to disable performance-critical hardware such as the instruction cache and the prefetcher. We formalize the semantics of Libra and propose a code transformation algorithm for securing programs, which we prove correct and secure. Finally, we implement and evaluate Libra on an out-of-order RISC-V processor, showing performance overhead on par with insecure balanced code, and outperforming state-of-the-art linearized code by 19.3%.