A system-level game semantics
From MaRDI portal
Abstract: Game semantics is a trace-like denotational semantics for programming languages where the notion of legal observable behaviour of a term is defined combinatorially, by means of rules of a game between the term (the "Proponent") and its context (the "Opponent"). In general, the richer the computational features a language has, the less constrained the rules of the semantic game. In this paper we consider the consequences of taking this relaxation of rules to the limit, by granting the Opponent omnipotence, that is, permission to play any move without combinatorial restrictions. However, we impose an epistemic restriction by not granting Opponent omniscience, so that Proponent can have undisclosed secret moves. We introduce a basic C-like programming language and we define such a semantic model for it. We argue that the resulting semantics is an appealingly simple combination of operational and game semantics and we show how certain traces explain system-level attacks, i.e. plausible attacks that are realizable outside of the programming language itself. We also show how allowing Proponent to have secrets ensures that some desirable equivalences in the programming language are preserved.
Recommendations
Cites work
- A Fully Abstract Trace Semantics for General References
- A new approach to abstract syntax with variable binding
- Angelic semantics of fine-grained concurrency
- Biorthogonality, step-indexing and compiler correctness
- Foundations of Software Science and Computation Structures
- From applicative to environmental bisimulation
- Full abstraction for PCF
- scientific article; zbMATH DE number 1231510 (Why is no real title available?)
- On full abstraction for PCF: I, II and III
- Parametricity and local variables
- Programming Languages and Systems
- Semantical analysis of specification logic
Cited in
(18)- Fully abstract trace semantics for protected module architectures
- A curry-style semantics of interaction: from untyped to second-order lazy -calculus
- Complete trace models of state and control
- Higher-order linearisability
- Latent semantic analysis of game models using LSTM
- Game semantics for access control
- Game semantics in the nominal model
- scientific article; zbMATH DE number 3878725 (Why is no real title available?)
- scientific article; zbMATH DE number 1241700 (Why is no real title available?)
- scientific article; zbMATH DE number 7456059 (Why is no real title available?)
- Higher-order linearisability
- The far side of the cube. An elementary introduction to game semantics
- Disentangling parallelism and interference in game semantics
- Symbolic execution game semantics
- Fully abstract normal form bisimulation for call-by-value PCF
- Pushdown normal-form bisimulation: a nominal context-free approach to program equivalence
- A robust graph-based approach to observational equivalence
- Nanopass back-translation of call-return trees for mechanized secure compilation proofs
This page was built for publication: A system-level game semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3178283)
