A formalized programming language with speculative execution

Jamie Wright 📧 and Andrei Popescu 📧

August 16, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We present the formalization of a programming language whose operational semantics allows for the speculative execution of its statements. This type of semantics is relevant for discussing transient execution security vulnerabilities such as Spectre and Meltdown. An instantiation of Relative Security to this language is provided along with proofs of security and insecurity of selected programs from the Spectre benchmark.

License

BSD License

Topics

Related publications

  • https://doi.ieeecomputersociety.org/10.1109/CSF61375.2024.00027

Session IMP_With_Speculation

Depends on

Cite

× 
@article{IMP_With_Speculation-AFP,
  author  = {Jamie Wright and Andrei Popescu},
  title   = {A formalized programming language with speculative execution},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/IMP_With_Speculation.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest