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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Quantitative Static Timing Analysis

  • Denis Mazzucato,
  • Marco Campion,
  • Caterina Urban

摘要

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.