Verifying constant-time implementations by abstract interpretation
From MaRDI portal
Publication:2167720
DOI10.1007/978-3-319-66402-6_16zbMath1496.68100MaRDI 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
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Unnamed Item, 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