Memory-Safe Elimination of Side Channels - Soares, Luigi; Pereira, Fernando Magno Quintão (Anais do Concurso de Teses e Dissertações da SBC (CTD-SBC); 2023: Anais do XXXVI Concurso de Teses e DissertaçõesDO - 10.5753/ctd.2023.229445, 2023)
In this project, we find a new service for partial control-flow linearization (PCFL), a code transformation initially conceived to maximize work performed in vectorized programs. We show that PCFL can be employed as a defense mechanism against timing attacks. This transformation is sound: given an instance of its public inputs, the partially linearized program always runs the same sequence of instructions, regardless of secret inputs. Incidentally, if the original program is publicly safe, then accesses to the data cache will be data oblivious in the transformed code. The transformation is optimal: every branch that depends on some secret data is linearized; no branch that depends on only public data is linearized. Therefore, the transformation preserves loops that depend exclusively on public information. If every branch that leaves a loop depends on secret data, then the transformed program will not terminate. Our transformation extends previous work in non-trivial ways. It handles C constructs such as “break”, “switch” and “continue”, which are absent in the FaCT domain-specific language (2018). Like Constantine (2021), our code transformation ensures operation invariance, but without requiring profiling information. Additionally, in contrast to SC-Eliminator (2018), our implementation handles programs containing general, unbounded loops.