Programming errors in software applications can often be difficult to detect, as they may appear without clear indications of failure. One such example is when certain input variables have an unexpected impact on the program’s behavior. As an indicator of the program’s runtime behavior, this work studies the impact of input variables on the number of loop iterations in a program. Such information is valuable for debugging, optimizing performance, and analyzing security vulnerabilities, such as in side-channel attacks where execution times can be exploited. To address this issue, we propose a sound static analysis based on abstract interpretation to quantify the impact of each input variable on the global number of iterations. Our approach combines a dependency analysis with a global loop bound analysis to derive an over-approximation of the impact quantity. We demonstrate our prototype tool in the S2N-Bignum library for cryptographic systems to certify the absence of timing side-channels.
Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | Verification cost and quantitative analysisSAS at San Gabriel Chair(s): Sébastien Bardin CEA LIST, University Paris-Saclay | ||
11:00 30mFull-paper | Verification of programs with ADTs using Shallow Horn Clauses SAS Pre-print | ||
11:30 30mFull-paper | An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants SAS Louis Rustenholz Universidad Politécnica de Madrid (UPM) and IMDEA Software Institute, Pedro López-García IMDEA Software Institute, José Morales IMDEA Software Institute, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute Link to publication Pre-print File Attached | ||
12:00 30mFull-paper | Quantitative Static Timing Analysis SAS Denis Mazzucato INRIA & École Normale Supérieure, Marco Campion INRIA & École Normale Supérieure | Université PSL, Caterina Urban Inria - École Normale Supérieure Pre-print |