Verifying Secure Speculation in Isabelle/HOL

DOI10.1007/978-3-030-90870-6_3MaRDI QIDQ6488460zbMATH OpenFDO

Authors Brijesh Dongol

Publication date 21 April 2023

Full work available at URL https://doi.org/10.1007/978-3-030-90870-6_3

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Efficient Information-Flow Verification Under Speculative Execution
• A theory of speculative computation
• Formally verified implementation of an idealized model of virtualization
• Securing a compiler transformation
• Lazy self-composition for security verification

Cited in

(3)

• How to simulate it in Isabelle: towards formal proof for secure multi-party computation
• Model checking speculation-dependent security properties: abstracting and reducing processor models for sound and complete verification
• A theory of speculative computation

This page was built for publication: Verifying Secure Speculation in Isabelle/HOL

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