Efficient Information-Flow Verification Under Speculative Execution

DOI10.1007/978-3-030-31784-3_29zbMath1437.68111OpenAlexW2981929361MaRDI QIDQ3297608

Swen Jacobs, Yakir Vizel, Roderick Bloem

Publication date: 20 July 2020

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-31784-3_29

zbMATH Keywords

verificationspeculative executioninformation flowside channels

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Velev SAT Benchmarks
• SeaHorn

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal verification of side-channel countermeasures using self-composition
• Secure information flow by self-composition
• A Theory of Speculative Computation
• Certification of programs for secure information flow
• Transforming out timing leaks
• Static Analysis
• Computer Aided Verification
• Lazy self-composition for security verification