Verifying constant-time implementations by abstract interpretation

DOI10.1007/978-3-319-66402-6_16zbMath1496.68100OpenAlexW2745299473MaRDI QIDQ2167720

Sandrine Blazy, David Pichardie, Alix Trieu

Publication date: 25 August 2022

Full work available at URL: https://hal.inria.fr/hal-02025047/file/jcs19.pdf

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Unnamed Item ⋮ Output-sensitive information flow analysis ⋮ System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory

Cites Work

• Unnamed Item
• The octagon abstract domain
• The Security Impact of a New Cryptographic Library
• Formalizing the LLVM intermediate representation for verified program transformations
• An abstract memory functor for verified C static analyzers
• Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems
• Grammar Analysis and Parsing by Abstract Interpretation
• A lattice model of secure information flow
• Information flow inference for ML
• Programming Languages and Systems
• Advances in Cryptology - CRYPTO 2003
• Public Key Cryptography - PKC 2006

This page was built for publication: Verifying constant-time implementations by abstract interpretation