A formalized programming language with speculative execution (Q7361809)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry IMP_With_Speculation
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A formalized programming language with speculative execution |
AFP entry IMP_With_Speculation |
Statements
16 August 2024
0 references
Jamie Wright
0 references
Andrei Popescu
0 references
A formalized programming language with speculative execution (English)
0 references
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.
0 references
