Output-sensitive information flow analysis

MaRDI QIDQ5856419zbMATH OpenFDO

Authors Laurent Mounier, Marie-Laure Potet, Cristian Ene

Publication date 26 March 2021

Full work available at URL https://arxiv.org/abs/1909.09567, https://lmcs.episciences.org/7172

zbMATH Keywords

type systeminformation flowoutput-sensitive non-interference

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Verifying constant-time implementations by abstract interpretation
• System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
• System-level non-interference of constant-time cryptography. I: Model
• Tempus fugit: How to plug it
• All Secrets Great and Small

Cites work

• Downgrading policies and relaxed noninterference
• Information Security and Cryptology - ICISC 2005
• Lucky microseconds: a timing attack on Amazon's s2n implementation of TLS
• On flow-sensitive security types
• Security types preserving compilation
• The program dependence graph and its use in optimization
• The security impact of a new cryptographic library
• Transforming out timing leaks
• Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC
• Verification, Model Checking, and Abstract Interpretation
• Verifying constant-time implementations by abstract interpretation

Cited in

(3)

• System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
• Output-sensitive information flow analysis
• Verifying constant-time implementations by abstract interpretation

Describes a project that uses

Uses Software

• CacheAudit
• JFlow
• NaCl
• Boogie
• LLVM

This page was built for publication: Output-sensitive information flow analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5856419)