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 Oct

Displayed 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
30m
Full-paper
Verification of programs with ADTs using Shallow Horn Clauses
SAS
Théo Losekoot , Thomas Genet IRISA, Univ Rennes, Thomas P. Jensen INRIA Rennes
Pre-print
11:30
30m
Full-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
30m
Full-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