The constant-time programming discipline is an effective countermeasure against timing and cache-timing attacks, which can lead to complete breaks of otherwise secure systems. However, adhering to it is hard, especially under additional efficienty and legacy constraints. This makes automated verification of constant-time code an essential component for building secure software. We propose a novel approach, … Continue reading Verifying Constant-Time Implementations