Model checking speculation-dependent security properties: abstracting and reducing processor models for sound and complete verification

DOI10.1007/978-3-030-16458-4_27MaRDI QIDQ2327211zbMATH OpenOpenAlexFDO

Authors G. Cabodi, Paolo Camurati, Fabrizio Finocchiaro, Danilo Vendraminetto

Publication date 14 October 2019

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-16458-4_27

zbMATH Keywords

abstraction and reductionconfidentialitymeltdownmodel checkingpipeline flushingreorder buffersecure CPU architecturespectrespeculative executiontaint propagation

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25)

Recommendations

• Efficient Information-Flow Verification Under Speculative Execution
• Verifying Secure Speculation in Isabelle/HOL
• scientific article; zbMATH DE number 1796150
• scientific article; zbMATH DE number 1670784
• Self-Spectre, Write-Execute and the Hidden State

Cited in

(1)

• scientific article; zbMATH DE number 2102695 (Why is no real title available?)

This page was built for publication: Model checking speculation-dependent security properties: abstracting and reducing processor models for sound and complete verification

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